-- 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)
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)
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)
simp_rw₅ :
  (∀ (a : R),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₆ :
  (∀ (a : R),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R))) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₇ :
  (∀ (a : R),
      a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) *
          ((↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * (a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)))) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₈ :
  (∀ (a : R),
      a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) =
        HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
              (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) *
            a *
          (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u)⁻¹ : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₉ :
  (∀ (a : R),
      a * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) * (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
            (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) *
          a) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₀ :
  (∀ (a : R),
      a *
          HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
            (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R) * ((↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) * a)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₁ :
  (∀ (a : R),
      a *
          HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
            (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
            (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) *
          a) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₂ :
  Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R)
      (HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₃ :
  Membership.mem (γ := Subalgebra S R) ⊥
      (HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₄ :
  Membership.mem (γ := Set R) (Set.range.{u_2, u_3 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R))
      (HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₅ :
  (∃ (y : S),
      (algebraMap S R : (a : S) → R) y =
        HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
          (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₆ :
  (∃ (y : S),
      HSMul.hSMul (β := R) y 1 =
        HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v)⁻¹ : R)
          (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₇ :
  (∃ (y : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) * HSMul.hSMul (β := R) y 1 =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₈ :
  (∃ (y : S),
      y • HMul.hMul (α := R) (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) 1 =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R)
simp_rw₁₉ :
  (∃ (y : S),
      HSMul.hSMul (β := R) y (↑((toUnits : (a : ↥(unitary R)) → Rˣ) v) : R) =
        (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R)) ↔
    ∃ (α : S),
      (↑((toUnits : (a : ↥(unitary R)) → Rˣ) u) : R) =
        HSMul.hSMul (β := R) α (↑((toUnits : (a : ↥(unitary R)) → 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)

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]

Premises used: Units.val, Set.mem_range, Subalgebra.mem_center_iff, Algebra.mem_bot, Unitary.toUnits, mul_assoc, eq_comm, 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, mul_smul_comm, Unitary.star_eq_inv, mul_one, DFunLike.coe, Unitary.coe_star, Units.eq_inv_mul_iff_mul_eq