awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : 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)
⊢ 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α

Premises used: Algebra.toRingHom_ofId, Algebra.algebraMap_eq_smul_one, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : 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α :
  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)
⊢ comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W) *
        (↑y.symm : W →L[𝕜] V).comp (σ₁₂ := RingHom.id 𝕜)
          ((adjoint : (a : W →L[𝕜] V) → V →L[𝕜] W) (↑y.symm : W →L[𝕜] V)) =
      1 ∧
    (↑y.symm : W →L[𝕜] V).comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : W →L[𝕜] V) → V →L[𝕜] W) (↑y.symm : W →L[𝕜] V)) *
        comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : V →L[𝕜] W) → W →L[𝕜] V) (↑y : V →L[𝕜] W)) (↑y : V →L[𝕜] W) =
      1

Tactic:
simp [mul_def, ← comp_assoc, comp_assoc _ _ (adjoint y.toContinuousLinearMap),
        ← adjoint_comp, one_def, comp_assoc _ y.toContinuousLinearMap]

Premises used: ContinuousLinearMap.adjoint, ContinuousLinearMap.comp_assoc, ContinuousLinearMap.adjoint_comp, ContinuousLinearMap.mul_def, DFunLike.coe, ContinuousLinearMap.one_def, 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
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))
⊢ HSMul.hSMul (α := 𝕜) (β := V →L[𝕜] V) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) α : 𝕜) (ContinuousLinearMap.id 𝕜 V) =
    HSMul.hSMul (β := V →L[𝕜] V) α (ContinuousLinearMap.id 𝕜 V)

Tactic:
simpa [IsSelfAdjoint, ← hα, one_def, star_eq_adjoint] using
      (IsSelfAdjoint.one (W →L[𝕜] W)).adjoint_conj y.toContinuousLinearMap

Premises used: IsSelfAdjoint, ContinuousLinearMap, ContinuousLinearMap.star_eq_adjoint, IsSelfAdjoint.adjoint_conj, RingHom.id, IsSelfAdjoint.one, ContinuousLinearMap.one_def, 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
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))
⊢ 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
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this_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 : 𝕜) → ℝ) α) : 𝕜)
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : α = (↑((RCLike.re : (a : 𝕜) → ℝ) α) : 𝕜)), α = (↑((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

Premises used: Function.Injective.eq_iff, RCLike.conj_eq_iff_re, smul_left_injective, eq_comm, one_ne_zero, 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
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 : 𝕜) → ℝ) α) : 𝕜)

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
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h_1 : 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 : α = 0
⊢ False

Tactic:
simp [h, ← hα] at this
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this_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 : 𝕜) → ℝ) α) : 𝕜)
⊢ α ≠ 0

Tactic:
have hα_ne_zero : α ≠ 0 := fun h ↦ by simp [h, ← hα] at this
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this_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 ≤ HSMul.hSMul (β := V →L[𝕜] V) α 1

Tactic:
have := hα_re.symm ▸ (nonneg_iff_isPositive _ |>.mpr
      (hα_re ▸ hα ▸ isPositive_adjoint_comp_self y.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
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
rw : (HSMul.hSMul (β := V →ₗ[𝕜] V) α 1).IsPositive
⊢ 0 ≤ α

Tactic:
rw [← LinearMap.isPositive_one.isPositive_smul_iff (E := V) (one_ne_zero' (V →ₗ[𝕜] V))]

Premises used: one_ne_zero', LinearMap.IsPositive.isPositive_smul_iff, LinearMap, RingHom.id, LinearMap.isPositive_one
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this_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
⊢ (HSMul.hSMul (β := V →ₗ[𝕜] V) α 1).IsPositive

Tactic:
(nonneg_iff_isPositive _).mp this

Premises used: ContinuousLinearMap.IsPositive, ContinuousLinearMap.nonneg_iff_isPositive, ContinuousLinearMap.reApplyInnerSelf, LinearMap.IsPositive, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this_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
⊢ (HSMul.hSMul (β := V →ₗ[𝕜] V) α 1).IsPositive

Tactic:
exact (nonneg_iff_isPositive _).mp this

Premises used: ContinuousLinearMap.nonneg_iff_isPositive, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this_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 ≤ α

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
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h : Nontrivial V
y : V ≃L[𝕜] W
hy :
  Eq (α := (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } : (a : V →L[𝕜] V) → W →L[𝕜] W)
    (⇑y.conjContinuousAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W)
this_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 ≤ α
⊢ 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)
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
f : StarAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hf : Continuous.{u_2, u_3} (X := V →L[𝕜] V) (Y := W →L[𝕜] W) (⇑f : (a : V →L[𝕜] V) → W →L[𝕜] W)
h_1 : 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 :
  ∀ (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)
⊢ (↑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:
ext x