case inl
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
⊢ 0⁻¹ = ↑(starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹

case inr
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = ↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
z : K
⊢ z⁻¹ = ↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
rcases eq_or_ne z 0 with (rfl | h₀)
no goals
case inl
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
⊢ 0⁻¹ = ↑(starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹
simp
case inr.a
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ z * (↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = 1
case inr
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = ↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
apply inv_eq_of_mul_eq_one_right
case inr.a
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ ↑(↑normSq z) ≠ 0
case inr.a
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ z * (↑(starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = 1
rw [← mul_assoc, mul_conj, ofReal_inv, ← normSq_eq_def', mul_inv_cancel]
no goals
case inr.a
K : Type u_1
E : Type ?u.5349633
inst✝ : IsROrC K
z : K
h₀ : z ≠ 0
⊢ ↑(↑normSq z) ≠ 0
rwa [ofReal_ne_zero, Ne.def, normSq_eq_zero]