no goals
α : Type u_2
β : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Ring β
inst✝¹ : IsDomain β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : const abv 1 ≈ const abv 0
this : ∀ (ε : α), ε > 0 → ∃ i, ∀ (k : ℕ), i ≤ k → abv (1 - 0) < ε
h2 : 0 < abv 1
i : ℕ
hi : ∀ (k : ℕ), i ≤ k → abv (1 - 0) < abv 1
⊢ abv 1 < abv 1
simpa using hi _ le_rfl