awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace 𝕜
inst_4 : FiniteDimensional 𝕜 E
⊢ ProperSpace E
have this : ProperSpace 𝕜
Tactic: have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
⊢ ProperSpace.{u_2} ↥S
have a : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
h : Nontrivial E
⊢ ProperSpace.{u_2} ↥S
have this : ProperSpace 𝕜
Tactic: have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
h : Nontrivial E
this : ProperSpace 𝕜
⊢ ProperSpace.{u_2} ↥S
have this₁ : FiniteDimensional 𝕜 E
Tactic: have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y
have rcases : ∀ (y : E) (hys : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] sᶜ) (hyd : infDist x sᶜ = dist x y),
  ∃ y ∈ frontier s, infDist x sᶜ = dist x y
Tactic: rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] sᶜ
hyd : infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y
have hys₁ : y ∈ (interior s)ᶜ
Tactic: rw [closure_compl] at hys
Cleared hypotheses: hys, hyd
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y
have refine : infDist x sᶜ = dist y x
Tactic: refine ⟨y, ⟨Metric.closedBall_infDist_compl_subset_closure hx <|
    Metric.mem_closedBall.2 <| ge_of_eq ?_, hys⟩, hyd⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ x ∈ interior K ∪ frontier K
have rw : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
Tactic: rw [← closure_eq_interior_union_frontier]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
have inl : ∀ (hx' : x ∈ interior K), ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
Tactic: obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
    rw [← closure_eq_interior_union_frontier]
    exact subset_closure hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
inl : ∀ (hx' : x ∈ interior K), ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
have inr : ∀ (hx' : x ∈ frontier K), ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
Tactic: obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
    rw [← closure_eq_interior_union_frontier]
    exact subset_closure hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ interior K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
have hx'₁ : ∃ (i : ℝ), 0 < i ∧ closedBall x i ⊆ K
Tactic: rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : ∃ (i : ℝ), 0 < i ∧ closedBall x i ⊆ K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
have inl : ∀ (r : ℝ) (hr₀ : 0 < r) (hrK : closedBall x r ⊆ K), ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
Tactic: rcases hx' with ⟨r, hr₀, hrK⟩
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : closedBall x r ⊆ K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
have this : FiniteDimensional ℝ E
Tactic: have : FiniteDimensional ℝ E :=
      .of_isCompact_closedBall ℝ hr₀
        (hK.of_isClosed_subset Metric.isClosed_closedBall hrK)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
have inr : infDist x Kᶜ = dist x x
Tactic: refine ⟨x, hx', ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ infDist x Kᶜ = dist x x
have hx'₁ : x ∈
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ
Tactic: rw [frontier_eq_closure_inter_closure] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' :
  x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ
⊢ infDist x Kᶜ = dist x x
have inr : 0 = dist x x
Tactic: rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' :
  x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ
inr : 0 = dist x x
⊢ infDist x Kᶜ = dist x x
have inr₁ : Eq (α := ℝ) 0 0
Tactic: rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
⊢ (Summable (α := ℝ) fun (x : α) ↦ ‖f x‖) ↔ Summable f
have refine : ∀ (hf : Summable f), Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
Tactic: refine ⟨Summable.of_norm, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
have obtain : ∀ (v : Basis (Fin (finrank ℝ E)) ℝ E), Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
Tactic: obtain v := Module.finBasis ℝ E
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
have H : Summable (α := ℝ) fun (x : α) ↦
  norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f x) : Fin (finrank ℝ E) → ℝ)
Tactic: have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
H :
  Summable (α := ℝ) fun (x : α) ↦
    norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f x) : Fin (finrank ℝ E) → ℝ)
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
have refine : ∀ (i : α),
  ‖‖f i‖‖ ≤
    (↑‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ : ℝ) *
      norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f i) : Fin (finrank ℝ E) → ℝ)
Tactic: refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
have suffices : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
Tactic: suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by
    obtain v := Module.finBasis ℝ E
    set e := v.equivFunL
    have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
    refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
    simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
