no goals
α : 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
rwa [← lim_eq_zero_iff] at hf
α : 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)
α : 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)
have h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g := by rw [one_mul g]
α : 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)
α : 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)
have h₃ : f * inv f hf * g = (f * inv f hf) * g := by simp [mul_assoc]
α : 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)
α : 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)
have h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g := by rw [h₂, h₃, ← sub_mul]
α : 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)
α : 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)
have h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf) := by rw [h₄, mul_comm]
α : 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)
α : 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)
have h₆ : g - f * inv f hf * g = g * (1 - inv f hf * f) := by rw [h₅, mul_comm f]
α : 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))
α : 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)
rw [h₆]
no goals
α : 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))
exact mul_limZero_right _ (Setoid.symm (CauSeq.inv_mul_cancel _))
no goals
α : 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
rw [one_mul g]
no goals
α : 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
simp [mul_assoc]
no goals
α : 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
rw [h₂, h₃, ← sub_mul]
no goals
α : 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)
rw [h₄, mul_comm]
no goals
α : 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)
rw [h₅, mul_comm f]
α : 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)⁻¹)))
α : 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)⁻¹))
rw [sub_mul, ← sub_add, sub_sub, sub_add_eq_sub_sub, sub_right_comm, sub_add]
α : 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)⁻¹)))
α : 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)⁻¹)))
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)⁻¹)))
no goals
α : 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)⁻¹)))
exact sub_limZero
  (by rw [← mul_assoc, mul_right_comm, const_inv hl]; exact h₁ _ _ _)
  (by rw [← mul_assoc]; exact h₁ _ _ _)
α : 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)
α : 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)⁻¹))
rw [← mul_assoc, mul_right_comm, const_inv hl]
no goals
α : 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)
exact h₁ _ _ _
α : 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)⁻¹)
α : 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)⁻¹))
rw [← mul_assoc]
no goals
α : 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)⁻¹)
exact h₁ _ _ _