awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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))
⊢ Continuous.{u_3, u_2} (X := W) (Y := V) (⇑(↑Tₗ.symm : W →ₗ[𝕜] V) : (a : W) → V)
have suffices : (↑T' : W →ₗ[𝕜] V) = (↑Tₗ.symm : W →ₗ[𝕜] V)
Tactic: suffices T'.toLinearMap = Tₗ.symm from this ▸ T'.continuous
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
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
⊢ ((↑(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
have 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
Tactic: have := by simpa using congr($he x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
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 : 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
have 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
Tactic: have := by simpa using congr($he' x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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 : 𝕜) → 𝕜) α' = α'
⊢ ∀ (x : V), norm.{u_3} (E := W) (((↑(auxContinuousLinearEquiv e hα hα2 he he') : V ≃ₗ[𝕜] W) : (a : V) → W) x : W) = ‖x‖
have 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
Tactic: rw [ContinuousLinearEquiv.coe_toLinearEquiv, ← ContinuousLinearEquiv.coe_coe,
      norm_map_iff_adjoint_comp_self, coe_auxContinuousLinearEquiv,
      MulActionSemiHomClass.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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 (α := 𝕜) (β := 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
have 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
Tactic: simp only [hαa, comp_smulₛₗ, RingHom.id_apply, smul_comp, smul_smul, hα2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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).symm : W →L[𝕜] V) = α'⁻¹ • (↑e.symm : W →L[𝕜] V)
have 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)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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_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)
have 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)
Tactic: apply (auxIsometry e hα hα2 he he' hαa).toContinuousLinearEquiv.injective
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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)
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have pos : Subsingleton V → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
Tactic: by_cases! Subsingleton V
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have neg : Nontrivial V → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
Tactic: by_cases! Subsingleton V
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have pos : Subsingleton W → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
Tactic: by_cases! Subsingleton W
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have neg : Nontrivial W → ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
Tactic: by_cases! Subsingleton W
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have h : f =
  LinearIsometryEquiv.conjStarAlgEquiv
    (let __LinearEquiv : V ≃ₗ[𝕜] W := 0;
    { toLinearEquiv := __LinearEquiv, norm_map' := sorry })
Tactic: use { toLinearEquiv := 0, norm_map' _ := by simp [Subsingleton.eq_zero] }
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have 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 := sorry } y.conjContinuousAlgEquiv),
  ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
Tactic: obtain ⟨y, hy⟩ := (ContinuousAlgEquiv.mk f.toAlgEquiv hf
    (f.toAlgEquiv.toLinearEquiv.continuous_symm hf)).eq_continuousLinearEquivConjContinuousAlgEquiv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
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
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have 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)
Tactic: have (x : V →L[𝕜] V) : adjoint (f x) = f (adjoint x) := map_star _ _ |>.symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
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)
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have hy₁ : Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
  (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := sorry } : (a : V →L[𝕜] V) → W →L[𝕜] W)
  (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
Tactic: rw [ContinuousAlgEquiv.ext_iff] at hy
Cleared hypotheses: hy, this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
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)
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have 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)
Tactic: simp_rw [← StarAlgEquiv.coe_toAlgEquiv, ContinuousAlgEquiv.coe_mk f.toAlgEquiv hf _ ▸ hy,
    conjContinuousAlgEquiv_apply,  adjoint_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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)))
have 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)
Tactic: simp_rw [← this x, ← comp_assoc, ← adjoint_comp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
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)
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have 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)))
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
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))
have 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))
Tactic: simp_rw [commute_iff_eq, mul_def, ← comp_assoc, ← (adjoint_adjoint x ▸ this _), comp_assoc]