R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r = ⅟(star r)
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r = ⅟(star r)
have : star (⅟ r) = star (⅟ r) * ((star r) * ⅟ (star r)) := by
  simp only [mul_invOf_self, mul_one]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r = ⅟(star r)
rw [this, ← mul_assoc]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this✝ : star ⅟r = star ⅟r * (star r * ⅟(star r))
this : star ⅟r * star r = star 1
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)
have : (star (⅟ r)) * (star r) = star 1 := by rw [← star_mul, mul_invOf_self]
no goals
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this✝ : star ⅟r = star ⅟r * (star r * ⅟(star r))
this : star ⅟r * star r = star 1
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)
rw [this, star_one, one_mul]
no goals
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r = star ⅟r * (star r * ⅟(star r))
simp only [mul_invOf_self, mul_one]
no goals
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r = star 1
rw [← star_mul, mul_invOf_self]