awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x y : ↥(unitary R)
a : star (↑(x * y) : R) = (↑(star y * star x) : R)
a₁ : star ((↑x : R) * (↑y : R)) = (↑(star y * star x) : R)
a₂ : star ((↑x : R) * (↑y : R)) = (↑(star y) : R) * (↑(star x) : R)
a₃ : star ((↑x : R) * (↑y : R)) = star (↑y : R) * (↑(star x) : R)
a₄ : star ((↑x : R) * (↑y : R)) = star (↑y : R) * star (↑x : R)
⊢ (↑(star (x * y)) : R) = (↑(star y * star x) : R)
have a₅ : star (↑y : R) * star (↑x : R) = star (↑y : R) * star (↑x : R)
Tactic: rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
⊢ Membership.mem (γ := Submonoid R) (unitary R) u ↔ star u * u = 1
have rw : ∀ (h_mul : star u * u = 1), u * star u = 1
Tactic: rw [mem_iff, and_iff_left_of_imp fun h_mul => ?_]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
⊢ u * star u = 1
have lift : ∀ (u : Rˣ) (h_mul : star (↑u : R) * (↑u : R) = 1), (↑u : R) * star (↑u : R) = 1
Tactic: lift u to Rˣ using hu
Cleared hypotheses: u, hu, h_mul
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
⊢ Membership.mem (γ := Submonoid R) (unitary R) u ↔ u * star u = 1
have rw : Membership.mem (γ := Submonoid R) (unitary R) (star u) ↔ u * star u = 1
Tactic: rw [← star_mem_iff, hu.star.mem_unitary_iff_star_mul_self, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
rw : Membership.mem (γ := Submonoid R) (unitary R) (star u) ↔ u * star u = 1
⊢ Membership.mem (γ := Submonoid R) (unitary R) u ↔ u * star u = 1
have rw₁ : star (star u) * star u = 1 ↔ u * star u = 1
Tactic: rw [← star_mem_iff, hu.star.mem_unitary_iff_star_mul_self, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
rw : Membership.mem (γ := Submonoid R) (unitary R) (star u) ↔ u * star u = 1
rw₁ : star (star u) * star u = 1 ↔ u * star u = 1
⊢ Membership.mem (γ := Submonoid R) (unitary R) u ↔ u * star u = 1
have rw₂ : u * star u = 1 ↔ u * star u = 1
Tactic: rw [← star_mem_iff, hu.star.mem_unitary_iff_star_mul_self, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw₂ : (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₂ : (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw₃ : (star b)⁻¹ * (star a * (a * b⁻¹)) = 1 ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₂ : (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₃ : (star b)⁻¹ * (star a * (a * b⁻¹)) = 1 ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw₄ : star a * (a * b⁻¹) = star b * 1 ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₂ : (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₃ : (star b)⁻¹ * (star a * (a * b⁻¹)) = 1 ↔ star a * a = star b * b
rw₄ : star a * (a * b⁻¹) = star b * 1 ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw₅ : star a * (a * b⁻¹) = star b ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₂ : (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₃ : (star b)⁻¹ * (star a * (a * b⁻¹)) = 1 ↔ star a * a = star b * b
rw₄ : star a * (a * b⁻¹) = star b * 1 ↔ star a * a = star b * b
rw₅ : star a * (a * b⁻¹) = star b ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw₆ : star a * a * b⁻¹ = star b ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₂ : (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₃ : (star b)⁻¹ * (star a * (a * b⁻¹)) = 1 ↔ star a * a = star b * b
rw₄ : star a * (a * b⁻¹) = star b * 1 ↔ star a * a = star b * b
rw₅ : star a * (a * b⁻¹) = star b ↔ star a * a = star b * b
rw₆ : star a * a * b⁻¹ = star b ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b
have rw₇ : star a * a = star b * b ↔ star a * a = star b * b
Tactic: rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
⊢ Eq (α := Submonoid Rˣ) (unitary Rˣ) (Submonoid.comap (F := Rˣ →* R) (Units.coeHom R) (unitary R))
have h : ∀ (x : Rˣ),
  Membership.mem (γ := Submonoid Rˣ) (unitary Rˣ) x ↔
    Membership.mem (γ := Submonoid Rˣ) (Submonoid.comap (F := Rˣ →* R) (Units.coeHom R) (unitary R)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
g : G
hg : Membership.mem (γ := Submonoid G) (unitary G) g
⊢ Membership.mem (γ := Submonoid G) (unitary G) g⁻¹
have simp_rw : ∀ (hg : star g * g = 1 ∧ g * star g = 1), g * star g = 1 ∧ star g * g = 1
Tactic: simp_rw [mem_iff, star_inv, ← mul_inv_rev, inv_eq_one] at *
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
F : Type u_5
inst_4 : FunLike F R S
inst_5 : StarHomClass F R S
inst_6 : MonoidHomClass F R S
f : F
r : R
hr : Membership.mem (γ := Submonoid R) (unitary R) r
⊢ Membership.mem (α := S) (γ := Submonoid S) (unitary S) ((f : (a : R) → S) r : S)
have hr₁ : star r * r = 1 ∧ r * star r = 1
Tactic: rw [mem_iff] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R →⋆* S
⊢ MonoidHom.comp toUnits (map f).toMonoidHom = (Units.map f.toMonoidHom).comp toUnits
have h : ∀ (x : ↥(unitary R)),
  Eq.{u_3 + 1} (α := S) (↑((MonoidHom.comp toUnits (map f).toMonoidHom : (a : ↥(unitary R)) → Sˣ) x) : S)
    (↑((((Units.map f.toMonoidHom).comp toUnits : MonoidHom.{u_2, u_3} (↥(unitary R)) Sˣ) : (a : ↥(unitary R)) → Sˣ)
          x) :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
U : ↥(unitary R)
z : ℤ
⊢ (↑(U ^ z) : R) = (↑U : R) ^ z
have ofNat : ∀ (a : ℕ), (↑(U ^ Int.ofNat a) : R) = (↑U : R) ^ Int.ofNat a
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
U : ↥(unitary R)
z : ℤ
ofNat : ∀ (a : ℕ), (↑(U ^ Int.ofNat a) : R) = (↑U : R) ^ Int.ofNat a
⊢ (↑(U ^ z) : R) = (↑U : R) ^ z
have negSucc : ∀ (a : ℕ), (↑(U ^ Int.negSucc a) : R) = (↑U : R) ^ Int.negSucc a
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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
⊢ (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)
have dsimp : (↑u : R) * star x * (↑u⁻¹ : R) = star ((↑u : R) * x * (↑u⁻¹ : R))
Tactic: dsimp [ConjAct.units_smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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
⊢ 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
have 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' := sorry, map_smul' := sorry } :
          (a : R) → R)
        a :
      R)
    ((1 : (a : R) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
⊢ (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 })
have 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' := sorry, map_smul' := sorry } :
          (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' := sorry, map_smul' := sorry : 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' := sorry, map_smul' := sorry : R ≃⋆ₐ[S] R }) :
          (a : R) → R)
        a :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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.{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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
| 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)
have 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)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
⊢ 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)
have 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)
Tactic: conv_lhs => rw [eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
⊢ 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)
have simp_rw : (∀ (a : R),
    Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
      ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
  ∃ (α : S), (↑u : R) = α • (↑v : R)
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, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
simp_rw :
  (∀ (a : R),
      Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
⊢ 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)
have simp_rw₁ : (∀ (a : R), (↑v : R) * a * star (↑v : R) = (↑u : R) * a * star (↑u : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
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, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
simp_rw :
  (∀ (a : R),
      Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₁ : (∀ (a : R), (↑v : R) * a * star (↑v : R) = (↑u : R) * a * star (↑u : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
⊢ 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)
have simp_rw₂ : (∀ (a : R), (↑v : R) * a * (↑(star v) : R) = (↑u : R) * a * (↑(star u) : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
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, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
simp_rw :
  (∀ (a : R),
      Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₁ : (∀ (a : R), (↑v : R) * a * star (↑v : R) = (↑u : R) * a * star (↑u : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₂ :
  (∀ (a : R), (↑v : R) * a * (↑(star v) : R) = (↑u : R) * a * (↑(star u) : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
⊢ 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)
have simp_rw₃ : (∀ (a : R), (↑v : R) * a * (↑v⁻¹ : R) = (↑u : R) * a * (↑u⁻¹ : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
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, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.UnitaryStarAlgAut (goal)
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)
simp_rw :
  (∀ (a : R),
      Eq (α := R) ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) v : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)
        ((((conjStarAlgAut S R : (a : ↥(unitary R)) → R ≃⋆ₐ[S] R) u : R ≃⋆ₐ[S] R) : (a : R) → R) a : R)) ↔
    ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₁ : (∀ (a : R), (↑v : R) * a * star (↑v : R) = (↑u : R) * a * star (↑u : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₂ :
  (∀ (a : R), (↑v : R) * a * (↑(star v) : R) = (↑u : R) * a * (↑(star u) : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
simp_rw₃ : (∀ (a : R), (↑v : R) * a * (↑v⁻¹ : R) = (↑u : R) * a * (↑u⁻¹ : R)) ↔ ∃ (α : S), (↑u : R) = α • (↑v : R)
⊢ 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)
have simp_rw₄ : (∀ (a : R),
    (↑v : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
      (↑u : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
  ∃ (α : S), (↑u : R) = α • (↑v : R)
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, Units.eq_inv_mul_iff_mul_eq, mul_smul_comm,
    mul_one, eq_comm]