[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₁ _ _ _
