awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have h_comp_adjoint : (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
  HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
Tactic: have h_comp_adjoint : y.toContinuousLinearMap ∘L adjoint y.toContinuousLinearMap =
      α • ContinuousLinearMap.id 𝕜 _ := by
    ext x
    simpa using congr(y (($hα ∘L y.symm.toContinuousLinearMap) x)).symm
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
⊢ β * β = α⁻¹
have rw : β * β = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)⁻¹
Tactic: rw [hα_re]
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have hβ : β * β = α⁻¹
Tactic: have hβ : β * β = α⁻¹ := by
    rw [hα_re]
    norm_num [β, ← RCLike.ofReal_mul, ← Real.rpow_add hα_pos, Real.rpow_neg_one]
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have h : f = U.conjStarAlgEquiv
Tactic: use U
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ β⁻¹ * β = 1
have refine : β ≠ 0
Tactic: refine inv_mul_cancel₀ ?_
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ β ≠ 0
have simp : ¬HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2)) = 0
Tactic: simp only [β, ne_eq, map_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
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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ ¬HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2)) = 0
have rw : ¬Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (0 : ℝ)
Tactic: rw [Real.rpow_eq_zero hα_pos.le (by simp)]
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ f = U.conjStarAlgEquiv
have hβ₂ : β⁻¹ * β = 1
Tactic: have hβ₂ : β⁻¹ * β = 1 := by
    refine inv_mul_cancel₀ ?_
    simp only [β, ne_eq, map_eq_zero]
    rw [Real.rpow_eq_zero hα_pos.le (by simp)]
    exact ne_of_gt hα_pos
-- 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_1 :
  ∀ (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))
α : 𝕜
hα :
  HSMul.hSMul (β := V →L[𝕜] V) α 1 =
    comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W)
this :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
h_comp_adjoint :
  (↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) =
    HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W)
β : 𝕜 := (↑(HPow.hPow (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ) (-(1 / 2))) : 𝕜)
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
hβ₂ : β⁻¹ * β = 1
⊢ f = U.conjStarAlgEquiv
have h : ∀ (a : V →L[𝕜] V) (x : W),
  Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) a : W →L[𝕜] W) : (a : W) → W) x : W)
    (((((U.conjStarAlgEquiv : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)) : (a : V →L[𝕜] V) → W →L[𝕜] W) a :
            W →L[𝕜] W) :
          (a : W) → W)
        x :
      W)
Tactic: ext
-- 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 : Type u_4
inst_7 : EquivLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (V →L[𝕜] V) (W →L[𝕜] W)
inst_8 : NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
inst_9 : StarHomClass.{u_4, u_2, u_3} F (V →L[𝕜] V) (W →L[𝕜] W)
inst_10 : ContinuousMapClass.{u_4, u_2, u_3} F (V →L[𝕜] V) (W →L[𝕜] W)
f : F
x y : V →L[𝕜] V
⊢ LE.le.{u_3} (α := W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) y : W →L[𝕜] W) ↔
    x ≤ y
have obtain : ∀ (U : V ≃ₗᵢ[𝕜] W)
  (hU :
    Eq (α := StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)) (↑f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W)
      U.conjStarAlgEquiv),
  LE.le.{u_3} (α := W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) y : W →L[𝕜] W) ↔
    x ≤ y
Tactic: obtain ⟨U, hU⟩ := StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv
      (StarAlgEquivClass.toStarAlgEquiv f : _ ≃⋆ₐ[𝕜] _) (map_continuous f)
-- 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 : Type u_4
inst_7 : EquivLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (V →L[𝕜] V) (W →L[𝕜] W)
inst_8 : NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
inst_9 : StarHomClass.{u_4, u_2, u_3} F (V →L[𝕜] V) (W →L[𝕜] W)
inst_10 : ContinuousMapClass.{u_4, u_2, u_3} F (V →L[𝕜] V) (W →L[𝕜] W)
f : F
x y : V →L[𝕜] V
U : V ≃ₗᵢ[𝕜] W
hU :
  Eq (α := StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)) (↑f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W)
    U.conjStarAlgEquiv
⊢ LE.le.{u_3} (α := W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) y : W →L[𝕜] W) ↔
    x ≤ y
have this : ∀ (a : V →L[𝕜] V),
  Eq.{u_3 + 1} (α := W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) a : W →L[𝕜] W)
    (((U.conjStarAlgEquiv : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)) : (a : V →L[𝕜] V) → W →L[𝕜] W) a :
      W →L[𝕜] W)
Tactic: have this a : f a = U.conjStarAlgEquiv a := by simpa using congr($hU a)
-- 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 : Type u_4
inst_7 : EquivLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (V →L[𝕜] V) (W →L[𝕜] W)
inst_8 : NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
inst_9 : StarHomClass.{u_4, u_2, u_3} F (V →L[𝕜] V) (W →L[𝕜] W)
inst_10 : ContinuousMapClass.{u_4, u_2, u_3} F (V →L[𝕜] V) (W →L[𝕜] W)
f : F
x y : V →L[𝕜] V
U : V ≃ₗᵢ[𝕜] W
hU :
  Eq (α := StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)) (↑f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W)
    U.conjStarAlgEquiv
this :
  ∀ (a : V →L[𝕜] V),
    Eq.{u_3 + 1} (α := W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) a : W →L[𝕜] W)
      (((U.conjStarAlgEquiv : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)) : (a : V →L[𝕜] V) → W →L[𝕜] W) a :
        W →L[𝕜] W)
⊢ LE.le.{u_3} (α := W →L[𝕜] W) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x : W →L[𝕜] W)
      ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) y : W →L[𝕜] W) ↔
    x ≤ y
have simp_rw : LinearMap.IsPositive.{u_1, u_3} (𝕜 := 𝕜) (E := W)
    (↑(((U.conjStarAlgEquiv : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)) : (a : V →L[𝕜] V) → W →L[𝕜] W)
          (y - x)) :
      W →ₗ[𝕜] W) ↔
  (↑(y - x) : V →ₗ[𝕜] V).IsPositive
Tactic: simp_rw [le_def, ← _root_.map_sub, ← isPositive_toLinearMap_iff, this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : SeminormedRing 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
| Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) x : E)
have rw : Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) (x * 1) : E)
Tactic: rw [← mul_one x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : SeminormedRing 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) x : E) ≤ Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E) * ‖x‖
have conv_lhs : Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) (x * 1) : E) ≤ Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E) * ‖x‖
Tactic: conv_lhs => rw [← mul_one x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : SeminormedRing 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) (x * 1) : E) ≤ Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E) * ‖x‖
have rw : ‖HSMul.hSMul (β := E) x ((f : (a : 𝕜) → E) 1 : E)‖ ≤ ‖x‖ * Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E)
Tactic: rw [← smul_eq_mul, f.map_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
y : F
⊢ Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
    a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E))
have rw : Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
  a⁻¹ * a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)
Tactic: rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
y : F
rw :
  Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
    a⁻¹ * a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)
⊢ Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
    a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E))
have rw₁ : Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) = 1 * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)
Tactic: rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]