awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f g : ι → E
hg : Summable g
h : f ~[cofinite] g
⊢ Summable f

Tactic:
summable_of_isBigO' hg h.isBigO

Premises used: Asymptotics.IsEquivalent.isBigO, summable_of_isBigO'
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f g : ℕ → E
hg : Summable g
h : f ~[atTop] g
⊢ Summable f

Tactic:
summable_of_isBigO_nat' hg h.isBigO

Premises used: Asymptotics.IsEquivalent.isBigO, summable_of_isBigO_nat'
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ E
inst_5 : FiniteDimensional ℝ F
f : ι → E
g : ι → F
h : f =Θ[cofinite] g
⊢ Summable f ↔ Summable g

Tactic:
⟨fun hf => summable_of_isBigO' hf h.isBigO_symm, fun hg => summable_of_isBigO' hg h.isBigO⟩

Premises used: Asymptotics.IsTheta.isBigO_symm, Asymptotics.IsTheta.isBigO, Iff.intro, summable_of_isBigO'
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ E
inst_5 : FiniteDimensional ℝ F
f : ℕ → E
g : ℕ → F
h : f =Θ[atTop] g
⊢ f =Θ[cofinite] g

Tactic:
simpa [← Nat.cofinite_eq_atTop] using h

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f g : ι → E
h : f ~[cofinite] g
⊢ Summable f ↔ Summable g

Tactic:
h.isTheta.summable_iff

Premises used: Asymptotics.IsTheta.summable_iff, Asymptotics.IsEquivalent.isTheta
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f g : ℕ → E
h : f ~[atTop] g
⊢ Summable f ↔ Summable g

Tactic:
h.isTheta.summable_iff_nat

Premises used: Asymptotics.IsTheta.summable_iff_nat, Asymptotics.IsEquivalent.isTheta
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : NontriviallyNormedField R
inst_2 : CompleteSpace R
inst_3 : AddCommGroup M
inst_4 : TopologicalSpace M
inst_5 : IsTopologicalAddGroup M
inst_6 : T2Space M
inst_7 : Module R M
inst_8 : ContinuousSMul R M
B : Basis ι R M
⊢ Continuous[inst_4, Pi.topologicalSpace] fun (m : M) ↦ (⇑((B.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R)

Tactic:
have := Finite.of_basis B
  LinearMap.continuous_of_finiteDimensional B.equivFun.toLinearMap

Premises used: LinearEquiv.toLinearMap, LinearMap.continuous_of_finiteDimensional, Module.Finite.of_basis, Module.Basis.equivFun
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : NontriviallyNormedField R
inst_2 : CompleteSpace R
inst_3 : AddCommGroup M
inst_4 : TopologicalSpace M
inst_5 : IsTopologicalAddGroup M
inst_6 : T2Space M
inst_7 : Module R M
inst_8 : ContinuousSMul R M
B : Basis ι R M
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpaceMatrix] fun (v : ι → M) ↦ B.toMatrix v

Tactic:
let _ := Fintype.ofFinite ι
  have := Finite.of_basis B
  LinearMap.continuous_of_finiteDimensional B.toMatrixEquiv.toLinearMap

Premises used: Fintype.ofFinite, Module.Basis.toMatrixEquiv, Module.Basis.toMatrix, LinearEquiv.toLinearMap, LinearMap.continuous_of_finiteDimensional, Module.Finite.of_basis
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
c : ℝ
hc : 0 < c
x : E
⊢ (fun (x : E) ↦ ‖f‖ * ‖x‖) (c • x) = c * (fun (x : E) ↦ ‖f‖ * ‖x‖) x

Tactic:
simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm]

Premises used: norm_smul, mul_left_comm, abs_of_pos, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
x y : E
rw : (fun (x : E) ↦ ‖f‖ * ‖x‖) (x + y) ≤ ‖f‖ * (‖x‖ + ‖y‖)
⊢ (fun (x : E) ↦ ‖f‖ * ‖x‖) (x + y) ≤ HAdd.hAdd (α := ℝ) ((fun (x : E) ↦ ‖f‖ * ‖x‖) x) ((fun (x : E) ↦ ‖f‖ * ‖x‖) y)

