awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : AddCommGroup F
inst_5 : NormedAddCommGroup Fₗ
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 Eₗ
inst_8 : IsBoundedSMul 𝕜 Eₗ
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₂ Fₗ
inst_11 : IsBoundedSMul 𝕜₂ Fₗ
inst_12 : CompleteSpace Eₗ
inst_13 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_14 : RingHomInvPair σ₁₂ σ₂₁
inst_15 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_norm₁ :
  ∃ (C : ℝ),
    ∀ (x : E),
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) ≤
        C * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm₂ :
  ∃ (C : ℝ),
    ∀ (x : F),
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) ≤
        C * norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ Continuous (Y := Eₗ) fun (x : Eₗ) ↦
    ((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
          Fₗ →SL[σ₂₁] Eₗ) :
        (a : Fₗ) → Eₗ)
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁) :
            Eₗ →ₛₗ[σ₁₂] Fₗ))
        x)
have simp : Continuous (Y := Eₗ) fun (x : Eₗ) ↦
  ((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ : Fₗ →SL[σ₂₁] Eₗ) :
      (a : Fₗ) → Eₗ)
    (((LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁ : Eₗ →SL[σ₁₂] Fₗ) :
          (a : Eₗ) → Fₗ)
        x :
      Fₗ)
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : AddCommGroup F
inst_5 : NormedAddCommGroup Fₗ
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 Eₗ
inst_8 : IsBoundedSMul 𝕜 Eₗ
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₂ Fₗ
inst_11 : IsBoundedSMul 𝕜₂ Fₗ
inst_12 : CompleteSpace Eₗ
inst_13 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_14 : RingHomInvPair σ₁₂ σ₂₁
inst_15 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_norm₁ :
  ∃ (C : ℝ),
    ∀ (x : E),
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) ≤
        C * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm₂ :
  ∃ (C : ℝ),
    ∀ (x : F),
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) ≤
        C * norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ Function.RightInverse.{u_4 + 1, u_6 + 1} (α := Eₗ)
    (⇑(LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
          Fₗ →SL[σ₂₁] Eₗ) :
      (a : Fₗ) → Eₗ)
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁) :
          Eₗ →ₛₗ[σ₁₂] Fₗ)))
have refine_1 : ∀ (x : Fₗ),
  Membership.mem (γ := Set Fₗ) (Set.range.{u_6, u_5 + 1} (ι := F) (⇑e₂ : (a : F) → Fₗ)) x →
    AddHom.toFun.{u_4, u_6} (M := Eₗ)
        (LinearMap.toAddHom
            (↑(LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁) :
              Eₗ →ₛₗ[σ₁₂] Fₗ) :
          Eₗ →ₙ+ Fₗ)
        (((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
                Fₗ →SL[σ₂₁] Eₗ) :
              (a : Fₗ) → Eₗ)
            x :
          Eₗ) =
      x
Tactic: refine h_dense₂.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : AddCommGroup F
inst_5 : NormedAddCommGroup Fₗ
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 Eₗ
inst_8 : IsBoundedSMul 𝕜 Eₗ
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₂ Fₗ
inst_11 : IsBoundedSMul 𝕜₂ Fₗ
inst_12 : CompleteSpace Eₗ
inst_13 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_14 : RingHomInvPair σ₁₂ σ₂₁
inst_15 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_norm₁ :
  ∃ (C : ℝ),
    ∀ (x : E),
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) ≤
        C * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm₂ :
  ∃ (C : ℝ),
    ∀ (x : F),
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) ≤
        C * norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
refine_1 :
  ∀ (x : Fₗ),
    Membership.mem (γ := Set Fₗ) (Set.range.{u_6, u_5 + 1} (ι := F) (⇑e₂ : (a : F) → Fₗ)) x →
      AddHom.toFun.{u_4, u_6} (M := Eₗ)
          (LinearMap.toAddHom
              (↑(LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁) :
                Eₗ →ₛₗ[σ₁₂] Fₗ) :
            Eₗ →ₙ+ Fₗ)
          (((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
                  Fₗ →SL[σ₂₁] Eₗ) :
                (a : Fₗ) → Eₗ)
              x :
            Eₗ) =
        x
⊢ Function.RightInverse.{u_4 + 1, u_6 + 1} (α := Eₗ)
    (⇑(LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
          Fₗ →SL[σ₂₁] Eₗ) :
      (a : Fₗ) → Eₗ)
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁) :
          Eₗ →ₛₗ[σ₁₂] Fₗ)))
