awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ)
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 ⋯ ∘ₛₗ (↑g.quotKerEquivRange.symm : ↥g.range →ₗ[𝕜] E ⧸ g.ker) : (a : ↥g.range) → F) x : F) ≤
          C_1 * ‖x‖
⊢ ∃ (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‖

Tactic:
obtain ⟨C, h⟩ := h
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ)
h₁ :
  ∀ (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‖
⊢ ∃ (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‖

Tactic:
use C
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
y : E
hxy : (g : (a : E) → Eₗ) y = x
⊢ norm.{u_5} (E := F)
      ((g.ker.liftQ f ⋯ ∘ₛₗ (↑g.quotKerEquivRange.symm : ↥g.range →ₗ[𝕜] E ⧸ g.ker) : (a : ↥g.range) → F)
          (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ g.range) x ⋯) :
        F) ≤
    C * norm (E := ↥g.range) (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ g.range) x ⋯)

Tactic:
simpa [← hxy] using h y
-- Module: Mathlib.Analysis.Normed.Operator.Extend
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
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_norm :
  ∃ (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ₗ)
x : E
y : Eₗ
hx : (g : (a : E) → Eₗ) x = y
⊢ Eq.{u_5 + 1} (α := F)
    ((f.compLeftInverse g : (a : ↥g.range) → F) (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ g.range) y ⋯) : F)
    ((f : (a : E) → F) x : F)

Tactic:
simp [compLeftInverse, h_norm, ← hx]

Premises used: LinearMap.compLeftInverse
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ DenseRange (X := Eₗ) (α := ↥e.range) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)

Tactic:
simpa using h_dense
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ ∀ (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
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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.compLeftInverse e).extend e.range.subtypeL : (a : Eₗ) → F)
        ((e.range.subtypeL : (a : ↥e.range) → Eₗ)
            (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) ((e : (a : E) → Eₗ) x) ⋯ : ↥e.range) :
          Eₗ) :
      F)
    ((f.compLeftInverse e : (a : ↥e.range) → F)
        (Subtype.mk (p := fun (x : Eₗ) ↦ x ∈ e.range) ((e : (a : E) → Eₗ) x) ⋯ : ↥e.range) :
      F)

Tactic:
this ⟨e x, LinearMap.mem_range_self e x⟩

Premises used: LinearMap.mem_range_self, Subtype.mk, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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)
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) ⋯ : ↥e.range) :
      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)

Tactic:
convert! this ⟨e x, LinearMap.mem_range_self e x⟩

Premises used: LinearMap.mem_range_self, Subtype.mk, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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 : (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) ⋯ : ↥e.range) :
      F)

Tactic:
(compLeftInverse_apply_of_bdd _ _ h_norm _ _ rfl).symm

Premises used: LinearMap.compLeftInverse_apply_of_bdd, Eq.symm, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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 : (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) ⋯ : ↥e.range) :
      F)

Tactic:
exact (compLeftInverse_apply_of_bdd _ _ h_norm _ _ rfl).symm

Premises used: LinearMap.compLeftInverse_apply_of_bdd, Eq.symm, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
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‖
⊢ ∀ (hy : x ∈ e.range), norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖

Tactic:
⟨y, hxy⟩
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
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:
simpa only [← hxy, extendOfNorm_eq h_dense ⟨C, h_norm⟩ y] using h_norm y

Premises used: LinearMap.extendOfNorm_eq, Exists.intro
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
⊢ ∀ (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
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
h_mem : ∀ (x : Eₗ) (hy : x ∈ e.range), norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖
⊢ Continuous (Y := ℝ) fun (x : Eₗ) ↦ norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
h_mem : ∀ (x : Eₗ) (hy : x ∈ e.range), norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖
⊢ Continuous (Y := ℝ) fun (x : Eₗ) ↦ C * ‖x‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
h_mem : ∀ (x : Eₗ) (hy : x ∈ e.range), norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖
⊢ norm.{u_5} (E := F) ((f.extendOfNorm e : (a : Eₗ) → F) x : F) ≤ C * ‖x‖

Tactic:
exact h_dense.induction h_mem (isClosed_le (by fun_prop) (by fun_prop)) x
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ)
H₁ : g ∘SL e.range.subtypeL = f.compLeftInverse e
⊢ f.extendOfNorm e = g

Tactic:
apply ContinuousLinearMap.extend_unique

Premises used: ContinuousLinearMap.extend_unique
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ DenseRange (X := Eₗ) (α := ↥e.range) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)

Tactic:
simpa using h_dense
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ IsUniformInducing (α := ↥e.range) (β := Eₗ) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)

Tactic:
isUniformEmbedding_subtype_val.isUniformInducing

Premises used: IsUniformEmbedding.isUniformInducing, isUniformEmbedding_subtype_val
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ IsUniformInducing (α := ↥e.range) (β := Eₗ) (⇑e.range.subtypeL : (a : ↥e.range) → Eₗ)

Tactic:
exact isUniformEmbedding_subtype_val.isUniformInducing

Premises used: IsUniformEmbedding.isUniformInducing, isUniformEmbedding_subtype_val
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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₁ :
  ∀ (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)
⊢ g ∘SL e.range.subtypeL = f.compLeftInverse e

Tactic:
ext ⟨y, x, hxy⟩
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
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 ⋯) : F)
    ((f : (a : E) → F) x : F)
⊢ 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)

Tactic:
rw [compLeftInverse_apply_of_bdd _ _ ⟨C, h_norm⟩ x y hxy]

Premises used: LinearMap.compLeftInverse_apply_of_bdd, Exists.intro
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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 : (a : E) → F) x : F)

Tactic:
simp [← hxy, ← H]