case pos
K : Type u_1
E : Type ?u.6057953
inst✝ : IsROrC K
h : I = 0
⊢ I⁻¹ = -I

case neg
K : Type u_1
E : Type ?u.6057953
inst✝ : IsROrC K
h : ¬I = 0
⊢ I⁻¹ = -I
K : Type u_1
E : Type ?u.6057953
inst✝ : IsROrC K
⊢ I⁻¹ = -I
by_cases h : (I : K) = 0
no goals
case pos
K : Type u_1
E : Type ?u.6057953
inst✝ : IsROrC K
h : I = 0
⊢ I⁻¹ = -I
simp [h]
no goals
case neg
K : Type u_1
E : Type ?u.6057953
inst✝ : IsROrC K
h : ¬I = 0
⊢ I⁻¹ = -I
field_simp [I_mul_I_of_nonzero h]