awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
U : ↥(unitary R)
a : ℕ
⊢ (↑(U ^ Int.ofNat a) : R) = (↑U : R) ^ Int.ofNat a

Tactic:
simp [SubmonoidClass.coe_pow]

Premises used: SubmonoidClass.coe_pow
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
U : ↥(unitary R)
a : ℕ
⊢ (↑(U ^ Int.negSucc a) : R) = (↑U : R) ^ Int.negSucc a

Tactic:
simp [coe_inv]

Premises used: Unitary.coe_inv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
U : ↥(unitary R)
⊢ Membership.mem (γ := Submonoid R) (unitary R) (-(↑U : R))

Tactic:
simp [mem_iff, star_neg]

Premises used: star_neg, Unitary.mem_iff
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
U : ↥(unitary R)
⊢ (↑(-U) : R) = -(↑U : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : StarMul A
a : A
U : ↥(unitary A)
⊢ spectrum R ((↑U : A) * a * star (↑U : A)) = spectrum R a

Tactic:
spectrum.units_conjugate (u := toUnits U)

Premises used: spectrum.units_conjugate
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : StarMul A
a : A
U : ↥(unitary A)
⊢ spectrum R (star (↑U : A) * a * (↑U : A)) = spectrum R a

Tactic:
simpa using spectrum_star_right_conjugate (U := star U)

Premises used: Unitary.spectrum_star_right_conjugate
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
inst : Ring R
inst_1 : StarRing R
p : R
hp : IsStarProjection p
⊢ Membership.mem (γ := Submonoid R) (unitary R) (2 * p - 1)

Tactic:
simp only [two_mul, Unitary.mem_iff, star_sub, star_add,
    hp.isSelfAdjoint.star_eq, star_one, mul_sub, mul_add,
    sub_mul, add_mul, hp.isIdempotentElem.eq, one_mul, add_sub_cancel_right,
    mul_one, sub_sub_cancel, and_self]

Premises used: add_mul, IsStarProjection.isIdempotentElem, mul_sub, and_self, StarAddMonoid.star_add, two_mul, sub_mul, sub_sub_cancel, IsStarProjection.isSelfAdjoint, star_sub, Unitary.mem_iff, mul_add, IsIdempotentElem.eq, add_sub_cancel_right, mul_one, IsSelfAdjoint.star_eq, one_mul, star_one
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
x : R
dsimp : (↑u : R) * star x * (↑u⁻¹ : R) = star ((↑u : R) * x * (↑u⁻¹ : R))
⊢ (RingEquiv.toEquiv
          (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
            ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) u) : ConjAct Rˣ))).toFun
      (star x) =
    star
      ((RingEquiv.toEquiv
            (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
              ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) u) : ConjAct Rˣ))).toFun
        x)

Tactic:
dsimp [ConjAct.units_smul_def]

Premises used: ConjAct.units_smul_def
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
x : R
⊢ (↑u : R) * star x * (↑u⁻¹ : R) = star ((↑u : R) * x * (↑u⁻¹ : R))

Tactic:
simp [mul_assoc, ← Unitary.star_eq_inv]

Premises used: mul_assoc, Unitary.star_eq_inv
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
h :
  ∀ (a : R),
    Eq (α := R)
      ((let __RingEquiv : R ≃+* R :=
              MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
                ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) 1) : ConjAct Rˣ);
            { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ } :
            (a : R) → R)
          a :
        R)
      ((1 : (a : R) → R) a : R)
⊢ Eq.{u_2 + 1} (α := R ≃⋆ₐ[S] R)
    (let __RingEquiv : R ≃+* R :=
      MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
        ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) 1) : ConjAct Rˣ);
    { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ })
    1

Tactic:
ext
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
a : R
⊢ Eq (α := R)
    ((let __RingEquiv : R ≃+* R :=
            MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
              ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) 1) : ConjAct Rˣ);
          { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ } :
          (a : R) → R)
        a :
      R)
    ((1 : (a : R) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
g h : ↥(unitary R)
h₁ :
  ∀ (a : R),
    Eq (α := R)
      ((let __RingEquiv : R ≃+* R :=
              MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
                ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) (g * h)) :
                  ConjAct Rˣ);
            { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ } :
            (a : R) → R)
          a :
        R)
      ((HMul.hMul (α := R ≃⋆ₐ[S] R)
              (let __RingEquiv : R ≃+* R :=
                MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
                  ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) g) : ConjAct Rˣ);
              { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ : R ≃⋆ₐ[S] R })
              (let __RingEquiv : R ≃+* R :=
                MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
                  ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) h) : ConjAct Rˣ);
              { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ : R ≃⋆ₐ[S] R }) :
            (a : R) → R)
          a :
        R)
