α : 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
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
⊢ mk f = 0 ↔ LimZero f
have : mk f = 0 ↔ LimZero (f - 0) := Quotient.eq
no goals
α : 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
rwa [sub_zero] at this