case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : IsUnit a
⊢ inverse (star a) = star (inverse a)

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ inverse (star a) = star (inverse a)
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
⊢ inverse (star a) = star (inverse a)
by_cases ha : IsUnit a
no goals
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ inverse (star a) = star (inverse a)
rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
case pos.intro
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ inverse (star ↑u) = star (inverse ↑u)
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : IsUnit a
⊢ inverse (star a) = star (inverse a)
obtain ⟨u, rfl⟩ := ha
no goals
case pos.intro
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ inverse (star ↑u) = star (inverse ↑u)
rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]