[GOAL]
⊢ ∀ (a : PrimeMultiset), ⊥ ≤ a
[PROOFSTEP]
simp only [bot_le, forall_const]
[GOAL]
⊢ Repr PrimeMultiset
[PROOFSTEP]
delta PrimeMultiset
[GOAL]
⊢ Repr (Multiset Nat.Primes)
[PROOFSTEP]
infer_instance
[GOAL]
v : PrimeMultiset
p : ℕ
h : p ∈ toNatMultiset v
⊢ Nat.Prime p
[PROOFSTEP]
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
[GOAL]
case intro.mk.intro
v : PrimeMultiset
p : ℕ
h : p ∈ toNatMultiset v
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ v
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ Nat.Prime p
[PROOFSTEP]
exact h_eq ▸ hp'
[GOAL]
v : PrimeMultiset
p : ℕ+
h : p ∈ toPNatMultiset v
⊢ PNat.Prime p
[PROOFSTEP]
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
[GOAL]
case intro.mk.intro
v : PrimeMultiset
p : ℕ+
h : p ∈ toPNatMultiset v
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ v
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ PNat.Prime p
[PROOFSTEP]
exact h_eq ▸ hp'
[GOAL]
v : PrimeMultiset
⊢ Multiset.map PNat.val (toPNatMultiset v) = toNatMultiset v
[PROOFSTEP]
change (v.map (Coe.coe : Nat.Primes → ℕ+)).map Subtype.val = v.map Subtype.val
[GOAL]
v : PrimeMultiset
⊢ Multiset.map Subtype.val (Multiset.map Coe.coe v) = Multiset.map Subtype.val v
[PROOFSTEP]
rw [Multiset.map_map]
[GOAL]
v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Coe.coe) v = Multiset.map Subtype.val v
[PROOFSTEP]
congr
[GOAL]
v : PrimeMultiset
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
let h : (v.prod : ℕ) = ((v.map Coe.coe).map Coe.coe).prod := PNat.coeMonoidHom.map_multiset_prod v.toPNatMultiset
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe (Multiset.map Coe.coe v)) :=
  MonoidHom.map_multiset_prod PNat.coeMonoidHom (toPNatMultiset v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
rw [Multiset.map_map] at h
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
have : (Coe.coe : ℕ+ → ℕ) ∘ (Coe.coe : Nat.Primes → ℕ+) = Coe.coe := funext fun p => rfl
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
rw [this] at h
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
exact h
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ toNatMultiset (ofNatMultiset v h) = v
[PROOFSTEP]
dsimp [ofNatMultiset, toNatMultiset]
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := p, property := hp }) v h) = v
[PROOFSTEP]
have : (fun p h => (Coe.coe : Nat.Primes → ℕ) ⟨p, h⟩) = fun p _ => id p :=
  by
  funext p h
  rfl
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ (fun p h => Coe.coe { val := p, property := h }) = fun p x => id p
[PROOFSTEP]
funext p h
[GOAL]
case h.h
v : Multiset ℕ
h✝ : ∀ (p : ℕ), p ∈ v → Nat.Prime p
p : ℕ
h : Nat.Prime p
⊢ Coe.coe { val := p, property := h } = id p
[PROOFSTEP]
rfl
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
this : (fun p h => Coe.coe { val := p, property := h }) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := p, property := hp }) v h) = v
[PROOFSTEP]
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ ↑(prod (ofNatMultiset v h)) = Multiset.prod v
[PROOFSTEP]
rw [coe_prod, to_ofNatMultiset]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ toPNatMultiset (ofPNatMultiset v h) = v
[PROOFSTEP]
dsimp [ofPNatMultiset, toPNatMultiset]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
[PROOFSTEP]
have : (fun (p : ℕ+) (h : p.Prime) => (Coe.coe : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p :=
  by
  funext p h
  apply Subtype.eq
  rfl
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ (fun p h => Coe.coe { val := ↑p, property := h }) = fun p x => id p
[PROOFSTEP]
funext p h
[GOAL]
case h.h
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ Coe.coe { val := ↑p, property := h } = id p
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case h.h.a
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ ↑(Coe.coe { val := ↑p, property := h }) = ↑(id p)
[PROOFSTEP]
rfl
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
this : (fun p h => Coe.coe { val := ↑p, property := h }) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
[PROOFSTEP]
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ prod (ofPNatMultiset v h) = Multiset.prod v
[PROOFSTEP]
dsimp [prod]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.prod (toPNatMultiset (ofPNatMultiset v h)) = Multiset.prod v
[PROOFSTEP]
rw [to_ofPNatMultiset]
[GOAL]
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ ↑(prod (ofNatList l h)) = List.prod l
[PROOFSTEP]
have := prod_ofNatMultiset (l : Multiset ℕ) h
[GOAL]
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = Multiset.prod ↑l
⊢ ↑(prod (ofNatList l h)) = List.prod l
[PROOFSTEP]
rw [Multiset.coe_prod] at this
[GOAL]
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = List.prod l
⊢ ↑(prod (ofNatList l h)) = List.prod l
[PROOFSTEP]
exact this
[GOAL]
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → PNat.Prime p
⊢ prod (ofPNatList l h) = List.prod l
[PROOFSTEP]
have := prod_ofPNatMultiset (l : Multiset ℕ+) h
[GOAL]
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → PNat.Prime p
this : prod (ofPNatMultiset (↑l) h) = Multiset.prod ↑l
⊢ prod (ofPNatList l h) = List.prod l
[PROOFSTEP]
rw [Multiset.coe_prod] at this
[GOAL]
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → PNat.Prime p
this : prod (ofPNatMultiset (↑l) h) = List.prod l
⊢ prod (ofPNatList l h) = List.prod l
[PROOFSTEP]
exact this
[GOAL]
⊢ prod 0 = 1
[PROOFSTEP]
exact Multiset.prod_zero
[GOAL]
u v : PrimeMultiset
⊢ prod (u + v) = prod u * prod v
[PROOFSTEP]
change (coePNatMonoidHom (u + v)).prod = _
[GOAL]
u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom (u + v)) = prod u * prod v
[PROOFSTEP]
rw [coePNatMonoidHom.map_add]
[GOAL]
u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom u + ↑coePNatMonoidHom v) = prod u * prod v
[PROOFSTEP]
exact Multiset.prod_add _ _
[GOAL]
d : ℕ
u : PrimeMultiset
⊢ prod (d • u) = Pow.pow (prod u) d
[PROOFSTEP]
induction' d with n ih
[GOAL]
case zero
u : PrimeMultiset
⊢ prod (Nat.zero • u) = Pow.pow (prod u) Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
[PROOFSTEP]
have : ∀ n' : ℕ, Pow.pow (prod u) n' = Monoid.npow n' (prod u) := fun _ ↦ rfl
[GOAL]
case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
this : ∀ (n' : ℕ), Pow.pow (prod u) n' = Monoid.npow n' (prod u)
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
[PROOFSTEP]
rw [succ_nsmul, prod_add, ih, this, this, Monoid.npow_succ, mul_comm]
[GOAL]
n : ℕ+
⊢ ↑(PrimeMultiset.prod (factorMultiset n)) = ↑n
[PROOFSTEP]
dsimp [factorMultiset]
[GOAL]
n : ℕ+
⊢ ↑(PrimeMultiset.prod (PrimeMultiset.ofNatList (Nat.factors ↑n) (_ : ∀ {p : ℕ}, p ∈ Nat.factors ↑n → Nat.Prime p))) =
    ↑n
[PROOFSTEP]
rw [PrimeMultiset.prod_ofNatList]
[GOAL]
n : ℕ+
⊢ List.prod (Nat.factors ↑n) = ↑n
[PROOFSTEP]
exact Nat.prod_factors n.ne_zero
[GOAL]
v : PrimeMultiset
⊢ PNat.factorMultiset (prod v) = v
[PROOFSTEP]
apply PrimeMultiset.coeNat_injective
[GOAL]
case a
v : PrimeMultiset
⊢ Coe.coe (PNat.factorMultiset (prod v)) = Coe.coe v
[PROOFSTEP]
suffices toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v by exact this
[GOAL]
v : PrimeMultiset
this : toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v
⊢ Coe.coe (PNat.factorMultiset (prod v)) = Coe.coe v
[PROOFSTEP]
exact this
[GOAL]
case a
v : PrimeMultiset
⊢ toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v
[PROOFSTEP]
rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]
[GOAL]
case a
v : PrimeMultiset
⊢ ↑(Nat.factors (Multiset.prod (toNatMultiset v))) = toNatMultiset v
[PROOFSTEP]
rcases v with
  ⟨l⟩
    --unfold_coes
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (Multiset.prod (toNatMultiset (Quot.mk Setoid.r l)))) = toNatMultiset (Quot.mk Setoid.r l)
[PROOFSTEP]
dsimp [PrimeMultiset.toNatMultiset]
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (Multiset.prod ↑(List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
rw [Multiset.coe_prod]
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
let l' := l.map (Coe.coe : Nat.Primes → ℕ)
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
have : ∀ p : ℕ, p ∈ l' → p.Prime := fun p hp =>
  by
  rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
  exact h_eq ▸ hp'
[GOAL]
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
p : ℕ
hp : p ∈ l'
⊢ Nat.Prime p
[PROOFSTEP]
rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
[GOAL]
case intro.mk.intro
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
p : ℕ
hp : p ∈ l'
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ l
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ Nat.Prime p
[PROOFSTEP]
exact h_eq ▸ hp'
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
this : ∀ (p : ℕ), p ∈ l' → Nat.Prime p
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
exact Multiset.coe_eq_coe.mpr (@Nat.factors_unique _ l' rfl this).symm
[GOAL]
⊢ factorMultiset 1 = 0
[PROOFSTEP]
simp [factorMultiset, PrimeMultiset.ofNatList, PrimeMultiset.ofNatMultiset]
[GOAL]
n m : ℕ+
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
let u := factorMultiset n
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
let v := factorMultiset m
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
have : n = u.prod := (prod_factorMultiset n).symm
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
rw [this]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
[PROOFSTEP]
have : m = v.prod := (prod_factorMultiset m).symm
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
[PROOFSTEP]
rw [this]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * PrimeMultiset.prod v) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [← PrimeMultiset.prod_add]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod (u + v)) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
repeat' rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod (u + v)) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ u + v = factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ u + v = u + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n : ℕ+
m : ℕ
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
[PROOFSTEP]
let u := factorMultiset n
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
[PROOFSTEP]
have : n = u.prod := (prod_factorMultiset n).symm
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
[PROOFSTEP]
rw [this, ← PrimeMultiset.prod_smul]
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod (m • u)) = m • factorMultiset (PrimeMultiset.prod u)
[PROOFSTEP]
repeat' rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod (m • u)) = m • factorMultiset (PrimeMultiset.prod u)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ m • u = m • factorMultiset (PrimeMultiset.prod u)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
p : Nat.Primes
⊢ factorMultiset ↑p = PrimeMultiset.ofPrime p
[PROOFSTEP]
apply factorMultisetEquiv.symm.injective
[GOAL]
case a
p : Nat.Primes
⊢ ↑factorMultisetEquiv.symm (factorMultiset ↑p) = ↑factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)
[PROOFSTEP]
change (p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
[GOAL]
case a
p : Nat.Primes
⊢ PrimeMultiset.prod (factorMultiset ↑p) = PrimeMultiset.prod (PrimeMultiset.ofPrime p)
[PROOFSTEP]
rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]
[GOAL]
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset n ↔ m ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset n → m ∣ n
[PROOFSTEP]
intro h
[GOAL]
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ m ∣ n
[PROOFSTEP]
rw [← prod_factorMultiset m, ← prod_factorMultiset m]
[GOAL]
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) ∣ n
[PROOFSTEP]
apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod
[GOAL]
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) *
      PrimeMultiset.prod (factorMultiset n - factorMultiset m) =
    n