have refine_2 : IsClosed.{u_6} (X := Fₗ)
  {x : Fₗ |
    AddHom.toFun.{u_4, u_6} (M := Eₗ)
        (LinearMap.toAddHom
            (↑(LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁) :
              Eₗ →ₛₗ[σ₁₂] Fₗ) :
          Eₗ →ₙ+ Fₗ)
        (((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
                Fₗ →SL[σ₂₁] Eₗ) :
              (a : Fₗ) → Eₗ)
            x :
          Eₗ) =
      x}
Tactic: refine h_dense₂.induction ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : AddCommGroup F
inst_5 : NormedAddCommGroup Fₗ
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 Eₗ
inst_8 : IsBoundedSMul 𝕜 Eₗ
inst_9 : Module 𝕜₂ F
inst_10 : Module 𝕜₂ Fₗ
inst_11 : IsBoundedSMul 𝕜₂ Fₗ
inst_12 : CompleteSpace Eₗ
inst_13 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_14 : RingHomInvPair σ₁₂ σ₂₁
inst_15 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_norm₁ :
  ∃ (C : ℝ),
    ∀ (x : E),
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) ≤
        C * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm₂ :
  ∃ (C : ℝ),
    ∀ (x : F),
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) ≤
        C * norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ Continuous (Y := Fₗ) fun (x : Fₗ) ↦
    AddHom.toFun.{u_4, u_6} (M := Eₗ)
      (LinearMap.toAddHom
          (↑(LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁) :
            Eₗ →ₛₗ[σ₁₂] Fₗ) :
        Eₗ →ₙ+ Fₗ)
      (((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
              Fₗ →SL[σ₂₁] Eₗ) :
            (a : Fₗ) → Eₗ)
          x :
        Eₗ)
