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
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ))
have hbc : ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
Tactic: gcongr
-- 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
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
⊢ ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)) ≤
    (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
have rw : ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)) ≤
  ‖f‖ * (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
Tactic: rw [mul_comm ↑N ‖f‖, mul_assoc]
-- 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
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
rw :
  ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)) ≤
    ‖f‖ * (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
⊢ ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)) ≤
    (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
have rw₁ : ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)) ≤
  ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ))
Tactic: rw [mul_comm ↑N ‖f‖, mul_assoc]
-- 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
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
have le_opNorm : ‖f‖ * ‖x‖ ≤ ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ))
Tactic: calc
      ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
      _ ≤ ‖f‖ * (N * ‖e x‖) := by gcongr; exact h_e x
      _ ≤ N * ‖f‖ * ‖e x‖ := by rw [mul_comm ↑N ‖f‖, mul_assoc]
-- 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
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
le_opNorm : ‖f‖ * ‖x‖ ≤ ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ))
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
have le_opNorm₁ : ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)) ≤
  (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
Tactic: calc
      ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
      _ ≤ ‖f‖ * (N * ‖e x‖) := by gcongr; exact h_e x
      _ ≤ N * ‖f‖ * ‖e x‖ := by rw [mul_comm ↑N ‖f‖, mul_assoc]
-- 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 : DivisionRing 𝕜
inst_1 : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : SeminormedAddCommGroup Eₗ
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
h :
  ∃ (C : ℝ),
    ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)
⊢ g.ker ≤ f.ker
have obtain : ∀ (C : ℝ)
  (h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)),
  g.ker ≤ f.ker
Tactic: obtain ⟨C, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : DivisionRing 𝕜
inst_1 : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : SeminormedAddCommGroup Eₗ
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
C : ℝ
h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)
x : E
hx : x ∈ g.ker
⊢ x ∈ f.ker
have h₁ : norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)
Tactic: specialize h x
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : DivisionRing 𝕜
inst_1 : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : SeminormedAddCommGroup Eₗ
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
C : ℝ
x : E
hx : x ∈ g.ker
h : norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)
⊢ x ∈ f.ker
have h₁ : norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) 0
Tactic: rw [hx] at h
Cleared hypotheses: h
-- 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 : DivisionRing 𝕜
inst_1 : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : SeminormedAddCommGroup Eₗ
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
h :
  ∃ (C : ℝ),
    ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)
⊢ ∃ (C : ℝ),
    ∀ (x : ↥g.range),
      norm.{u_5} (E := F)
          ((g.ker.liftQ f ⋯ ∘ₛₗ (↑g.quotKerEquivRange.symm : ↥g.range →ₗ[𝕜] E ⧸ g.ker) : (a : ↥g.range) → F) x : F) ≤
        C * ‖x‖
have obtain : ∀ (C : ℝ)
  (h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)),
  ∃ (C_1 : ℝ),
    ∀ (x : ↥g.range),
      norm.{u_5} (E := F)
          ((g.ker.liftQ f sorry ∘ₛₗ (↑g.quotKerEquivRange.symm : ↥g.range →ₗ[𝕜] E ⧸ g.ker) : (a : ↥g.range) → F) x : F) ≤
        C_1 * ‖x‖
Tactic: obtain ⟨C, h⟩ := h
Cleared hypotheses: h
-- 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 : DivisionRing 𝕜
inst_1 : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : SeminormedAddCommGroup Eₗ
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
C : ℝ
h : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((g : (a : E) → Eₗ) x : Eₗ)
⊢ ∃ (C_1 : ℝ),
    ∀ (x : ↥g.range),
      norm.{u_5} (E := F)
          ((g.ker.liftQ f ⋯ ∘ₛₗ (↑g.quotKerEquivRange.symm : ↥g.range →ₗ[𝕜] E ⧸ g.ker) : (a : ↥g.range) → F) x : F) ≤
        C_1 * ‖x‖
have h₁ : ∀ (x : ↥g.range),
  norm.{u_5} (E := F)
      ((g.ker.liftQ f sorry ∘ₛₗ (↑g.quotKerEquivRange.symm : ↥g.range →ₗ[𝕜] E ⧸ g.ker) : (a : ↥g.range) → F) x : F) ≤
    C * ‖x‖
Tactic: use C
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_norm :
  ∃ (C : ℝ),
    ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