[PROOFSTEP]
rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h, prod_factorMultiset]
[GOAL]
case mpr
m n : ℕ+
⊢ m ∣ n → factorMultiset m ≤ factorMultiset n
[PROOFSTEP]
intro h
[GOAL]
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset n
[PROOFSTEP]
rw [← mul_div_exact h, factorMultiset_mul]
[GOAL]
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset m + factorMultiset (divExact n m)
[PROOFSTEP]
exact le_self_add
[GOAL]
m : ℕ+
v : PrimeMultiset
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
[PROOFSTEP]
let h := @factorMultiset_le_iff m v.prod
[GOAL]
m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ factorMultiset (PrimeMultiset.prod v) ↔ m ∣ PrimeMultiset.prod v := factorMultiset_le_iff
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
[PROOFSTEP]
rw [v.factorMultiset_prod] at h
[GOAL]
m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
[PROOFSTEP]
exact h
[GOAL]
u v : PrimeMultiset
⊢ prod u ∣ prod v ↔ u ≤ v
[PROOFSTEP]
let h := @PNat.factorMultiset_le_iff' u.prod v
[GOAL]
u v : PrimeMultiset
h : PNat.factorMultiset (prod u) ≤ v ↔ prod u ∣ prod v := PNat.factorMultiset_le_iff'
⊢ prod u ∣ prod v ↔ u ≤ v
[PROOFSTEP]
rw [u.factorMultiset_prod] at h
[GOAL]
u v : PrimeMultiset
h : u ≤ v ↔ prod u ∣ prod v
⊢ prod u ∣ prod v ↔ u ≤ v
[PROOFSTEP]
exact h.symm
[GOAL]
u : PrimeMultiset
n : ℕ+
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
[PROOFSTEP]
let h := @prod_dvd_iff u n.factorMultiset
[GOAL]
u : PrimeMultiset
n : ℕ+
h : prod u ∣ prod (PNat.factorMultiset n) ↔ u ≤ PNat.factorMultiset n := prod_dvd_iff
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
[PROOFSTEP]
rw [n.prod_factorMultiset] at h
[GOAL]
u : PrimeMultiset
n : ℕ+
h : prod u ∣ n ↔ u ≤ PNat.factorMultiset n
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
[PROOFSTEP]
exact h
[GOAL]
m n : ℕ+
⊢ factorMultiset (gcd m n) = factorMultiset m ⊓ factorMultiset n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ⊓ factorMultiset n
[PROOFSTEP]
apply le_inf_iff.mpr
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ∧ factorMultiset (gcd m n) ≤ factorMultiset n
[PROOFSTEP]
constructor
[GOAL]
case a.left
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.right
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset n
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.left
m n : ℕ+
⊢ gcd m n ∣ m
case a.right m n : ℕ+ ⊢ gcd m n ∣ n
[PROOFSTEP]
exact gcd_dvd_left m n
[GOAL]
case a.right
m n : ℕ+
⊢ gcd m n ∣ n
[PROOFSTEP]
exact gcd_dvd_right m n
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset (gcd m n)
[PROOFSTEP]
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
[GOAL]
case a
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ gcd m n
[PROOFSTEP]
apply dvd_gcd
[GOAL]
case a.hm
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ m
[PROOFSTEP]
rw [PrimeMultiset.prod_dvd_iff']
[GOAL]
case a.hn
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ n
[PROOFSTEP]
rw [PrimeMultiset.prod_dvd_iff']
[GOAL]
case a.hm
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset m
case a.hn m n : ℕ+ ⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
[PROOFSTEP]
exact inf_le_left
[GOAL]
case a.hn
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
[PROOFSTEP]
exact inf_le_right
[GOAL]
m n : ℕ+
⊢ factorMultiset (lcm m n) = factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset (lcm m n) ≤ factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
[GOAL]
case a
m n : ℕ+
⊢ lcm m n ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
[PROOFSTEP]
apply lcm_dvd
[GOAL]
case a.hm
m n : ℕ+
⊢ m ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
[PROOFSTEP]
rw [← factorMultiset_le_iff']
[GOAL]
case a.hn
m n : ℕ+
⊢ n ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
[PROOFSTEP]
rw [← factorMultiset_le_iff']
[GOAL]
case a.hm
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset m ⊔ factorMultiset n
case a.hn m n : ℕ+ ⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
exact le_sup_left
[GOAL]
case a.hn
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
exact le_sup_right
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset m ⊔ factorMultiset n ≤ factorMultiset (lcm m n)
[PROOFSTEP]
apply sup_le_iff.mpr
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset (lcm m n) ∧ factorMultiset n ≤ factorMultiset (lcm m n)
[PROOFSTEP]
constructor
[GOAL]
case a.left
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset (lcm m n)
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.right
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset (lcm m n)
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.left
m n : ℕ+
⊢ m ∣ lcm m n
case a.right m n : ℕ+ ⊢ n ∣ lcm m n
[PROOFSTEP]
exact dvd_lcm_left m n
[GOAL]
case a.right
m n : ℕ+
⊢ n ∣ lcm m n
[PROOFSTEP]
exact dvd_lcm_right m n
[GOAL]
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ Pow.pow (↑p) k ∣ m ↔ k ≤ Multiset.count p (factorMultiset m)
[PROOFSTEP]
intros
[GOAL]
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ Pow.pow (↑p) k ∣ m ↔ k ≤ Multiset.count p (factorMultiset m)
[PROOFSTEP]
rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow, factorMultiset_ofPrime]
[GOAL]
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ factorMultiset m ↔ Multiset.replicate k p ≤ factorMultiset m
[PROOFSTEP]
congr! 2
[GOAL]
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p
[PROOFSTEP]
apply Multiset.eq_replicate.mpr
[GOAL]
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
[PROOFSTEP]
constructor
[GOAL]
case a.h.e'_3.h.left
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k
[PROOFSTEP]
rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
[GOAL]
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
[PROOFSTEP]
intro q h
[GOAL]
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p
[PROOFSTEP]
rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h
[GOAL]
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p
[PROOFSTEP]
exact Multiset.eq_of_mem_replicate h
[GOAL]
u v : PrimeMultiset
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
[PROOFSTEP]
let n := u.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
[PROOFSTEP]
let m := v.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
[PROOFSTEP]
change (u ⊓ v).prod = PNat.gcd n m
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd n m
[PROOFSTEP]
have : u = n.factorMultiset := u.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (u ⊓ v) = PNat.gcd n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
[PROOFSTEP]
have : v = m.factorMultiset := v.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ PNat.factorMultiset m) = PNat.gcd n m
[PROOFSTEP]
rw [← PNat.factorMultiset_gcd n m, PNat.prod_factorMultiset]
[GOAL]
u v : PrimeMultiset
⊢ prod (u ⊔ v) = PNat.lcm (prod u) (prod v)
[PROOFSTEP]
let n := u.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
⊢ prod (u ⊔ v) = PNat.lcm (prod u) (prod v)
[PROOFSTEP]
let m := v.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊔ v) = PNat.lcm (prod u) (prod v)
[PROOFSTEP]
change (u ⊔ v).prod = PNat.lcm n m
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊔ v) = PNat.lcm n m
[PROOFSTEP]
have : u = n.factorMultiset := u.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (u ⊔ v) = PNat.lcm n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (PNat.factorMultiset n ⊔ v) = PNat.lcm n m
[PROOFSTEP]
have : v = m.factorMultiset := v.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊔ v) = PNat.lcm n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊔ PNat.factorMultiset m) = PNat.lcm n m
[PROOFSTEP]
rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]


