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

Tactic:
rfl

Premises used: 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
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ₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ) : Fₗ)
    ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ)

Tactic:
LinearMap.extendOfNorm_eq h_dense₁ h_norm₁ x

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

Tactic:
LinearMap.extendOfNorm_eq h_dense₂ h_norm₂ x

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ₗ
C : ℝ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_norm₁ :
  ∀ (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ₗ
⊢ norm.{u_6} (E := Fₗ) ((f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ h_norm₂ : (a : Eₗ) → Fₗ) x : Fₗ) ≤ C * ‖x‖

Tactic:
LinearMap.norm_extendOfNorm_apply_le h_dense₁ _ h_norm₁ _

Premises used: LinearMap.norm_extendOfNorm_apply_le
-- 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ₗ
C : ℝ
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₂ :
  ∀ (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 : Fₗ
⊢ norm.{u_4} (E := Eₗ) (((f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ ⋯).symm : (a : Fₗ) → Eₗ) x : Eₗ) ≤ C * ‖x‖

Tactic:
LinearMap.norm_extendOfNorm_apply_le h_dense₂ _ h_norm₂ _

Premises used: LinearMap.norm_extendOfNorm_apply_le
-- 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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
x : F
⊢ norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)

Tactic:
simpa using (h_norm (f.symm x)).symm

Premises used: LinearEquiv.symm, Eq.symm, 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
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) ≤
      1 * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)

Tactic:
simp [h_norm]
-- 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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) ≤
      1 * norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)

Tactic:
simp [h_norm₂]
-- 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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [ContinuousLinearEquiv.coe_toLinearEquiv]

Premises used: ContinuousLinearEquiv.coe_toLinearEquiv
-- 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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine h_dense₁.induction ?_ (isClosed_eq (by
        simp only [ContinuousLinearEquiv.coe_toLinearEquiv]; fun_prop) continuous_norm)
-- 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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
y : E
⊢ norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) y : F) : Fₗ) =
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) y : Eₗ)

Tactic:
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
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
y : E
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
convert! 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
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
y : E
h :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F) : (a : E) → Fₗ) x : Fₗ) ≤
      1 * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      norm.{u_6} (E := Fₗ) ((e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F) : (a : E) → Fₗ) x : Fₗ) ≤
        C * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)

Tactic:
use 1
-- 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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
y : E
⊢ ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F) : (a : E) → Fₗ) x : Fₗ) ≤
      1 * norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)

Tactic:
simp [h_norm]
-- 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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
h_norm₂ :
  ∀ (x : F),
    norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) ((f.symm : (a : F) → E) x : E) : Eₗ) =
      norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) x : Fₗ)
y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply LinearMap.extendOfNorm_eq h_dense₁ (by use 1; simp [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 : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
x : Eₗ
⊢ Eq.{u_6 + 1} (α := Fₗ) ((f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm : (a : Eₗ) → Fₗ) x : Fₗ)
    (((LinearMap.extendOfNorm.{u_1, u_2, u_3, u_4, u_6} (𝕜 := 𝕜) (𝕜₂ := 𝕜₂) (E := E) (Eₗ := Eₗ) (F := Fₗ) (σ₁₂ := σ₁₂)
              (e₂ ∘ₛₗ (↑f : E →ₛₗ[σ₁₂] F)) e₁ :
            Eₗ →SL[σ₁₂] Fₗ) :
          (a : Eₗ) → Fₗ)
        x :
      Fₗ)

Tactic:
rfl

Premises used: 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
Fₗ : Type u_6
inst : NormedField 𝕜
inst_1 : NormedField 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : NormedAddCommGroup Eₗ
inst_7 : NormedSpace 𝕜 Eₗ
inst_8 : CompleteSpace Eₗ
inst_9 : NormedAddCommGroup Fₗ
inst_10 : NormedSpace 𝕜₂ Fₗ
inst_11 : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e₁ : (a : E) → Eₗ)
h_dense₂ : DenseRange.{u_6, u_5} (X := Fₗ) (α := F) (⇑e₂ : (a : F) → Fₗ)
h_norm :
  ∀ (x : E),
    norm.{u_6} (E := Fₗ) ((e₂ : (a : F) → Fₗ) ((f : (a : E) → F) x : F) : Fₗ) =
      norm.{u_4} (E := Eₗ) ((e₁ : (a : E) → Eₗ) x : Eₗ)
x : Fₗ
⊢ Eq.{u_4 + 1} (α := Eₗ) (((f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm).symm : (a : Fₗ) → Eₗ) x : Eₗ)
    (((LinearMap.extendOfNorm.{u_2, u_1, u_5, u_6, u_4} (𝕜 := 𝕜₂) (𝕜₂ := 𝕜) (E := F) (Eₗ := Fₗ) (F := Eₗ) (σ₁₂ := σ₂₁)
              (e₁ ∘ₛₗ (↑f.symm : F →ₛₗ[σ₂₁] E)) e₂ :
            Fₗ →SL[σ₂₁] Eₗ) :
          (a : Fₗ) → Eₗ)
        x :
      Eₗ)

Tactic:
rfl

Premises used: rfl