have simp : Continuous (Y := Fₗ) fun (x : Fₗ) ↦
  ((LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (Eₗ := Eₗ) (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁ : Eₗ →SL[σ₁₂] Fₗ) :
      (a : Eₗ) → Fₗ)
    (((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (Eₗ := Fₗ) (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
            Fₗ →SL[σ₂₁] Eₗ) :
          (a : Fₗ) → Eₗ)
        x :
      Eₗ)
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [ContinuousLinearEquiv.coe_toLinearEquiv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine h_dense₁.induction ?_ (isClosed_eq (by
        simp only [ContinuousLinearEquiv.coe_toLinearEquiv]; fun_prop) continuous_norm)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: convert! h_norm y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
y : E
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      norm.{u_6} (E := Fₗ) ((e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F) : (a : E) → Fₗ) x : Fₗ) ≤
        C * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
have h : ∀ (x : E),
  norm.{u_6} (E := Fₗ) ((e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F) : (a : E) → Fₗ) x : Fₗ) ≤
    1 * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.LinearIsometry (goal)
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
inst_8 : RingHomInvPair σ₂₃ σ₃₂
inst_9 : RingHomInvPair σ₃₂ σ₂₃
inst_10 : RingHomInvPair σ₁₄ σ₄₁
inst_11 : RingHomInvPair σ₄₁ σ₁₄
inst_12 : RingHomInvPair σ₂₄ σ₄₂
inst_13 : RingHomInvPair σ₄₂ σ₂₄
inst_14 : RingHomInvPair σ₃₄ σ₄₃
inst_15 : RingHomInvPair σ₄₃ σ₃₄
inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_18 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_19 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_20 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_21 : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst_22 : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst_23 : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst_24 : SeminormedAddCommGroup E
inst_25 : SeminormedAddCommGroup E₂
inst_26 : SeminormedAddCommGroup E₃
inst_27 : SeminormedAddCommGroup E₄
inst_28 : Module R E
inst_29 : Module R₂ E₂
inst_30 : Module R₃ E₃
inst_31 : Module R₄ E₄
inst_32 : NormedAddCommGroup F
inst_33 : Module R F
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry.{u_5, u_6} (α := E) (β := E₂) (⇑f : (a : E) → E₂)
⊢ ∀ (x : E), norm.{u_6} (E := E₂) ((f : (a : E) → E₂) x : E₂) = ‖x‖
have simp_rw : ∀ (x : E), dist.{u_6} (α := E₂) ((f : (a : E) → E₂) x : E₂) (0 : E₂) = dist x 0
Tactic: simp_rw [← dist_zero_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.LinearIsometry (goal)
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Eq.{u_6 + 1} (α := Set E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑e : (a : E) → E₂)) univ
have rw : Eq.{u_6 + 1} (α := Set E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑e.toIsometryEquiv : (a : E) → E₂)) univ
Tactic: rw [← coe_toIsometryEquiv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.LinearIsometry (goal)
Goal:
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E₂
inst_5 : Module R₂ E₂
inst_6 : NormedAddCommGroup F
inst_7 : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective.{u_9 + 1, u_6 + 1} (α := F) (β := E₂) (⇑f : (a : F) → E₂)
⊢ Eq (α := (a : F) → E₂) (⇑(ofSurjective f hfr) : (a : F) → E₂) (⇑f : (a : F) → E₂)
have h : ∀ (x : F), Eq.{u_6 + 1} (α := E₂) ((ofSurjective f hfr : (a : F) → E₂) x : E₂) ((f : (a : F) → E₂) x : E₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜_1 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜_1
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜_1 E
R_1 : Type u_3
inst_3 : NonUnitalSeminormedRing R_1
inst_4 : NormedSpace 𝕜_1 R_1
inst_5 : IsScalarTower 𝕜_1 R_1 R_1
inst_6 : SMulCommClass 𝕜_1 R_1 R_1
𝕜 : Type u_4
R : Type u_5
inst_7 : NontriviallyNormedField 𝕜
inst_8 : SeminormedRing R
inst_9 : NormedAlgebra 𝕜 R
inst_10 : NormOneClass R
x : R
⊢ ‖x‖ ≤ norm (E := R →L[𝕜] R) ((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R)
have h : ‖x‖ = norm (E := R) ((((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) 1 : R) / norm.{u_5} (E := R) 1
Tactic: convert! ratio_le_opNorm ((mul 𝕜 R) x) (1 : R)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_3
inst_1 : NonUnitalSeminormedCommRing R
inst_2 : NormedSpace 𝕜 R
inst_3 : IsScalarTower 𝕜 R R
inst_4 : SMulCommClass 𝕜 R R
⊢ Eq.{u_3 + 1} (α := R →L[𝕜] R →L[𝕜] R) (flip (mul 𝕜 R)) (mul 𝕜 R)
have h : ∀ (x x_1 : R),
  Eq (α := R) ((((flip (mul 𝕜 R) : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) x_1 : R)
    ((((mul 𝕜 R : (a : R) → R →L[𝕜] R) x : R →L[𝕜] R) : (a : R) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
⊢ norm (E := ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) (lsmul 𝕜 R) ≤ 1
have refine : ∀ (x : R), norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ 1 * ‖x‖
Tactic: refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : SeminormedRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : IsBoundedSMul R E
inst_7 : IsScalarTower 𝕜 R E
x : R
⊢ norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ 1 * ‖x‖
have simp_rw : norm.{u_2} (E := E →L[𝕜] E) ((lsmul 𝕜 R : (a : R) → E →L[𝕜] E) x : E →L[𝕜] E) ≤ ‖x‖
Tactic: simp_rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
⊢ norm (E := ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) (lsmul 𝕜 R) = 1
have refine_1 : ∀ (x : R),
  norm.{u_2} (E := E →L[𝕜] E)
      (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
        E →L[𝕜] E) ≤
    1 * ‖x‖
Tactic: refine ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
refine_1 :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      1 * ‖x‖
⊢ norm (E := ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) (lsmul 𝕜 R) = 1
have refine_2 : ∀ N ≥ 0,
  ∀
    (h :
      ∀ (x : R),
        norm.{u_2} (E := E →L[𝕜] E)
            (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E)
                x :
              E →L[𝕜] E) ≤
          N * ‖x‖),
    1 ≤ N
Tactic: refine ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
x : R
⊢ norm.{u_2} (E := E →L[𝕜] E)
      (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
        E →L[𝕜] E) ≤
    1 * ‖x‖
have refine_1 : norm.{u_2} (E := E →L[𝕜] E)
    (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
      E →L[𝕜] E) ≤
  ‖x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
N : ℝ
h_1 : N ≥ 0
h :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      N * ‖x‖
⊢ 1 ≤ N
have refine_2 : ∀ (y : E) (hy : y ≠ 0), 1 ≤ N
Tactic: obtain ⟨y, hy⟩ := exists_ne (0 : E)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_3
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
inst_5 : Module R E
inst_6 : NormSMulClass R E
inst_7 : IsScalarTower 𝕜 R E
inst_8 : Nontrivial E
N : ℝ
h_1 : N ≥ 0
h :
  ∀ (x : R),
    norm.{u_2} (E := E →L[𝕜] E)
        (((lsmul 𝕜 R : ContinuousLinearMap.{u_1, u_1, u_3, u_2} (RingHom.id 𝕜) R (E →L[𝕜] E)) : (a : R) → E →L[𝕜] E) x :
          E →L[𝕜] E) ≤
      N * ‖x‖
y : E
hy : y ≠ 0
⊢ 1 ≤ N
have refine_2 : 1 * ‖y‖ ≤ N * ‖y‖
Tactic: refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)