have this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
Tactic: have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
have refine : ∀ (x : α), ‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖
Tactic: refine .of_norm_bounded (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
⊢ ‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖
have rw : ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖
Tactic: rw [norm_norm, pi_norm_le_iff_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
rw : ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖
⊢ ‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖
have rw₁ : LE.le (α := ℝ) 0 (∑ i : Fin N, ‖g x i‖)
Tactic: rw [norm_norm, pi_norm_le_iff_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
⊢ ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖
have refine : ∀ (i i : Fin N), Membership.mem (γ := Finset (Fin N)) Finset.univ i → LE.le (α := ℝ) 0 ((fun (i : Fin N) ↦ ‖g x i‖) i)
Tactic: refine fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n * r ^ n‖
have rcases : ∀ (r' : ℝ) (hrr' : ‖r‖ < r') (h : r' < 1), Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n * r ^ n‖
Tactic: rcases exists_between hr with ⟨r', hrr', h⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n * r ^ n‖
have apply : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (x : ℕ) ↦ ‖r' ^ x‖
Tactic: apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h).norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n
have apply : ∀ᶠ (x : ℕ) in atTop, ‖‖u x * r ^ x‖‖ ≤ norm (E := ℝ) 1 * ‖‖u x‖ * ‖r‖ ^ x‖
Tactic: apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ ∀ᶠ (x : ℕ) in atTop, ‖‖u x * r ^ x‖‖ ≤ norm (E := ℝ) 1 * ‖‖u x‖ * ‖r‖ ^ x‖
have h₁ : ∀ (n : ℕ) (hn : ‖r ^ n‖ ≤ ‖r‖ ^ n), ‖‖u n * r ^ n‖‖ ≤ norm (E := ℝ) 1 * ‖‖u n‖ * ‖r‖ ^ n‖
Tactic: filter_upwards [eventually_norm_pow_le r] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖r' ^ n‖
have h₁ : ∀ (x : ℕ), ‖HPow.hPow (α := F) (↑x : F) k‖ * ‖r‖ ^ x = ‖HPow.hPow (α := F) (↑x : F) k * r ^ x‖
Tactic: convert!
        isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (x : ℕ) ↦ ‖r' ^ x‖
have fun : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n
Tactic: calc
  fun n ↦ ‖(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp
  _ =O[atTop] fun n ↦ ‖((n : F) ^ k)‖ * ‖r‖ ^ n := by
      simpa [Nat.cast_pow] using
      (isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)
  _ =O[atTop] fun n ↦ ‖r' ^ n‖ := by
      convert!
        isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
      simp only [norm_pow, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
fun : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (x : ℕ) ↦ ‖r' ^ x‖
have fun₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n
Tactic: calc
  fun n ↦ ‖(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp
  _ =O[atTop] fun n ↦ ‖((n : F) ^ k)‖ * ‖r‖ ^ n := by
      simpa [Nat.cast_pow] using
      (isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)
  _ =O[atTop] fun n ↦ ‖r' ^ n‖ := by
      convert!
        isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
      simp only [norm_pow, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
fun : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n
fun₁ :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (x : ℕ) ↦ ‖r' ^ x‖
have fun₂ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖r' ^ n‖
Tactic: calc
  fun n ↦ ‖(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp
  _ =O[atTop] fun n ↦ ‖((n : F) ^ k)‖ * ‖r‖ ^ n := by
      simpa [Nat.cast_pow] using
      (isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)
  _ =O[atTop] fun n ↦ ‖r' ^ n‖ := by
      convert!
        isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
      simp only [norm_pow, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
x y : E
⊢ (fun (x : E) ↦ ‖f‖ * ‖x‖) (x + y) ≤ HAdd.hAdd (α := ℝ) ((fun (x : E) ↦ ‖f‖ * ‖x‖) x) ((fun (x : E) ↦ ‖f‖ * ‖x‖) y)
have rw : (fun (x : E) ↦ ‖f‖ * ‖x‖) (x + y) ≤ ‖f‖ * (‖x‖ + ‖y‖)
Tactic: rw [← left_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
x y : E
⊢ ‖f‖ * ‖x + y‖ ≤ ‖f‖ * (‖x‖ + ‖y‖)
have hbc : ‖x + y‖ ≤ ‖x‖ + ‖y‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
p : Subspace ℝ E
f : StrongDual ℝ ↥p
⊢ ∃ (g : StrongDual ℝ E),
    (∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((f : (a : ↥p) → ℝ) x : ℝ)) ∧ ‖g‖ = ‖f‖
have 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‖
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⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖
have refine : ‖g'‖ = ‖f‖
Tactic: refine ⟨g', g_eq, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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'‖ = ‖f‖
have apply : ‖f‖ ≤ ‖g.mkContinuous ‖f‖ sorry‖
Tactic: apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖ ⋯‖
have refine : ∀ (x : ↥p), Norm.norm (E := ℝ) ((f : (a : ↥p) → ℝ) x : ℝ) ≤ ‖g.mkContinuous ‖f‖ sorry‖ * ‖x‖
Tactic: refine f.opNorm_le_bound (norm_nonneg _) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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 := ℝ) ((f : (a : ↥p) → ℝ) x : ℝ) ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖
have rw : Norm.norm (E := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ≤ ‖g.mkContinuous ‖f‖ sorry‖ * ‖x‖
Tactic: rw [← g_eq]