α : 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)
α : 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)
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]
α : 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))
α : 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)
rw [h]
no goals
α : 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))
exact
  add_limZero (mul_limZero_left _ (Setoid.symm (equiv_lim _)))
    (mul_limZero_right _ (Setoid.symm (equiv_lim _)))
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))
α : 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)
apply Subtype.ext
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))
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))
rw [coe_add]
no goals
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))
simp [sub_mul, mul_sub]