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 :
  ∀ (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)))
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have 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))
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
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),
    Commute x (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have 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
Tactic: obtain ⟨α, hα⟩ := by simpa using (Subalgebra.mem_center_iff (R := 𝕜)).mpr fun _ ↦ 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),
    Commute x (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
α : 𝕜
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
have 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)
Tactic: simp only [AlgHom.toRingHom_eq_coe, Algebra.toRingHom_ofId, Algebra.algebraMap_eq_smul_one] at hα
Cleared hypotheses: hα
-- 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))
⊢ α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
have this₁ : HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) (ContinuousLinearMap.id 𝕜 V) =
  HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
Tactic: have := by simpa [IsSelfAdjoint, ← hα, one_def, star_eq_adjoint] using
      (IsSelfAdjoint.one (W →L[𝕜] W)).adjoint_conj y.toContinuousLinearMap
-- 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_2 :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
this :
  HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) (ContinuousLinearMap.id 𝕜 V) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
⊢ α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
have rwa : ∀
  (this :
    HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) 1 = HSMul.hSMul (β := V →L[𝕜] V) α 1),
  α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
Tactic: rwa [← one_def, (smul_left_injective 𝕜 one_ne_zero).eq_iff, RCLike.conj_eq_iff_re,
      eq_comm] 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_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_2 :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
this :
  HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) (ContinuousLinearMap.id 𝕜 V) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
rwa :
  ∀
    (this :
      HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) 1 = HSMul.hSMul (β := V →L[𝕜] V) α 1),
    α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
⊢ α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
have rwa₁ : ∀ (this : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α = α), α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
Tactic: rwa [← one_def, (smul_left_injective 𝕜 one_ne_zero).eq_iff, RCLike.conj_eq_iff_re,
      eq_comm] 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_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_2 :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
this :
  HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) (ContinuousLinearMap.id 𝕜 V) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
rwa :
  ∀
    (this :
      HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) 1 = HSMul.hSMul (β := V →L[𝕜] V) α 1),
    α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
rwa₁ : ∀ (this : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α = α), α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
⊢ α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
have rwa₂ : ∀ (this : (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜) = α), α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
Tactic: rwa [← one_def, (smul_left_injective 𝕜 one_ne_zero).eq_iff, RCLike.conj_eq_iff_re,
      eq_comm] 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_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_2 :
  IsUnit (M := V →L[𝕜] V)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W))
this :
  HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) (ContinuousLinearMap.id 𝕜 V) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)
rwa :
  ∀
    (this :
      HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) 1 = HSMul.hSMul (β := V →L[𝕜] V) α 1),
    α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
rwa₁ : ∀ (this : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α = α), α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
rwa₂ : ∀ (this : (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜) = α), α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
⊢ α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
have rwa₃ : ∀ (this : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)), α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
Tactic: rwa [← one_def, (smul_left_injective 𝕜 one_ne_zero).eq_iff, RCLike.conj_eq_iff_re,
      eq_comm] at this
Cleared hypotheses: 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_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))
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have hα_re : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)
Tactic: have hα_re : α = RCLike.re α := by
    have := by simpa [IsSelfAdjoint, ← hα, one_def, star_eq_adjoint] using
      (IsSelfAdjoint.one (W →L[𝕜] W)).adjoint_conj y.toContinuousLinearMap
    rwa [← one_def, (smul_left_injective 𝕜 one_ne_zero).eq_iff, RCLike.conj_eq_iff_re,
      eq_comm] at 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_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 : 𝕜) → ℝ) α) : 𝕜)
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have hα_ne_zero : α ≠ 0
Tactic: have hα_ne_zero : α ≠ 0 := fun h ↦ by simp [h, ← hα] at 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_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
⊢ 0 ≤ α
have this₁ : 0 ≤ HSMul.hSMul (β := V →L[𝕜] V) α 1
Tactic: have := hα_re.symm ▸ (nonneg_iff_isPositive _ |>.mpr
      (hα_re ▸ hα ▸ isPositive_adjoint_comp_self y.toContinuousLinearMap))
-- 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_2 :
  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
this : 0 ≤ HSMul.hSMul (β := V →L[𝕜] V) α 1
⊢ 0 ≤ α
have rw : (HSMul.hSMul (β := V →ₗ[𝕜] V) α 1).IsPositive
Tactic: rw [← LinearMap.isPositive_one.isPositive_smul_iff (E := V) (one_ne_zero' (V →ₗ[𝕜] V))]
-- 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
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have hα_nonneg : 0 ≤ α
Tactic: have hα_nonneg : 0 ≤ α := by
    have := hα_re.symm ▸ (nonneg_iff_isPositive _ |>.mpr
      (hα_re ▸ hα ▸ isPositive_adjoint_comp_self y.toContinuousLinearMap))
    rw [← LinearMap.isPositive_one.isPositive_smul_iff (E := V) (one_ne_zero' (V →ₗ[𝕜] V))]
    exact (nonneg_iff_isPositive _).mp 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_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 ≤ α
⊢ ∃ (U : V ≃ₗᵢ[𝕜] W), f = U.conjStarAlgEquiv
have hα_pos : LT.lt (α := ℝ) (0 : ℝ) ((RCLike.re : (a : 𝕜) → ℝ) α : ℝ)
Tactic: have hα_pos := RCLike.ofReal_pos.mp <| hα_re ▸ (lt_of_le_of_ne' hα_nonneg hα_ne_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 : 𝕜) → ℝ) α : ℝ)
⊢ (↑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)
have h : ∀ (x : W),
  Eq (α := W)
    (((↑y : V →L[𝕜] W).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) :
          (a : W) → W)
        x :
      W)
    ((HSMul.hSMul (β := W →L[𝕜] W) α (ContinuousLinearMap.id 𝕜 W) : (a : W) → W) x : W)
Tactic: ext x