[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
⊢ mk f = 0 ↔ LimZero f
[PROOFSTEP]
have : mk f = 0 ↔ LimZero (f - 0) := Quotient.eq
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
this : mk f = 0 ↔ LimZero (f - 0)
⊢ mk f = 0 ↔ LimZero f
[PROOFSTEP]
rwa [sub_zero] at this
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
⊢ mk (if h : LimZero f then 0 else inv f h) = mk (if h : LimZero g then 0 else inv g h)
[PROOFSTEP]
have := limZero_congr fg
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
⊢ mk (if h : LimZero f then 0 else inv f h) = mk (if h : LimZero g then 0 else inv g h)
[PROOFSTEP]
by_cases hf : LimZero f
[GOAL]
case pos
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : LimZero f
⊢ mk (if h : LimZero f then 0 else inv f h) = mk (if h : LimZero g then 0 else inv g h)
[PROOFSTEP]
simp [hf, this.1 hf, Setoid.refl]
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : ¬LimZero f
⊢ mk (if h : LimZero f then 0 else inv f h) = mk (if h : LimZero g then 0 else inv g h)
[PROOFSTEP]
have hg := mt this.2 hf
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : ¬LimZero f
hg : ¬LimZero g
⊢ mk (if h : LimZero f then 0 else inv f h) = mk (if h : LimZero g then 0 else inv g h)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : ¬LimZero f
hg : ¬LimZero g
⊢ mk (inv f (_ : ¬LimZero f)) = mk (inv g (_ : ¬LimZero g))
[PROOFSTEP]
have If : mk (inv f hf) * mk f = 1 := mk_eq.2 (inv_mul_cancel hf)
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : ¬LimZero f
hg : ¬LimZero g
If : mk (inv f hf) * mk f = 1
⊢ mk (inv f (_ : ¬LimZero f)) = mk (inv g (_ : ¬LimZero g))
[PROOFSTEP]
have Ig : mk (inv g hg) * mk g = 1 := mk_eq.2 (inv_mul_cancel hg)
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : ¬LimZero f
hg : ¬LimZero g
If : mk (inv f hf) * mk f = 1
Ig : mk (inv g hg) * mk g = 1
⊢ mk (inv f (_ : ¬LimZero f)) = mk (inv g (_ : ¬LimZero g))
[PROOFSTEP]
have Ig' : mk g * mk (inv g hg) = 1 := mk_eq.2 (mul_inv_cancel hg)
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : ¬LimZero f
hg : ¬LimZero g
If : mk (inv f hf) * mk f = 1
Ig : mk (inv g hg) * mk g = 1
Ig' : mk g * mk (inv g hg) = 1
⊢ mk (inv f (_ : ¬LimZero f)) = mk (inv g (_ : ¬LimZero g))
[PROOFSTEP]
rw [mk_eq.2 fg, ← Ig] at If
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : LimZero f ↔ LimZero g
hf : ¬LimZero f
hg : ¬LimZero g
If : mk (inv f hf) * mk g = mk (inv g hg) * mk g
Ig : mk (inv g hg) * mk g = 1
Ig' : mk g * mk (inv g hg) = 1
⊢ mk (inv f (_ : ¬LimZero f)) = mk (inv g (_ : ¬LimZero g))
[PROOFSTEP]
rw [← mul_one (mk (inv f hf)), ← Ig', ← mul_assoc, If, mul_assoc, Ig', mul_one]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : LimZero (const abv 0) then 0 else inv (const abv 0) h) = const abv 0
[PROOFSTEP]
rw [dif_pos] <;> [rfl; exact zero_limZero]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : LimZero (const abv 0) then 0 else inv (const abv 0) h) = const abv 0
[PROOFSTEP]
rw [dif_pos]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ 0 = const abv 0
[PROOFSTEP]
rfl
[GOAL]
case hc
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ LimZero (const abv 0)
[PROOFSTEP]
exact zero_limZero
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ (if h : LimZero f then 0 else inv f h) = inv f hf
[PROOFSTEP]
rw [dif_neg]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : 0 ≈ 1
this : LimZero (1 - 0)
⊢ LimZero 1
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : 0 ≈ 1
this✝ : LimZero (1 - 0)
this : LimZero 1
⊢ False
[PROOFSTEP]
apply one_ne_zero <| const_limZero.1 this
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : Quotient.mk equiv f ≠ 0
⊢ (Quotient.mk equiv f)⁻¹ * Quotient.mk equiv f = 1
[PROOFSTEP]
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ (Quotient.mk equiv f)⁻¹ * Quotient.mk equiv f = 1
[PROOFSTEP]
simp [hf]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ mk (inv f (_ : ¬LimZero f) * f) = 1
[PROOFSTEP]
exact Quotient.sound (CauSeq.inv_mul_cancel hf)
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : Quotient.mk equiv f ≠ 0
⊢ Quotient.mk equiv f * (Quotient.mk equiv f)⁻¹ = 1
[PROOFSTEP]
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ Quotient.mk equiv f * (Quotient.mk equiv f)⁻¹ = 1
[PROOFSTEP]
simp [hf]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ mk (f * inv f (_ : ¬LimZero f)) = 1
[PROOFSTEP]
exact Quotient.sound (CauSeq.mul_inv_cancel hf)
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
⊢ const abv x⁻¹ = if h : LimZero (const abv x) then 0 else inv (const abv x) h
[PROOFSTEP]
split_ifs with h <;> [simp [const_limZero.1 h]; rfl]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
⊢ const abv x⁻¹ = if h : LimZero (const abv x) then 0 else inv (const abv x) h
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
h : LimZero (const abv x)
⊢ const abv x⁻¹ = 0
[PROOFSTEP]
simp [const_limZero.1 h]
[GOAL]
case neg
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
h : ¬LimZero (const abv x)
⊢ const abv x⁻¹ = inv (const abv x) h
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
n : ℤ
d : ℕ
hd : d ≠ 0
hnd : Nat.coprime (Int.natAbs n) d
⊢ ↑(Rat.mk' n d) = ↑n * (↑d)⁻¹
[PROOFSTEP]
rw [← ofRat_ratCast, Rat.cast_mk', ofRat_mul, ofRat_inv]
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
n : ℤ
d : ℕ
hd : d ≠ 0
hnd : Nat.coprime (Int.natAbs n) d
⊢ ofRat ↑n * (ofRat ↑d)⁻¹ = ↑n * (↑d)⁻¹
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ ofRat (x / y) = ofRat x / ofRat y
[PROOFSTEP]
simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ LimZero (const abv (lim f + lim g) - (f + g))
[PROOFSTEP]
rw [const_add, add_sub_add_comm]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ LimZero (const abv (lim f) - f + (const abv (lim g) - g))
[PROOFSTEP]
exact add_limZero (Setoid.symm (equiv_lim f)) (Setoid.symm (equiv_lim g))
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ LimZero (const abv (lim f * lim g) - f * g)
[PROOFSTEP]
have h :
  const abv (lim f * lim g) - f * g = (const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g) :=
  by
  apply Subtype.ext
  rw [coe_add]
  simp [sub_mul, mul_sub]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ const abv (lim f * lim g) - f * g = (const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g)
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ ↑(const abv (lim f * lim g) - f * g) = ↑((const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g))
[PROOFSTEP]
rw [coe_add]
[GOAL]
case a
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ ↑(const abv (lim f * lim g) - f * g) = ↑((const abv (lim f) - f) * g) + ↑(const abv (lim f) * (const abv (lim g) - g))
[PROOFSTEP]
simp [sub_mul, mul_sub]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (lim f * lim g) - f * g = (const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g)
⊢ LimZero (const abv (lim f * lim g) - f * g)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (lim f * lim g) - f * g = (const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g)
⊢ LimZero ((const abv (lim f) - f) * g + const abv (lim f) * (const abv (lim g) - g))
[PROOFSTEP]
exact add_limZero (mul_limZero_left _ (Setoid.symm (equiv_lim _))) (mul_limZero_right _ (Setoid.symm (equiv_lim _)))
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
x : β
⊢ lim f * x = lim (f * const abv x)
[PROOFSTEP]
rw [← lim_mul_lim, lim_const]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ LimZero (-f - const abv (-lim f))
[PROOFSTEP]
rw [const_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ LimZero (const abv (lim f) - f)
[PROOFSTEP]
exact Setoid.symm (equiv_lim f)
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
⊢ LimZero f
[PROOFSTEP]
have hf := equiv_lim f
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
hf : f ≈ const abv (lim f)
⊢ LimZero f
[PROOFSTEP]
rw [h] at hf
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
hf : f ≈ const abv 0
⊢ LimZero f
[PROOFSTEP]
exact (limZero_congr hf).mpr (const_limZero.mpr rfl)
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero f
⊢ lim f = 0
[PROOFSTEP]
have h₁ : f = f - const abv 0 := ext fun n => by simp [sub_apply, const_apply]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero f
n : ℕ
⊢ ↑f n = ↑(f - const abv 0) n
[PROOFSTEP]
simp [sub_apply, const_apply]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero f
h₁ : f = f - const abv 0
⊢ lim f = 0
[PROOFSTEP]
rw [h₁] at h
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero (f - const abv 0)
h₁ : f = f - const abv 0
⊢ lim f = 0
[PROOFSTEP]
exact lim_eq_of_equiv_const h
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ lim f ≠ 0
[PROOFSTEP]
rwa [← lim_eq_zero_iff] at hf
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
⊢ LimZero (g - f * inv f hf * g)
[PROOFSTEP]
have h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g := by rw [one_mul g]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
⊢ g - f * inv f hf * g = 1 * g - f * inv f hf * g
[PROOFSTEP]
rw [one_mul g]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
⊢ LimZero (g - f * inv f hf * g)
[PROOFSTEP]
have h₃ : f * inv f hf * g = (f * inv f hf) * g := by simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
⊢ f * inv f hf * g = f * inv f hf * g
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
⊢ LimZero (g - f * inv f hf * g)
[PROOFSTEP]
have h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g := by rw [h₂, h₃, ← sub_mul]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
⊢ g - f * inv f hf * g = (1 - f * inv f hf) * g
[PROOFSTEP]
rw [h₂, h₃, ← sub_mul]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g
⊢ LimZero (g - f * inv f hf * g)
[PROOFSTEP]
have h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf) := by rw [h₄, mul_comm]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g
⊢ g - f * inv f hf * g = g * (1 - f * inv f hf)
[PROOFSTEP]
rw [h₄, mul_comm]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g
h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf)
⊢ LimZero (g - f * inv f hf * g)
[PROOFSTEP]
have h₆ : g - f * inv f hf * g = g * (1 - inv f hf * f) := by rw [h₅, mul_comm f]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g
h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf)
⊢ g - f * inv f hf * g = g * (1 - inv f hf * f)
[PROOFSTEP]
rw [h₅, mul_comm f]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g
h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf)
h₆ : g - f * inv f hf * g = g * (1 - inv f hf * f)
⊢ LimZero (g - f * inv f hf * g)
[PROOFSTEP]
rw [h₆]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬LimZero f✝
hl : lim f✝ ≠ 0
g f : CauSeq β abv
hf : ¬LimZero f
h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g
h₃ : f * inv f hf * g = f * inv f hf * g
h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g
h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf)
h₆ : g - f * inv f hf * g = g * (1 - inv f hf * f)
⊢ LimZero (g * (1 - inv f hf * f))
[PROOFSTEP]
exact mul_limZero_right _ (Setoid.symm (CauSeq.inv_mul_cancel _))
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
hl : lim f ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬LimZero f), LimZero (g - f * inv f hf * g)
⊢ LimZero (inv f hf - const abv (lim f)⁻¹ - (const abv (lim f) - f) * (inv f hf * const abv (lim f)⁻¹))
[PROOFSTEP]
rw [sub_mul, ← sub_add, sub_sub, sub_add_eq_sub_sub, sub_right_comm, sub_add]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
hl : lim f ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬LimZero f), LimZero (g - f * inv f hf * g)
⊢ LimZero
    (inv f hf - const abv (lim f) * (inv f hf * const abv (lim f)⁻¹) -
      (const abv (lim f)⁻¹ - f * (inv f hf * const abv (lim f)⁻¹)))
