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
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
x : E
⊢ Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x) : F) ((f : (a : E) → F) x : F)

Tactic:
exact IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _

Premises used: IsUniformInducing.isDenseInducing, ContinuousLinearMap.cont, IsDenseInducing.extend_eq
-- 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 : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
g : Eₗ →SL[σ₁₂] F
H : g ∘SL e = f
simp : { toFun := ⋯.extend (⇑f : (a : E) → F), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } = g
⊢ f.extend e = g

Tactic:
simp only [extend, h_dense, h_e, and_self, ↓reduceDIte]

Premises used: and_self, reduceDIte, ContinuousLinearMap.extend
-- 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 : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
g : Eₗ →SL[σ₁₂] F
H : g ∘SL e = f
⊢ { toFun := ⋯.extend (⇑f : (a : E) → F), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } = g

Tactic:
ContinuousLinearMap.coeFn_injective <|
    uniformly_extend_unique h_e h_dense (ContinuousLinearMap.ext_iff.1 H) g.continuous

Premises used: uniformly_extend_unique, ContinuousLinearMap.continuous, ContinuousLinearMap.coeFn_injective, ContinuousLinearMap.ext_iff, Iff.mp
-- 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 : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
g : Eₗ →SL[σ₁₂] F
H : g ∘SL e = f
⊢ { toFun := ⋯.extend (⇑f : (a : E) → F), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } = g

Tactic:
exact ContinuousLinearMap.coeFn_injective <|
    uniformly_extend_unique h_e h_dense (ContinuousLinearMap.ext_iff.1 H) g.continuous

Premises used: uniformly_extend_unique, ContinuousLinearMap.continuous, ContinuousLinearMap.coeFn_injective, ContinuousLinearMap.ext_iff, Iff.mp
-- 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 : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
⊢ Eq (α := Eₗ →SL[σ₁₂] F) (extend 0 e) 0

Tactic:
extend_unique _ h_dense h_e _ (zero_comp _)

Premises used: ContinuousLinearMap.zero_comp, 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 : 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ₗ)
⊢ Continuous (Y := ℝ) fun (x : Eₗ) ↦ (↑N : ℝ) * ‖f‖ * ‖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 : 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ₗ)
refine_1 : 0 ≤ (↑N : ℝ) * ‖f‖
refine_2 : Continuous (Y := ℝ) fun (x : Eₗ) ↦ norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) x : F)
refine_3 :
  ∀ (x : E),
    norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : F) ≤
      (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
⊢ ‖f.extend e‖ ≤ (↑N : ℝ) * ‖f‖

Tactic:
refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ (by fun_prop)) fun x ↦ ?_)

Premises used: isClosed_le, ContinuousLinearMap.opNorm_le_bound, isClosed_property
-- 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 : 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ₗ)
hN : 0 ≤ N
⊢ 0 ≤ (↑N : ℝ) * ‖f‖

Tactic:
mul_nonneg hN (norm_nonneg _)

Premises used: mul_nonneg, norm_nonneg
-- 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 : 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ₗ)
hN : 0 ≤ N
⊢ 0 ≤ (↑N : ℝ) * ‖f‖

Tactic:
exact mul_nonneg hN (norm_nonneg _)

Premises used: mul_nonneg
-- 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 : 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ₗ)
hN : N ≤ 0
refine_1 : ∀ (this : Unique E), 0 ≤ (↑N : ℝ) * ‖f‖
⊢ 0 ≤ (↑N : ℝ) * ‖f‖

Tactic:
have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
-- 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 : 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ₗ)
hN : N ≤ 0
this : Unique E
⊢ f = 0

Tactic:
Subsingleton.elim ..

Premises used: Subsingleton.elim
-- 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 : 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ₗ)
hN : N ≤ 0
this : Unique E
refine_1 : 0 ≤ (↑N : ℝ) * norm (E := E →SL[σ₁₂] F) 0
⊢ 0 ≤ (↑N : ℝ) * ‖f‖

Tactic:
obtain rfl : f = 0 := Subsingleton.elim ..

Premises used: Subsingleton.elim, 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 : 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
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ₗ)
hN : N ≤ 0
this : Unique E
⊢ 0 ≤ (↑N : ℝ) * norm (E := E →SL[σ₁₂] F) 0

Tactic:
simp
-- 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 : 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ₗ)
⊢ 0 ≤ N ∨ N ≤ 0

Tactic:
cases le_total 0 N with
    | inl hN => exact mul_nonneg hN (norm_nonneg _)
    | inr hN =>
      have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
      obtain rfl : f = 0 := Subsingleton.elim ..
      simp

Premises used: le_total, ContinuousLinearMap.inr, ContinuousLinearMap.inl, Subsingleton.elim, OfNat.ofNat, 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 : 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ₗ)
⊢ Continuous (Y := ℝ) fun (x : Eₗ) ↦ norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) x : F)

Tactic:
(cont _).norm

Premises used: Continuous.norm, ContinuousLinearMap.cont
-- 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 : 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ₗ)
⊢ Continuous (Y := ℝ) fun (x : Eₗ) ↦ norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) x : F)

Tactic:
exact (cont _).norm

Premises used: Continuous.norm, ContinuousLinearMap.cont
-- 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 : 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
refine_3 :
  norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
⊢ norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : F) ≤
    (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)

Tactic:
rw [extend_eq _ h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing]

Premises used: IsUniformEmbedding.isUniformInducing, ContinuousLinearMap.extend_eq, ContinuousLinearMap.isUniformEmbedding_of_bound
-- 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 : 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) ≤ ‖f‖ * ‖x‖

Tactic:
le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- 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 : 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
hbc : ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * ((↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ))

Tactic:
gcongr
-- 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 : 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
⊢ ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)

Tactic:
h_e 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 : 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
⊢ ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)

Tactic:
exact h_e 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 : 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ₗ)
rw₁ 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ₗ)

Tactic:
rw [mul_comm ↑N ‖f‖, mul_assoc]

Premises used: Norm.norm, mul_assoc, mul_comm
-- 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 : 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ₗ))
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ₗ)
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑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]

Premises used: Norm.norm, HMul.hMul, ContinuousLinearMap.le_opNorm, DFunLike.coe, NNReal.toReal
-- 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ₗ)),
    g.ker ≤ f.ker
⊢ g.ker ≤ f.ker

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ₗ)
x : E
hx : x ∈ g.ker
⊢ 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
-- 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 : ℝ
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ₗ)
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) 0

Tactic:
rw [hx] at 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 : ℝ
x : E
hx : x ∈ g.ker
h : norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * norm.{u_4} (E := Eₗ) 0
⊢ x ∈ f.ker

Tactic:
simpa using h