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 : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
Tₗ : V ≃ₗ[𝕜] W := LinearEquiv.ofBijective (↑T : V →ₗ[𝕜] W) ⋯
T' : W →L[𝕜] V :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' V (RingHom.id 𝕜) : (a : V) → (V →L[𝕜] V) →L[𝕜] V) u)
    ((↑f.symm : (W →L[𝕜] W) →A[𝕜] V →L[𝕜] V).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 W W : (a : StrongDual 𝕜 W) → W →L[𝕜] W →L[𝕜] W) d))
⊢ (↑T' : W →ₗ[𝕜] V) = (↑Tₗ.symm : W →ₗ[𝕜] V)

Tactic:
simp [LinearMap.ext_iff, ← Tₗ.injective.eq_iff, T', this, hT, hd, Tₗ]

Premises used: Function.Injective.eq_iff, LinearMap.ext_iff, LinearEquiv.injective
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
Tₗ : V ≃ₗ[𝕜] W := LinearEquiv.ofBijective (↑T : V →ₗ[𝕜] W) ⋯
T' : W →L[𝕜] V :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' V (RingHom.id 𝕜) : (a : V) → (V →L[𝕜] V) →L[𝕜] V) u)
    ((↑f.symm : (W →L[𝕜] W) →A[𝕜] V →L[𝕜] V).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 W W : (a : StrongDual 𝕜 W) → W →L[𝕜] W →L[𝕜] W) d))
TL : V ≃L[𝕜] W := { toLinearEquiv := Tₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x

Tactic:
⟨TL, fun A ↦ (ContinuousLinearMap.ext <| this A).symm⟩

Premises used: Exists.intro, Eq.symm, ContinuousLinearMap.ext
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
Tₗ : V ≃ₗ[𝕜] W := LinearEquiv.ofBijective (↑T : V →ₗ[𝕜] W) ⋯
T' : W →L[𝕜] V :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' V (RingHom.id 𝕜) : (a : V) → (V →L[𝕜] V) →L[𝕜] V) u)
    ((↑f.symm : (W →L[𝕜] W) →A[𝕜] V →L[𝕜] V).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 W W : (a : StrongDual 𝕜 W) → W →L[𝕜] W →L[𝕜] W) d))
TL : V ≃L[𝕜] W := { toLinearEquiv := Tₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x

Tactic:
exact ⟨TL, fun A ↦ (ContinuousLinearMap.ext <| this A).symm⟩
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
⊢ Function.Surjective (α := V ≃L[𝕜] W) (β := ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W))
    conjContinuousAlgEquiv

Tactic:
fun f ↦ f.eq_continuousLinearEquivConjContinuousAlgEquiv.imp fun _ h ↦ h.symm

