awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Subsingleton V
pos : Subsingleton W → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
neg : Nontrivial W → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv

Tactic:
by_cases! Subsingleton W

Premises used: Subsingleton
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Subsingleton V
h_1 : Subsingleton W
x : V
⊢ norm.{u_3} (E := W) ((0 : (a : V) → W) x : W) = ‖x‖

Tactic:
simp [Subsingleton.eq_zero]

Premises used: Subsingleton.eq_zero
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h_1 : Subsingleton V
h_2 : Subsingleton W
h :
  f =
    LinearIsometryEquiv.conjStarAlgEquiv
      (let __LinearEquiv : V ≃ₗ[𝕜] W := 0;
      { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ })
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv

Tactic:
use { toLinearEquiv := 0, norm_map' _ := by simp [Subsingleton.eq_zero] }
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Subsingleton V
h_1 : Subsingleton W
⊢ f =
    LinearIsometryEquiv.conjStarAlgEquiv
      (let __LinearEquiv : V ≃ₗ[𝕜] W := 0;
      { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ })

Tactic:
ext fun _ ↦ Subsingleton.allEq _ _

Premises used: Norm.norm, congrArg, LinearIsometryEquiv.conjStarAlgEquiv, norm_zero, LinearIsometryEquiv.mk, Subsingleton.allEq, congr, eq_self, of_eq_true, Subsingleton.eq_zero, StarAlgEquiv.ext, OfNat.ofNat, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Subsingleton V
h_1 : Subsingleton W
⊢ f =
    LinearIsometryEquiv.conjStarAlgEquiv
      (let __LinearEquiv : V ≃ₗ[𝕜] W := 0;
      { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ })

Tactic:
exact ext fun _ ↦ Subsingleton.allEq _ _

Premises used: Subsingleton.allEq, StarAlgEquiv.ext, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Subsingleton V
h_1 : Nontrivial W
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv

Tactic:
simpa using congr(f $(Subsingleton.allEq 0 1))
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
neg :
  ∀ (y : V ≃L[𝕜] W)
    (hy :
      Eq (α := ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W))
        { toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } y.conjContinuousAlgEquiv),
    ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv

Tactic:
obtain ⟨y, hy⟩ := (ContinuousAlgEquiv.mk f.toAlgEquiv hf
    (f.toAlgEquiv.toLinearEquiv.continuous_symm hf)).eq_continuousLinearEquivConjContinuousAlgEquiv

Premises used: StarAlgEquiv.toAlgEquiv, ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv, LinearEquiv.continuous_symm, AlgEquiv.toLinearEquiv, ContinuousAlgEquiv.mk
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W))
    { toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } y.conjContinuousAlgEquiv
⊢ ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] W)
      ((adjoint : (a : W →L[𝕜] W) → W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W) : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) : W →L[𝕜] W)

Tactic:
have (x : V →L[𝕜] V) : adjoint (f x) = f (adjoint x) := map_star _ _ |>.symm
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W))
    { toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } y.conjContinuousAlgEquiv
this :
  ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] W)
      ((adjoint : (a : W →L[𝕜] W) → W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W) : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) : W →L[𝕜] W)
⊢ Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)

Tactic:
rw [ContinuousAlgEquiv.ext_iff] at hy

Premises used: ContinuousAlgEquiv.ext_iff
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W))
    { toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } y.conjContinuousAlgEquiv
this :
  ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] W)
      ((adjoint : (a : W →L[𝕜] W) → W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W) : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) : W →L[𝕜] W)
hy₁ :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
⊢ ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] W)
      ((adjoint : (a : W →L[𝕜] W) → W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W) : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) : W →L[𝕜] W)

Tactic:
rw [ContinuousAlgEquiv.ext_iff] at hy

Premises used: ContinuousAlgEquiv.ext_iff
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] W)
      ((adjoint : (a : W →L[𝕜] W) → W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W) : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) : W →L[𝕜] W)
⊢ ∀ (x : V →L[𝕜] V),
    comp.{u_1, u_1, u_1, u_3, u_2, u_3} (σ₁₂ := RingHom.id 𝕜) (M₂ := V)
        (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V)
          ((adjoint : (a : W →L[𝕜] V) → V →L[𝕜] W) (↑y.symm : W →L[𝕜] V)) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x))
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
      (↑y : V →L[𝕜] W) ∘SL comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)

Tactic:
simp_rw [← StarAlgEquiv.coe_toAlgEquiv, ContinuousAlgEquiv.coe_mk f.toAlgEquiv hf _ ▸ hy,
    conjContinuousAlgEquiv_apply,  adjoint_comp] at this

Premises used: StarAlgEquiv.coe_toAlgEquiv, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, ContinuousLinearMap.adjoint_comp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    comp.{u_1, u_1, u_1, u_3, u_2, u_3} (σ₁₂ := RingHom.id 𝕜) (M₂ := V)
        (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V)
          ((adjoint : (a : W →L[𝕜] V) → V →L[𝕜] W) (↑y.symm : W →L[𝕜] V)) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x))
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
      (↑y : V →L[𝕜] W) ∘SL comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)
