no goals
α : Type u_2
inst✝² : LinearOrderedField α
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : 0 ≈ 1
this : LimZero (1 - 0)
⊢ LimZero 1
simpa
no goals
α : Type u_2
inst✝² : LinearOrderedField α
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : 0 ≈ 1
this✝ : LimZero (1 - 0)
this : LimZero 1
⊢ False
apply one_ne_zero <| const_limZero.1 this