[GOAL]
R : Type u
inst✝ : InvolutiveStar R
r s : R
h : r = star s
⊢ s = star r
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y : R
⊢ star (star x * y) = star y * x
[PROOFSTEP]
rw [star_mul, star_star]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y : R
⊢ star (x * star y) = y * star x
[PROOFSTEP]
rw [star_mul, star_star]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y z : R
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
[PROOFSTEP]
simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y : R
⊢ Commute (star x) y ↔ Commute x (star y)
[PROOFSTEP]
rw [← commute_star_star, star_star]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
src✝ : R ≃ Rᵐᵒᵖ := (Function.Involutive.toPerm star (_ : Function.Involutive star)).trans opEquiv
x y : R
⊢ Equiv.toFun
      { toFun := fun x => op (star x), invFun := src✝.invFun,
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (x * y) =
    Equiv.toFun
        { toFun := fun x => op (star x), invFun := src✝.invFun,
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        x *
      Equiv.toFun
        { toFun := fun x => op (star x), invFun := src✝.invFun,
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y
[PROOFSTEP]
simp only [star_mul, op_mul]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ star x ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
simp only [ne_eq, star_eq_zero]
[GOAL]
R : Type u
S : Type u_1
inst✝² : NonAssocSemiring S
inst✝¹ : CommSemiring R
inst✝ : StarRing R
⊢ Function.Involutive star
[PROOFSTEP]
intro
[GOAL]
R : Type u
S : Type u_1
inst✝² : NonAssocSemiring S
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : S →+* R
⊢ star (star x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type u_1
inst✝² : NonAssocSemiring S
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝¹ : S →+* R
x✝ : S
⊢ ↑(star (star x✝¹)) x✝ = ↑x✝¹ x✝
[PROOFSTEP]
simp only [RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply]
[GOAL]
R : Type u
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
⊢ star (x / y) = star x / star y
[PROOFSTEP]
apply op_injective
[GOAL]
case a
R : Type u
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
⊢ op (star (x / y)) = op (star x / star y)
[PROOFSTEP]
rw [division_def, op_div, mul_comm, star_mul, star_inv', op_mul, op_inv]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
r : R
⊢ star (bit0 r) = bit0 (star r)
[PROOFSTEP]
simp [bit0]
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R
⊢ star (bit1 r) = bit1 (star r)
[PROOFSTEP]
simp [bit1]
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
⊢ inverse (star a) = star (inverse a)
[PROOFSTEP]
by_cases ha : IsUnit a
[GOAL]
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : IsUnit a
⊢ inverse (star a) = star (inverse a)
[PROOFSTEP]
obtain ⟨u, rfl⟩ := ha
[GOAL]
case pos.intro
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ inverse (star ↑u) = star (inverse ↑u)
[PROOFSTEP]
rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ inverse (star a) = star (inverse a)
[PROOFSTEP]
rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
r : R
inst✝ : Invertible r
⊢ Star.star ⅟r * Star.star r = 1
[PROOFSTEP]
rw [← star_mul, mul_invOf_self, star_one]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
r : R
inst✝ : Invertible r
⊢ Star.star r * Star.star ⅟r = 1
[PROOFSTEP]
rw [← star_mul, invOf_mul_self, star_one]
[GOAL]
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)
[PROOFSTEP]
have : star (⅟r) = star (⅟r) * ((star r) * ⅟(star r)) := by simp only [mul_invOf_self, mul_one]
[GOAL]
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))
[PROOFSTEP]
simp only [mul_invOf_self, mul_one]
[GOAL]
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)
[PROOFSTEP]
rw [this, ← mul_assoc]
[GOAL]
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)
[PROOFSTEP]
have : (star (⅟r)) * (star r) = star 1 := by rw [← star_mul, mul_invOf_self]
[GOAL]
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
[PROOFSTEP]
rw [← star_mul, mul_invOf_self]
[GOAL]
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)
[PROOFSTEP]
rw [this, star_one, one_mul]
