α : 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
α : 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
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
α : 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
α : 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
simp [hf]
no goals
α : 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
exact Quotient.sound (CauSeq.inv_mul_cancel hf)