[PROOFSTEP]
show
  LimZero
    (inv f hf - const abv (lim f) * (inv f hf * const abv (lim f)⁻¹) -
      (const abv (lim f)⁻¹ - f * (inv f hf * const abv (lim f)⁻¹)))
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
hl : lim f ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬LimZero f), LimZero (g - f * inv f hf * g)
⊢ LimZero
    (inv f hf - const abv (lim f) * (inv f hf * const abv (lim f)⁻¹) -
      (const abv (lim f)⁻¹ - f * (inv f hf * const abv (lim f)⁻¹)))
[PROOFSTEP]
exact
  sub_limZero (by rw [← mul_assoc, mul_right_comm, const_inv hl]; exact h₁ _ _ _) (by rw [← mul_assoc]; exact h₁ _ _ _)
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
hl : lim f ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬LimZero f), LimZero (g - f * inv f hf * g)
⊢ LimZero (inv f hf - const abv (lim f) * (inv f hf * const abv (lim f)⁻¹))
[PROOFSTEP]
rw [← mul_assoc, mul_right_comm, const_inv hl]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
hl : lim f ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬LimZero f), LimZero (g - f * inv f hf * g)
⊢ LimZero (inv f hf - const abv (lim f) * inv (const abv (lim f)) (_ : ¬LimZero (const abv (lim f))) * inv f hf)
[PROOFSTEP]
exact h₁ _ _ _
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
hl : lim f ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬LimZero f), LimZero (g - f * inv f hf * g)
⊢ LimZero (const abv (lim f)⁻¹ - f * (inv f hf * const abv (lim f)⁻¹))
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬LimZero f
hl : lim f ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬LimZero f), LimZero (g - f * inv f hf * g)
⊢ LimZero (const abv (lim f)⁻¹ - f * inv f hf * const abv (lim f)⁻¹)
[PROOFSTEP]
exact h₁ _ _ _