x : V →L[𝕜] V
simp_rw :
  Eq (α := W →L[𝕜] V)
    ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) ((↑y : V →L[𝕜] W) ∘SL x ∘SL (↑y.symm : W →L[𝕜] V) ∘SL (↑y : V →L[𝕜] W)) :
      W →L[𝕜] V)
    ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) ((↑y : V →L[𝕜] W) ∘SL x) : W →L[𝕜] V)
⊢ Eq (α := W →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W))
      ((↑y : V →L[𝕜] W) ∘SL
        comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)))
    (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x)
      ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)))

Tactic:
simp_rw [← this x, ← comp_assoc, ← adjoint_comp]

Premises used: ContinuousLinearMap.comp_assoc, ContinuousLinearMap.adjoint_comp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    comp.{u_1, u_1, u_1, u_3, u_2, u_3} (σ₁₂ := RingHom.id 𝕜) (M₂ := V)
        (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V)
          ((adjoint : (a : W →L[𝕜] V) → V →L[𝕜] W) (↑y.symm : W →L[𝕜] V)) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x))
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
      (↑y : V →L[𝕜] W) ∘SL comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)
x : V →L[𝕜] V
⊢ Eq (α := W →L[𝕜] V)
    ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) ((↑y : V →L[𝕜] W) ∘SL x ∘SL (↑y.symm : W →L[𝕜] V) ∘SL (↑y : V →L[𝕜] W)) :
      W →L[𝕜] V)
    ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) ((↑y : V →L[𝕜] W) ∘SL x) : W →L[𝕜] V)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    comp.{u_1, u_1, u_1, u_3, u_2, u_3} (σ₁₂ := RingHom.id 𝕜) (M₂ := V)
        (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V)
          ((adjoint : (a : W →L[𝕜] V) → V →L[𝕜] W) (↑y.symm : W →L[𝕜] V)) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x))
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
      (↑y : V →L[𝕜] W) ∘SL comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)
⊢ ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W))
        ((↑y : V →L[𝕜] W) ∘SL
          comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)))
      (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x)
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)))

Tactic:
replace this (x : V →L[𝕜] V) : adjoint y.toContinuousLinearMap ∘L y ∘L adjoint x ∘L y.symm =
      adjoint x ∘L adjoint y.toContinuousLinearMap := by
    simp_rw [← this x, ← comp_assoc, ← adjoint_comp]
    simp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W))
        ((↑y : V →L[𝕜] W) ∘SL
          comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)))
      (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x)
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)))
x : V →L[𝕜] V
simp_rw :
  Eq (α := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W))
      ((↑y : V →L[𝕜] W) ∘SL x ∘SL (↑y.symm : W →L[𝕜] V) ∘SL (↑y : V →L[𝕜] W)))
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) ((↑y : V →L[𝕜] W) ∘SL x))
⊢ Commute x (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))

Tactic:
simp_rw [commute_iff_eq, mul_def, ← comp_assoc, ← (adjoint_adjoint x ▸ this _), comp_assoc]

Premises used: commute_iff_eq, ContinuousLinearMap.comp_assoc, ContinuousLinearMap.mul_def
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W))
        ((↑y : V →L[𝕜] W) ∘SL
          comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)))
      (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x)
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)))
x : V →L[𝕜] V
⊢ Eq (α := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W))
      ((↑y : V →L[𝕜] W) ∘SL x ∘SL (↑y.symm : W →L[𝕜] V) ∘SL (↑y : V →L[𝕜] W)))
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) ((↑y : V →L[𝕜] W) ∘SL x))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    Eq (α := W →L[𝕜] V)
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W))
        ((↑y : V →L[𝕜] W) ∘SL
          comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x) (↑y.symm : W →L[𝕜] V)))
      (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := V) ((adjoint : (a : V →L[𝕜] V) → V →L[𝕜] V) x)
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)))
⊢ ∀ (x : V →L[𝕜] V),
    Commute x (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))

Tactic:
replace this (x : V →L[𝕜] V) : Commute x (adjoint y.toContinuousLinearMap ∘L y) := by
    simp_rw [commute_iff_eq, mul_def, ← comp_assoc, ← (adjoint_adjoint x ▸ this _), comp_assoc]
    simp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    Commute x (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
⊢ Membership.mem (γ := Subalgebra 𝕜 (V →L[𝕜] V)) ⊥
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))

Tactic:
simpa using (Subalgebra.mem_center_iff (R := 𝕜)).mpr fun _ ↦ this _

Premises used: Iff.mpr, Subalgebra.mem_center_iff
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this :
  ∀ (x : V →L[𝕜] V),
    Commute x (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
neg :
  ∀ (α : 𝕜)
    (hα :
      Eq.{u_2 + 1} (α := V →L[𝕜] V)
        ((AlgHom.toRingHom (Algebra.ofId 𝕜 (V →L[𝕜] V)) : (a : 𝕜) → V →L[𝕜] V) α : V →L[𝕜] V)
        (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W) :
          V →L[𝕜] V)),
    ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv

Tactic:
obtain ⟨α, hα⟩ := by simpa using (Subalgebra.mem_center_iff (R := 𝕜)).mpr fun _ ↦ this _