-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem lim_mul_lim (f g : CauSeq β abv) : lim f * lim g = lim (f * g) :=
  eq_lim_of_const_equiv <|
    show LimZero (const abv (lim f * lim g) - f * g) by
      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)

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ (const abv (f.lim * g.lim) - f * g).LimZero

Tactic:
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]

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ (const abv (f.lim * g.lim) - f * g).LimZero

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero

Tactic:
exact
  add_limZero (mul_limZero_left _ (Setoid.symm (equiv_lim _)))
    (mul_limZero_right _ (Setoid.symm (equiv_lim _)))

Result:
no goals

Proof state:
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 (f.lim * g.lim) - f * g) = ↑((const abv f.lim - f) * g) + ↑(const abv f.lim * (const abv g.lim - g))

Tactic:
simp [sub_mul, mul_sub]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)

Tactic:
apply Subtype.ext

Result:
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 (f.lim * g.lim) - f * g) = ↑((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g))

Proof state:
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 (f.lim * g.lim) - f * g) = ↑((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g))

Tactic:
rw [coe_add]

Result:
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 (f.lim * g.lim) - f * g) = ↑((const abv f.lim - f) * g) + ↑(const abv f.lim * (const abv g.lim - g))

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ (const abv (f.lim * g.lim) - f * g).LimZero

Tactic:
rw [h]

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)
⊢ ((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero