no goals
α : Type u_2
inst✝² : LinearOrderedField α
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
⊢ const abv x⁻¹ = if h : LimZero (const abv x) then 0 else inv (const abv x) h
split_ifs with h <;> [simp [const_limZero.1 h]; rfl]