⊢ (let __RingEquiv : R ≃+* R :=
      MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
        ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) (g * h)) : ConjAct Rˣ);
    { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ }) =
    HMul.hMul (α := R ≃⋆ₐ[S] R)
      (let __RingEquiv : R ≃+* R :=
        MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
          ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) g) : ConjAct Rˣ);
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ : R ≃⋆ₐ[S] R })
      (let __RingEquiv : R ≃+* R :=
        MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
          ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) h) : ConjAct Rˣ);
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ : R ≃⋆ₐ[S] R })

Tactic:
ext
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
g h : ↥(unitary R)
a : R
⊢ Eq (α := R)
    ((let __RingEquiv : R ≃+* R :=
            MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
              ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) (g * h)) : ConjAct Rˣ);
          { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ } :
          (a : R) → R)
        a :
      R)
    ((HMul.hMul (α := R ≃⋆ₐ[S] R)
            (let __RingEquiv : R ≃+* R :=
              MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
                ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) g) : ConjAct Rˣ);
            { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ : R ≃⋆ₐ[S] R })
            (let __RingEquiv : R ≃+* R :=
              MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
                ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) h) : ConjAct Rˣ);
            { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ : R ≃⋆ₐ[S] R }) :
          (a : R) → R)
        a :
      R)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
x : R
⊢ (((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) x =
    (↑u : R) * x * star (↑u : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
x : R
⊢ (StarAlgEquiv.symm ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u) : (a : R) → R) x =
    star (↑u : R) * x * (↑u : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
x : R
⊢ (((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) (star u) : R ≃⋆ₐ[S] R) : (a : R) → R) x =
    star (↑u : R) * x * (↑u : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
h :
  ∀ (a : R),
    Eq (α := R) ((StarAlgEquiv.symm ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u) : (a : R) → R) a : R)
      ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) (star u) : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
⊢ Eq.{u_2 + 1} (α := R ≃⋆ₐ[S] R) (StarAlgEquiv.symm ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u))
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) (star u))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
a : R
⊢ Eq (α := R) ((StarAlgEquiv.symm ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u) : (a : R) → R) a : R)
    ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) (star u) : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)

Tactic:
simp [conjStarAlgAut_symm_apply]

Premises used: Unitary.conjStarAlgAut_symm_apply
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u₁ u₂ : ↥(unitary R)
⊢ Eq.{u_2 + 1} (α := R ≃⋆ₐ[S] R)
    (StarAlgEquiv.trans (B := R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u₁)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u₂))
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) (u₂ * u₁))

Tactic:
map_mul _ _ _ |>.symm

Premises used: map_mul, Eq.symm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u₁ u₂ : ↥(unitary R)
x : R
⊢ Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) (u₁ * u₂) : R ≃⋆ₐ[S] R) : (a : R) → R) x : R)
    ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u₁ : R ≃⋆ₐ[S] R) : (a : R) → R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u₂ : R ≃⋆ₐ[S] R) : (a : R) → R) x : R) :
      R)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
S : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
inst_2 : SMul S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
u : ↥(unitary R)
⊢ Eq (α := R ≃+* R)
    (StarRingEquiv.toRingEquiv
      (StarAlgEquiv.toStarRingEquiv.{u_1, u_2, u_2} (R := S)
        ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u)))
    (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R
      ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) u) : ConjAct Rˣ))

Tactic:
rfl

Premises used: MulSemiringAction.toRingEquiv, rfl
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra S R
u : ↥(unitary R)
⊢ Eq (α := R ≃ₐ[S] R) (StarAlgEquiv.toAlgEquiv ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u))
    (MulSemiringAction.toAlgEquiv (G := ConjAct Rˣ) S R
      ((ConjAct.toConjAct : (a : Rˣ) → ConjAct Rˣ) ((toUnits : (a : ↥(unitary R)) → Rˣ) u) : ConjAct Rˣ))

Tactic:
rfl

Premises used: StarAlgEquiv.toAlgEquiv, MulSemiringAction.toAlgEquiv, rfl
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra.IsCentral S R
u v : ↥(unitary R)
rw :
  Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
| Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_2
inst : Semiring R
inst_1 : StarMul R
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra.IsCentral S R
u v : ↥(unitary R)
conv_lhs :
  Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)

Tactic:
conv_lhs => rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
rw :
  Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
| Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
    ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
conv_lhs :
  Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
    ∃ (α : ↥(unitary S)), u = α • v
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) ↔
    ∃ (α : ↥(unitary S)), u = α • v