Tactic:
rw [← left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
x y : E
hbc : ‖x + y‖ ≤ ‖x‖ + ‖y‖
⊢ ‖f‖ * ‖x + y‖ ≤ ‖f‖ * (‖x‖ + ‖y‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
x y : E
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
norm_add_le x y

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
x y : E
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
exact norm_add_le x y

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
rcases :
  ∀ (g : E →ₗ[ℝ] ℝ)
    (g_eq :
      ∀ (x : ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ }.domain),
        (g : (a : E) → ℝ) (↑x : E) =
          (↑{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ } :
              ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) }.domain → ℝ)
            x)
    (g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖),
    ∃ (g : StrongDual ℝ E),
      (∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((f : (a : ↥p) → ℝ) x : ℝ)) ∧ ‖g‖ = ‖f‖
⊢ ∃ (g : StrongDual ℝ E),
    (∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((f : (a : ↥p) → ℝ) x : ℝ)) ∧ ‖g‖ = ‖f‖

Tactic:
rcases exists_extension_of_le_sublinear ⟨p, f⟩ (fun x => ‖f‖ * ‖x‖)
      (fun c hc x => by simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm])
      (fun x y => by
        rw [← left_distrib]
        dsimp; gcongr
        exact norm_add_le x y)
      fun x => le_trans (le_abs_self _) (f.le_opNorm _) with ⟨g, g_eq, g_le⟩

Premises used: Norm.norm, le_abs_self, HMul.hMul, ContinuousLinearMap.le_opNorm, exists_extension_of_le_sublinear, ContinuousLinearMap.toLinearMap, LinearPMap.mk, le_trans, LinearPMap.toFun'
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
g : E →ₗ[ℝ] ℝ
g_eq :
  ∀ (x : ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ }.domain),
    (g : (a : E) → ℝ) (↑x : E) =
      (↑{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ } :
          ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) }.domain → ℝ)
        x
g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ∃ (g : StrongDual ℝ E),
    (∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((f : (a : ↥p) → ℝ) x : ℝ)) ∧ ‖g‖ = ‖f‖

Tactic:
⟨g', g_eq, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
g : E →ₗ[ℝ] ℝ
g_eq :
  ∀ (x : ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ }.domain),
    (g : (a : E) → ℝ) (↑x : E) =
      (↑{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ } :
          ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) }.domain → ℝ)
        x
g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
refine : ‖g'‖ = ‖f‖
⊢ ∃ (g : StrongDual ℝ E),
    (∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((f : (a : ↥p) → ℝ) x : ℝ)) ∧ ‖g‖ = ‖f‖

Tactic:
refine ⟨g', g_eq, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
g : E →ₗ[ℝ] ℝ
g_eq :
  ∀ (x : ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ }.domain),
    (g : (a : E) → ℝ) (↑x : E) =
      (↑{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ } :
          ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) }.domain → ℝ)
        x
g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
apply : ‖f‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖
⊢ ‖g'‖ = ‖f‖

Tactic:
apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)

Premises used: le_antisymm, LinearMap.mkContinuous_norm_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
g : E →ₗ[ℝ] ℝ
g_eq :
  ∀ (x : ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ }.domain),
    (g : (a : E) → ℝ) (↑x : E) =
      (↑{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ } :
          ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) }.domain → ℝ)
        x
g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ‖f‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖

Tactic:
f.opNorm_le_bound (norm_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
g : E →ₗ[ℝ] ℝ
g_eq :
  ∀ (x : ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ }.domain),
    (g : (a : E) → ℝ) (↑x : E) =
      (↑{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) : E →ₗ.[ℝ] ℝ } :
          ↥{ domain := p, toFun := (↑f : ↥p →ₗ[ℝ] ℝ) }.domain → ℝ)
        x
g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
refine : ∀ (x : ↥p), Norm.norm (E := ℝ) ((f : (a : ↥p) → ℝ) x : ℝ) ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖
⊢ ‖f‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖

Tactic:
refine f.opNorm_le_bound (norm_nonneg _) fun x => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((f : (a : ↥p) → ℝ) x : ℝ)
g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
rw : Norm.norm (E := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖
⊢ Norm.norm (E := ℝ) ((f : (a : ↥p) → ℝ) x : ℝ) ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖

Tactic:
rw [← g_eq]
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((f : (a : ↥p) → ℝ) x : ℝ)
g_le : ∀ (x : E), (g : (a : E) → ℝ) x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
⊢ Norm.norm (E := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖

Tactic:
apply g'.le_opNorm

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
⊢ IsScalarTower ℝ 𝕜 E

Tactic:
haveI : IsScalarTower ℝ 𝕜 E := .restrictScalars _ _ _
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
obtain :
  ∀ (g : StrongDual ℝ E)
    (hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ))
    (hnormeq : ‖g‖ = ‖fr‖),
    ∃ (g : StrongDual 𝕜 E),
      (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖
⊢ ∃ (g : StrongDual 𝕜 E),
    (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖

Tactic:
obtain ⟨g, ⟨(hextends : ∀ x : p, g x = fr x), hnormeq⟩⟩ :=
    Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr

Premises used: Real, Submodule.restrictScalars, Real.exists_extension_norm_eq
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
⊢ ∃ (g : StrongDual 𝕜 E),
    (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖

Tactic:
⟨g.extendRCLike, ?_⟩

Premises used: StrongDual.extendRCLike, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
refine :
  (∀ (x : ↥p),
      Eq.{u_1 + 1} (α := 𝕜) (((g.extendRCLike : StrongDual 𝕜 E) : (a : E) → 𝕜) (↑x : E) : 𝕜)
        ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧
    norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) = ‖f‖
⊢ ∃ (g : StrongDual 𝕜 E),
    (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖

Tactic:
refine ⟨g.extendRCLike, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
rw :
  (↑((fr : (a : ↥p) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : ↥p) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜) =
    (f : (a : ↥p) → 𝕜) x
⊢ Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)

Tactic:
rw [g.extendRCLike_apply, ← Submodule.coe_smul,
      hextends, hextends]

Premises used: Submodule.coe_smul, StrongDual.extendRCLike_apply
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
⊢ (↑((fr : (a : ↥p) → ℝ) x) : 𝕜) -
      HMul.hMul (α := 𝕜) I (↑((fr : (a : ↥p) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜) =
    (f : (a : ↥p) → 𝕜) x

Tactic:
simp [fr, RCLike.algebraMap_eq_ofReal, mul_comm I, RCLike.re_add_im]

Premises used: RCLike.re_add_im, RCLike.algebraMap_eq_ofReal, RCLike.I, mul_comm
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
⊢ ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)

Tactic:
have h (x : p) : g.extendRCLike x = f x := by
    rw [g.extendRCLike_apply, ← Submodule.coe_smul,
      hextends, hextends]
    simp [fr, RCLike.algebraMap_eq_ofReal, mul_comm I, RCLike.re_add_im]
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
⊢ (∀ (x : ↥p),
      Eq.{u_1 + 1} (α := 𝕜) (((g.extendRCLike : StrongDual 𝕜 E) : (a : E) → 𝕜) (↑x : E) : 𝕜)
        ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧
    norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) = ‖f‖

Tactic:
⟨h, le_antisymm ?_ ?_⟩

Premises used: le_antisymm, And.intro
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
refine_1 : norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) ≤ ‖f‖
refine_2 : ‖f‖ ≤ norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E)
⊢ (∀ (x : ↥p),
      Eq.{u_1 + 1} (α := 𝕜) (((g.extendRCLike : StrongDual 𝕜 E) : (a : E) → 𝕜) (↑x : E) : 𝕜)
        ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧
    norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) = ‖f‖

Tactic:
refine ⟨h, le_antisymm ?_ ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
⊢ norm (E := StrongDual 𝕜 E) g.extendRCLike = ‖g‖

Tactic:
g.norm_extendRCLike

Premises used: StrongDual.norm_extendRCLike
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
⊢ ‖g‖ = ‖fr‖

Tactic:
hnormeq

Premises used: Set.Mem, Submodule.restrictScalars
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
⊢ ‖fr‖ ≤ norm.{u_1} (E := StrongDual ℝ 𝕜) reCLM * ‖f‖

Tactic:
ContinuousLinearMap.opNorm_comp_le _ _

Premises used: ContinuousLinearMap.restrictScalars, Set.Mem, setOf, ContinuousLinearMap.opNorm, ContinuousLinearMap.opNorm_comp_le