Premises used: Exists.imp, ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv, Function.Surjective
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
x : V
⊢ (((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) : (a : W) → V) ((e : (a : V) → W) x : W) =
    α • x

Tactic:
simpa using congr($he x)
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
x : V
⊢ (((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) : (a : W) → V) ((e : (a : V) → W) x : W) =
    α • x

Tactic:
have := by simpa using congr($he x)
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
x : V
this :
  (((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) : (a : W) → V) ((e : (a : V) → W) x : W) =
    α • x
⊢ ((↑(HSMul.hSMul (β := W →L[𝕜] V) α' ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V)) :
          W →ₗ[𝕜] V) :
        (a : W) → V)
      ((↑(α' • (↑e : V →L[𝕜] W)) : V →ₗ[𝕜] W).toFun x) =
    x

Tactic:
simp [smul_smul, hα2, this, hα, ← mul_assoc]

Premises used: mul_assoc, smul_smul
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
x : W
⊢ (e : (a : V) → W) ((((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) : (a : W) → V) x : V) =
    α • x

Tactic:
simpa using congr($he' x)
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
x : W
⊢ (e : (a : V) → W) ((((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) : (a : W) → V) x : V) =
    α • x

Tactic:
have := by simpa using congr($he' x)
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
x : W
this :
  (e : (a : V) → W) ((((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) : (a : W) → V) x : V) =
    α • x
⊢ (↑(α' • (↑e : V →L[𝕜] W)) : V →ₗ[𝕜] W).toFun
      (((↑(HSMul.hSMul (β := W →L[𝕜] V) α' ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V)) :
            W →ₗ[𝕜] V) :
          (a : W) → V)
        x) =
    x

Tactic:
simp [smul_smul, hα2, this, hα, ← mul_assoc]

Premises used: mul_assoc, smul_smul
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
⊢ (↑(auxContinuousLinearEquiv e hα hα2 he he') : V →L[𝕜] W) = α' • (↑e : V →L[𝕜] W)

Tactic:
rfl

Premises used: rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
rw :
  HSMul.hSMul (α := 𝕜) (β := W →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' : 𝕜)
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) ∘SL
      (α' • (↑e : V →L[𝕜] W)) =
    1
⊢ ∀ (x : V), norm.{u_3} (E := W) (((↑(auxContinuousLinearEquiv e hα hα2 he he') : V ≃ₗ[𝕜] W) : (a : V) → W) x : W) = ‖x‖

Tactic:
rw [ContinuousLinearEquiv.coe_toLinearEquiv, ← ContinuousLinearEquiv.coe_coe,
      norm_map_iff_adjoint_comp_self, coe_auxContinuousLinearEquiv,
      MulActionSemiHomClass.map_smulₛₗ]

Premises used: _private.0.coe_auxContinuousLinearEquiv, MulActionSemiHomClass.map_smulₛₗ, ContinuousLinearEquiv.coe_toLinearEquiv, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, ContinuousLinearEquiv.coe_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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
simp :
  HSMul.hSMul (β := V →L[𝕜] V) α⁻¹
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W)) =
    1
⊢ HSMul.hSMul (α := 𝕜) (β := W →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' : 𝕜)
        ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W) : W →L[𝕜] V) ∘SL
      (α' • (↑e : V →L[𝕜] W)) =
    1

Tactic:
simp only [hαa, comp_smulₛₗ, RingHom.id_apply, smul_comp, smul_smul, hα2]

Premises used: RingHom.id_apply, ContinuousLinearMap.smul_comp, smul_smul, ContinuousLinearMap.comp_smulₛₗ
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
⊢ HSMul.hSMul (β := V →L[𝕜] V) α⁻¹
      (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W)) =
    1

Tactic:
simp [he, smul_smul, hα, one_def]

Premises used: smul_smul, ContinuousLinearMap.one_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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
⊢ (↑(↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W) : V →L[𝕜] W) = α' • (↑e : V →L[𝕜] W)

Tactic:
rfl

Premises used: rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
h :
  ∀ (y : W),
    Eq.{u_2 + 1} (α := V) (((↑(↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W).symm : W →L[𝕜] V) : (a : W) → V) y : V)
      ((α'⁻¹ • (↑e.symm : W →L[𝕜] V) : (a : W) → V) y : V)
⊢ (↑(↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W).symm : W →L[𝕜] V) = α'⁻¹ • (↑e.symm : W →L[𝕜] V)

Tactic:
ext y
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
y : W
h :
  Eq.{u_3 + 1} (α := W)
    (((↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W) : (a : V) → W)
        (((↑(↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W).symm : W →L[𝕜] V) : (a : W) → V) y : V) :
      W)
    (((↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W) : (a : V) → W)
        ((α'⁻¹ • (↑e.symm : W →L[𝕜] V) : (a : W) → V) y : V) :
      W)
⊢ Eq.{u_2 + 1} (α := V) (((↑(↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W).symm : W →L[𝕜] V) : (a : W) → V) y : V)
    ((α'⁻¹ • (↑e.symm : W →L[𝕜] V) : (a : W) → V) y : V)

Tactic:
apply (auxIsometry e hα hα2 he he' hαa).toContinuousLinearEquiv.injective

Premises used: ContinuousLinearEquiv.injective, LinearIsometryEquiv.toContinuousLinearEquiv, _private.0.auxIsometry
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
y : W
⊢ α' ≠ 0

Tactic:
grind
-- 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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he :
  comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) (↑e : V →L[𝕜] W) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
he' :
  (↑e : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑e : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
hαa : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α' = α'
y : W
⊢ Eq.{u_3 + 1} (α := W)
    (((↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W) : (a : V) → W)
        (((↑(↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W).symm : W →L[𝕜] V) : (a : W) → V) y : V) :
      W)
    (((↑(auxIsometry e hα hα2 he he' hαa) : V ≃L[𝕜] W) : (a : V) → W)
        ((α'⁻¹ • (↑e.symm : W →L[𝕜] V) : (a : W) → V) y : V) :
      W)

Tactic:
simp [smul_smul, inv_mul_cancel₀ (a := α') (by grind)]

Premises used: smul_smul, inv_mul_cancel₀
-- 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)
pos : Subsingleton V → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
neg : Nontrivial V → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv

Tactic:
by_cases! Subsingleton V

Premises used: Subsingleton