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_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

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
-- 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_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
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)
⊢ f = U.conjStarAlgEquiv

Tactic:
ext
-- 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 ≤ α
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
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:
simp [U.conjStarAlgEquiv_apply, U, smul_smul, hβ₂, ← conjContinuousAlgEquiv_apply, ← hy]

Premises used: LinearIsometryEquiv.conjStarAlgEquiv_apply, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, smul_smul
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
inst_4 : NormedAddCommGroup W
inst_5 : InnerProductSpace 𝕜 W
inst_6 : CompleteSpace W
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
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
⊢ 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)

Premises used: StarAlgEquivClass.toStarAlgEquiv, StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv, ContinuousMapClass.map_continuous
-- 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 : 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
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:
simpa using congr($hU a)
-- 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 : 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
⊢ ∀ (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)
-- 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 : 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)
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
⊢ 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:
simp_rw [le_def, ← _root_.map_sub, ← isPositive_toLinearMap_iff, this]

Premises used: map_sub, ContinuousLinearMap.isPositive_toLinearMap_iff, ContinuousLinearMap.le_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 : 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)
⊢ 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:
LinearMap.isPositive_linearIsometryEquiv_conj_iff U

Premises used: LinearMap.isPositive_linearIsometryEquiv_conj_iff
-- 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 : 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)
⊢ 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:
exact LinearMap.isPositive_linearIsometryEquiv_conj_iff U

Premises used: LinearMap.isPositive_linearIsometryEquiv_conj_iff
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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
σ : 𝕜 →+* 𝕜₂
f : E → F
h_add : ∀ (x y : E), f (x + y) = f x + f y
h_smul : ∀ (c : 𝕜) (x : E), f (c • x) = HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜₂) ((σ : (a : 𝕜) → 𝕜₂) c : 𝕜₂) (f x)
C : ℝ
h_bound : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
⊢ Continuous f

Tactic:
let φ : E →ₛₗ[σ] F :=
    { toFun := f
      map_add' := h_add
      map_smul' := h_smul }
  AddMonoidHomClass.continuous_of_bound φ C h_bound

Premises used: AddMonoidHomClass.continuous_of_bound, LinearMap.mk, AddHom.mk
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_3
G : Type u_5
inst : Ring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup G
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 G
f : E → G
h_add : ∀ (x y : E), f (x + y) = f x + f y
h_smul : ∀ (c : 𝕜) (x : E), f (c • x) = c • f x
C : ℝ
h_bound : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
⊢ Continuous f

Tactic:
let φ : E →ₗ[𝕜] G :=
    { toFun := f
      map_add' := h_add
      map_smul' := h_smul }
  AddMonoidHomClass.continuous_of_bound φ C h_bound

Premises used: AddMonoidHomClass.continuous_of_bound, LinearMap.mk, AddHom.mk
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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
σ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ] F
C : ℝ
h : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ (↑(f.mkContinuous C h) : E →ₛₗ[σ] F) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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
σ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ] F
C : ℝ
h : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
x : E
⊢ Eq.{u_4 + 1} (α := F) ((f.mkContinuous C h : (a : E) → F) x : F) ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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
σ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ] F
h : ∃ (C : ℝ), ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ (↑(f.mkContinuousOfExistsBound h) : E →ₛₗ[σ] F) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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
σ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ] F
h : ∃ (C : ℝ), ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
x : E
⊢ Eq.{u_4 + 1} (α := F) ((f.mkContinuousOfExistsBound h : (a : E) → F) x : F) ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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
σ : 𝕜 →+* 𝕜₂
f : E →SL[σ] F
K : ℝ≥0
h : ∀ (x : E), ‖x‖ ≤ (↑K : ℝ) * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F)
⊢ AntilipschitzWith.{u_3, u_4} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
AddMonoidHomClass.antilipschitz_of_bound _ h

Premises used: AddMonoidHomClass.antilipschitz_of_bound
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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
σ : 𝕜 →+* 𝕜₂
f : E →SL[σ] F
K : ℝ≥0
h : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) K (⇑f : (a : E) → F)
x : E
⊢ ‖x‖ ≤ (↑K : ℝ) * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F)

Tactic:
ZeroHomClass.bound_of_antilipschitz _ h x

Premises used: ZeroHomClass.bound_of_antilipschitz
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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 : 𝕜
rw : Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) (x * 1) : E)
| Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) x : E)

Tactic:
rw [← mul_one x]

Premises used: mul_one
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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 : 𝕜
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‖
⊢ Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) x : E) ≤ Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E) * ‖x‖

Tactic:
conv_lhs => rw [← mul_one x]

Premises used: mul_one
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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 : 𝕜
rw : ‖HSMul.hSMul (β := E) x ((f : (a : 𝕜) → E) 1 : E)‖ ≤ ‖x‖ * Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E)
⊢ 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:
rw [← smul_eq_mul, f.map_smul, mul_comm]

Premises used: LinearMap.map_smul, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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 : 𝕜
⊢ ‖HSMul.hSMul (β := E) x ((f : (a : 𝕜) → E) 1 : E)‖ ≤ ‖x‖ * Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E)

Tactic:
norm_smul_le _ _

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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 : 𝕜
⊢ ‖HSMul.hSMul (β := E) x ((f : (a : 𝕜) → E) 1 : E)‖ ≤ ‖x‖ * Norm.norm.{u_3} (E := E) ((f : (a : 𝕜) → E) 1 : E)

Tactic:
exact norm_smul_le _ _

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
⊢ (↑f.toContinuousLinearMap₁ : 𝕜 →ₗ[𝕜] E) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ Eq.{u_3 + 1} (α := E) ((f.toContinuousLinearMap₁ : (a : 𝕜) → E) x : E) ((f : (a : 𝕜) → E) x : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f : E →SL[σ] F
K : ℝ≥0
hf : ∀ (x : E), ‖x‖ ≤ (↑K : ℝ) * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F)
⊢ IsUniformEmbedding.{u_3, u_4} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
(AddMonoidHomClass.antilipschitz_of_bound f hf).isUniformEmbedding f.uniformContinuous

Premises used: AntilipschitzWith.isUniformEmbedding, ContinuousLinearMap.uniformContinuous, AddMonoidHomClass.antilipschitz_of_bound
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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)
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)
rw₂ rw₃ :
  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)
⊢ 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]

Premises used: mul_assoc, Ne.symm, ne_of_lt, inv_mul_cancel₀, one_mul
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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 rw₁ :
  a⁻¹ * (a * 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))
⊢ a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)) =
    a⁻¹ * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F)

Tactic:
rw [hf]