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 : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Eₗ
inst_4 : NormedSpace 𝕜₂ F
inst_5 : NormedSpace 𝕜 Eₗ
inst_6 : AddCommGroup E
inst_7 : Module 𝕜 E
inst_8 : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
C : ℝ
hC : 0 ≤ 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ₗ)
⊢ norm (E := Eₗ →SL[σ₁₂] F)
      (extendOfNorm.{u_1, u_2, u_3, u_4, u_5} (𝕜 := 𝕜) (𝕜₂ := 𝕜₂) (E := E) (Eₗ := Eₗ) (F := F) (σ₁₂ := σ₁₂) f e :
        Eₗ →SL[σ₁₂] F) ≤
    C

Tactic:
(f.extendOfNorm e).opNorm_le_bound hC (norm_extendOfNorm_apply_le h_dense C h_norm)

Premises used: ContinuousLinearMap.opNorm_le_bound, LinearMap.norm_extendOfNorm_apply_le, LinearMap.extendOfNorm
-- 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 : 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
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}
⊢ 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ₗ)))

Tactic:
refine h_dense₁.induction ?_ ?_
-- 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 : 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ₗ)
w : E
⊢ Eq.{u_4 + 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.{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ₗ)
          ((e₁ : (a : E) → Eₗ) w : Eₗ)) :
      Eₗ)
    ((e₁ : (a : E) → Eₗ) w : Eₗ)

Tactic:
simp [LinearMap.extendOfNorm_eq, h_dense₁, h_norm₁, h_dense₂, h_norm₂]

Premises used: LinearMap.extendOfNorm_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
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ₗ)
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ₗ)
⊢ 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)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]

Premises used: AddHom.toFun_eq_coe, ContinuousLinearMap.coe_coe, LinearMap.coe_toAddHom
-- 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 : 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ₗ)
      (((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:
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
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ₗ)
⊢ 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:
exact isClosed_eq (by simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]; fun_prop) continuous_id

Premises used: continuous_id, isClosed_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
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ₗ)))

Tactic:
h_dense₂.induction ?_ ?_

Premises used: Function.LeftInverse, Dense.induction, Function.RightInverse
-- 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 : 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
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}
⊢ 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ₗ)))

Tactic:
refine h_dense₂.induction ?_ ?_
-- 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 : 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ₗ)
w : 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ₗ)
          ((e₂ : (a : F) → Fₗ) w : Fₗ) :
        Eₗ) =
    (e₂ : (a : F) → Fₗ) w

Tactic:
simp [LinearMap.extendOfNorm_eq, h_dense₁, h_norm₁, h_dense₂, h_norm₂]

Premises used: LinearMap.extendOfNorm_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
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ₗ)
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ₗ)
⊢ 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ₗ)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]

Premises used: AddHom.toFun_eq_coe, ContinuousLinearMap.coe_coe, LinearMap.coe_toAddHom
-- 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 : 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ₗ) ↦
    ((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:
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
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ₗ)
⊢ 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:
exact isClosed_eq (by simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]; fun_prop) continuous_id

Premises used: continuous_id, isClosed_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
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ₗ)
x : Eₗ
⊢ Eq.{u_6 + 1} (α := Fₗ) ((f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ h_norm₂ : (a : Eₗ) → Fₗ) 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ₗ)
        x :
      Fₗ)

Tactic:
rfl

Premises used: rfl