⊢ Eq.{u_5 + 1} (α := F) ((f.extendOfNorm e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : F) ((f : (a : E) → F) x : F)
have this : ∀ (x : ↥e.range),
  Eq.{u_5 + 1} (α := F)
    (((f.compLeftInverse e).extend e.range.subtypeL : (a : Eₗ) → F) ((e.range.subtypeL : (a : ↥e.range) → Eₗ) x : Eₗ) :
      F)
    ((f.compLeftInverse e : (a : ↥e.range) → F) x : F)
Tactic: have := (f.compLeftInverse e).extend_eq (e := (LinearMap.range e).subtypeL)
    (by simpa using h_dense) isUniformEmbedding_subtype_val.isUniformInducing
-- 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
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_norm :
  ∃ (C : ℝ),
    ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
this :
  ∀ (x : ↥e.range),
    Eq.{u_5 + 1} (α := F)
      (((f.compLeftInverse e).extend e.range.subtypeL : (a : Eₗ) → F)
          ((e.range.subtypeL : (a : ↥e.range) → Eₗ) x : Eₗ) :
        F)
      ((f.compLeftInverse e : (a : ↥e.range) → F) x : F)
⊢ Eq.{u_5 + 1} (α := F) ((f.extendOfNorm e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : F) ((f : (a : E) → F) x : F)
have h : Eq.{u_5 + 1} (α := F) ((f : (a : E) → F) x : F)
  ((f.compLeftInverse e : (a : ↥e.range) → F)
      (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) ((e : (a : E) → Eₗ) x) sorry : ↥e.range) :
    F)
Tactic: convert! this ⟨e x, LinearMap.mem_range_self e x⟩
-- 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
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
h_norm : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x_1 x : Eₗ
⊢ ∀ (hy : x ∈ e.range), norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖
have this : ∀ (y : E) (hxy : (e : (a : E) → Eₗ) y = x), norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖
Tactic: ⟨y, hxy⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
h_norm : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : Eₗ
⊢ norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖
have h_mem : ∀ (x : Eₗ) (hy : x ∈ e.range), norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖
Tactic: have h_mem : ∀ (x : Eₗ) (hy : x ∈ (LinearMap.range e)), ‖extendOfNorm f e x‖ ≤ C * ‖x‖ := by
    intro x ⟨y, hxy⟩
    simpa only [← hxy, extendOfNorm_eq h_dense ⟨C, h_norm⟩ y] using 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
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
h_norm : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
g : Eₗ →SL[σ₁₂] F
H : (↑g : Eₗ →ₛₗ[σ₁₂] F) ∘ₛₗ e = f
⊢ f.extendOfNorm e = g
have h_dense₁ : DenseRange (X := Eₗ) (α := ↥e.range) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)
Tactic: apply ContinuousLinearMap.extend_unique
-- 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
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
h_norm : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
g : Eₗ →SL[σ₁₂] F
H : (↑g : Eₗ →ₛₗ[σ₁₂] F) ∘ₛₗ e = f
h_dense₁ : DenseRange (X := Eₗ) (α := ↥e.range) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)
⊢ f.extendOfNorm e = g
have h_e : IsUniformInducing (α := ↥e.range) (β := Eₗ) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)
Tactic: apply ContinuousLinearMap.extend_unique
-- 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
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
h_norm : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
g : Eₗ →SL[σ₁₂] F
H : (↑g : Eₗ →ₛₗ[σ₁₂] F) ∘ₛₗ e = f
h_dense₁ : DenseRange (X := Eₗ) (α := ↥e.range) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)
h_e : IsUniformInducing (α := ↥e.range) (β := Eₗ) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)
⊢ f.extendOfNorm e = g
have H₁ : g ∘SL e.range.subtypeL = f.compLeftInverse e
Tactic: apply ContinuousLinearMap.extend_unique
-- 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
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
h_norm : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
g : Eₗ →SL[σ₁₂] F
H : (↑g : Eₗ →ₛₗ[σ₁₂] F) ∘ₛₗ e = f
⊢ g ∘SL e.range.subtypeL = f.compLeftInverse e
have H₁ : ∀ (y : Eₗ) (x : E) (hxy : (e : (a : E) → Eₗ) x = y),
  Eq.{u_5 + 1} (α := F)
    ((g ∘SL e.range.subtypeL : (a : ↥e.range) → F) (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) y sorry) : F)
    ((f.compLeftInverse e : (a : ↥e.range) → F) (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) y sorry) : F)
Tactic: ext ⟨y, x, hxy⟩
-- 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
inst : NormedDivisionRing 𝕜
inst_1 : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : AddCommGroup E
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜₂ F
inst_7 : IsBoundedSMul 𝕜₂ F
inst_8 : Module 𝕜 Eₗ
inst_9 : IsBoundedSMul 𝕜 Eₗ
inst_10 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
h_norm : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
g : Eₗ →SL[σ₁₂] F
H : (↑g : Eₗ →ₛₗ[σ₁₂] F) ∘ₛₗ e = f
y : Eₗ
x : E
hxy : (e : (a : E) → Eₗ) x = y
⊢ Eq.{u_5 + 1} (α := F)
    ((g ∘SL e.range.subtypeL : (a : ↥e.range) → F) (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) y ⋯) : F)
    ((f.compLeftInverse e : (a : ↥e.range) → F) (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) y ⋯) : F)
have H₁ : Eq.{u_5 + 1} (α := F)
  ((g ∘SL e.range.subtypeL : (a : ↥e.range) → F) (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) y sorry) : F)
  ((f : (a : E) → F) x : F)
Tactic: rw [compLeftInverse_apply_of_bdd _ _ ⟨C, h_norm⟩ x y hxy]
-- 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.LeftInverse.{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 : Eₗ),
  Membership.mem (γ := Set Eₗ) (Set.range.{u_4, u_3 + 1} (ι := E) (⇑e₁ : (a : E) → Eₗ)) x →
    ((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) =
      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 : Eₗ),
    Membership.mem (γ := Set Eₗ) (Set.range.{u_4, u_3 + 1} (ι := E) (⇑e₁ : (a : E) → Eₗ)) x →
      ((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) =
        x
⊢ Function.LeftInverse.{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_4} (X := Eₗ)
  {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) =
      x}
Tactic: refine h_dense₁.induction ?_ ?_