Tactic:
conv_lhs => rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
simp_rw : (∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)) ↔ ∃ (α : ↥(unitary S)), u = α • v
⊢ Eq (α := R ≃⋆ₐ[S] R) ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R)
      ((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) ↔
    ∃ (α : ↥(unitary S)), u = α • v

Tactic:
simp_rw [StarAlgEquiv.ext_iff, conjStarAlgAut_apply, ← coe_star, star_eq_inv,
    ← val_inv_toUnits_apply, ← val_toUnits_apply, mul_assoc, ← Units.eq_inv_mul_iff_mul_eq,
    ← mul_assoc, Units.eq_mul_inv_iff_mul_eq, mul_assoc, ← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),
    ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot, Algebra.mem_bot,
    Set.mem_range, Algebra.algebraMap_eq_smul_one, val_inv_toUnits_apply, val_toUnits_apply,
    ← star_eq_inv, coe_star]

Premises used: Units.val, Set.mem_range, Subalgebra.mem_center_iff, Algebra.mem_bot, Unitary.toUnits, mul_assoc, Unitary.conjStarAlgAut_apply, Algebra.algebraMap_eq_smul_one, Unitary.val_toUnits_apply, Inv.inv, Unitary.val_inv_toUnits_apply, Units.eq_mul_inv_iff_mul_eq, StarAlgEquiv.ext_iff, Algebra.IsCentral.center_eq_bot, Unitary.star_eq_inv, DFunLike.coe, Unitary.coe_star, Units.eq_inv_mul_iff_mul_eq
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (α : ↥(unitary S)), u = α • v
y : ↥(unitary S)
h : u = y • v
simp : HSMul.hSMul (β := R) (↑y : S) 1 = HSMul.hSMul (β := R) y 1
⊢ HSMul.hSMul (β := R) (↑y : S) 1 = star (↑v : R) * (↑u : R)

Tactic:
simp only [h, coe_smul, mul_smul_comm, SetLike.coe_mem, star_mul_self_of_mem]

Premises used: SetLike.coe_mem, Unitary.star_mul_self_of_mem, Unitary.coe_smul, mul_smul_comm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (α : ↥(unitary S)), u = α • v
y : ↥(unitary S)
h : u = y • v
⊢ HSMul.hSMul (β := R) (↑y : S) 1 = HSMul.hSMul (β := R) y 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
refine :
  (∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)) →
    ∀ (y : S) (h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)), ∃ (α : ↥(unitary S)), u = α • v
⊢ (∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)) ↔ ∃ (α : ↥(unitary S)), u = α • v

Tactic:
refine ⟨fun ⟨y, h⟩ ↦ ?_, fun ⟨y, h⟩ ↦ ⟨(y : S), by
    simp only [h, coe_smul, mul_smul_comm, SetLike.coe_mem, star_mul_self_of_mem]; rfl⟩⟩
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
⊢ (↑u : R) = y • (↑v : R)

Tactic:
simpa [← mul_assoc] using congr(v * $h).symm

Premises used: HMul.hMul, congrArg, mul_assoc, id, Eq.symm, Subtype.val
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
⊢ (↑u : R) = y • (↑v : R)

Tactic:
have huv : (u : R) = y • (v : R) := by simpa [← mul_assoc] using congr(v * $h).symm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
⊢ (↑v : R) = star y • (↑u : R)

Tactic:
simpa [← mul_assoc] using congr(u * (star $h)).symm

Premises used: HMul.hMul, congrArg, mul_assoc, id, Eq.symm, Subtype.val, Star.star
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
⊢ (↑v : R) = star y • (↑u : R)

Tactic:
have hvu : (v : R) = star y • (u : R) := by simpa [← mul_assoc] using congr(u * (star $h)).symm
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
⊢ (↑v : R) = (star y * y) • (↑v : R)

Tactic:
simp [← smul_smul, ← huv, ← hvu]

Premises used: smul_smul
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
⊢ (↑v : R) = (star y * y) • (↑v : R)

Tactic:
have hvy : (v : R) = (star y * y) • (v : R) := by simp [← smul_smul, ← huv, ← hvu]
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
hvy : (↑v : R) = (star y * y) • (↑v : R)
⊢ HSMul.hSMul.{u_4, u_3, u_3} (α := S) 1 (↑v : R) = (star y * y) • (↑v : R)

Tactic:
nth_rw 1 [← one_smul S (v : R)] at hvy

Premises used: one_smul, Subtype.val
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
hvy : HSMul.hSMul.{u_4, u_3, u_3} (α := S) 1 (↑v : R) = (star y * y) • (↑v : R)
⊢ star y * y = 1 ∨ (↑v : R) = 0

Tactic:
rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero, eq_comm] at hvy

Premises used: sub_eq_zero, sub_smul, eq_comm, smul_eq_zero