awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q : ℝ≥0∞
h : p ≤ q
f : ↥(lp E p)
⊢ (↑((linearMapOfLE 𝕜 E h : (a : ↥(lp E p)) → ↥(lp E q)) f) : (i : α) → E i) = (↑f : (i : α) → E i)
have h₁ : ∀ (x : α), (↑((linearMapOfLE 𝕜 E h : (a : ↥(lp E p)) → ↥(lp E q)) f) : (i : α) → E i) x = (↑f : (i : α) → E i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q : ℝ≥0∞
h : p ≤ q
⊢ Eq (α := ↥(lp E p) →+ ↥(lp E q))
    (LinearMap.toAddMonoidHom (modM₁ := instModuleSubtypePreLpMemAddSubgroup (E := E)) (linearMapOfLE 𝕜 E h))
    (AddSubgroup.inclusion ⋯)
have h₁ : ∀ (x : ↥(lp E p)) (x_1 : α),
  Eq.{u_4 + 1} (α := E x_1)
    ((↑((LinearMap.toAddMonoidHom (modM₁ := instModuleSubtypePreLpMemAddSubgroup (E := E)) (linearMapOfLE 𝕜 E h) :
              (a : ↥(lp E p)) → ↥(lp E q))
            x) :
        (i : α) → E i)
      x_1)
    ((↑((AddSubgroup.inclusion sorry : (a : ↥(lp E p)) → ↥(lp E q)) x) : (i : α) → E i) x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
hpq : p ≤ q
hqr : q ≤ r
⊢ Eq (α := ↥(lp E p) →ₗ[𝕜] ↥(lp E r)) (linearMapOfLE 𝕜 E hqr ∘ₗ linearMapOfLE 𝕜 E hpq) (linearMapOfLE 𝕜 E ⋯)
have h : ∀ (x : ↥(lp E p)) (x_1 : α),
  Eq.{u_4 + 1} (α := E x_1)
    ((↑((linearMapOfLE 𝕜 E hqr ∘ₗ linearMapOfLE 𝕜 E hpq : (a : ↥(lp E p)) → ↥(lp E r)) x) : (i : α) → E i) x_1)
    ((↑((linearMapOfLE 𝕜 E sorry : (a : ↥(lp E p)) → ↥(lp E r)) x) : (i : α) → E i) x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
p q r : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
i : α
x : ↥(lp E p)
⊢ norm.{u_4} (E := E i) ((evalₗ E p i : (a : ↥(lp E p)) → E i) x : E i) ≤ 1 * ‖x‖
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := zero_lt_one.trans_le Fact.out |>.ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
a : α
⊢ ‖f a‖ ≤ C
have this : Tendsto (fun (k : ι) ↦ ‖(↑(F k) : (i : α) → E i) a‖) l (𝓝 ‖f a‖)
Tactic: have : Tendsto (fun k => ‖F k a‖) l (𝓝 ‖f a‖) :=
    (Tendsto.comp (continuous_apply a).continuousAt hf).norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
a : α
this : Tendsto (fun (k : ι) ↦ ‖(↑(F k) : (i : α) → E i) a‖) l (𝓝 ‖f a‖)
⊢ ‖f a‖ ≤ C
have refine : ∀ (x : ι), ‖F x‖ ≤ C → ‖(↑(F x) : (i : α) → E i) a‖ ≤ C
Tactic: refine le_of_tendsto this (hCF.mono ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
have hp' : p ≠ 0
Tactic: have hp' : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
have hp'' : 0 < p.toReal
Tactic: have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp' hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
⊢ Continuous[Pi.topologicalSpace, _] G
have refine : ∀ i ∈ s, Continuous[Pi.topologicalSpace, _] fun (f : (a : α) → E a) ↦ ‖f i‖ ^ p.toReal
Tactic: refine continuous_finsetSum s ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
a : α
h : a ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun (f : (a : α) → E a) ↦ ‖f a‖ ^ p.toReal
have this : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : (a : α) → E a) ↦ f a
Tactic: have : Continuous fun f : ∀ a, E a => f a := continuous_apply a
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
have hG : Continuous[Pi.topologicalSpace, _] G
Tactic: have hG : Continuous G := by
    refine continuous_finsetSum s ?_
    intro a _
    have : Continuous fun f : ∀ a, E a => f a := continuous_apply a
    exact this.norm.rpow_const fun _ => Or.inr hp''.le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
have refine : ∀ᶠ (c : ι) in l, (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) c ≤ C ^ p.toReal
Tactic: refine le_of_tendsto (hG.continuousAt.tendsto.comp hf) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
⊢ ∀ᶠ (c : ι) in l, (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) c ≤ C ^ p.toReal
have refine : ∀ (x : ι), ‖F x‖ ≤ C → (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) x ≤ C ^ p.toReal
Tactic: refine hCF.mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
k : ι
hCFk : ‖F k‖ ≤ C
⊢ (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) k ≤ C ^ p.toReal
have refine : ‖F k‖ ^ p.toReal ≤ C ^ p.toReal
Tactic: refine (lp.sum_rpow_le_norm_rpow hp'' (F k) s).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
k : ι
hCFk : ‖F k‖ ≤ C
⊢ ‖F k‖ ^ p.toReal ≤ C ^ p.toReal
have h : 0 ≤ ‖F k‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
G : ((a : α) → E a) → ℝ := fun (f : (a : α) → E a) ↦ ∑ a ∈ s, ‖f a‖ ^ p.toReal
hG : Continuous[Pi.topologicalSpace, _] G
k : ι
hCFk : ‖F k‖ ≤ C
h : 0 ≤ ‖F k‖
⊢ ‖F k‖ ^ p.toReal ≤ C ^ p.toReal
have h₂ : 0 ≤ p.toReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
⊢ ‖f‖ ≤ C
have obtain : ∀ (i : ι) (hi : ‖F i‖ ≤ C), ‖f‖ ≤ C
Tactic: obtain ⟨i, hi⟩ := hCF.exists
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
i : ι
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C
have hC : 0 ≤ C
Tactic: have hC : 0 ≤ C := (norm_nonneg _).trans hi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
⊢ ‖f‖ ≤ C
have inl : ∀ [_i : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] {F : ι → ↥(lp E ∞)} (hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) {f : ↥(lp E ∞)}
  (hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))) (hi : ‖F i‖ ≤ C), ‖f‖ ≤ C
Tactic: rcases eq_top_or_lt_top p with (rfl | hp)
Cleared hypotheses: p, _i, F, hCF, f, hf, hi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
inl :
  ∀ [_i : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] {F : ι → ↥(lp E ∞)} (hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) {f : ↥(lp E ∞)}
    (hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))) (hi : ‖F i‖ ≤ C), ‖f‖ ≤ C
⊢ ‖f‖ ≤ C
have inr : ∀ (hp : p < ∞), ‖f‖ ≤ C
Tactic: rcases eq_top_or_lt_top p with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ∞)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C
have inl : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
Tactic: apply norm_le_of_forall_le hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
⊢ ‖f‖ ≤ C
have this : 0 < p
Tactic: have : 0 < p := zero_lt_one.trans_le _i.elim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
this : 0 < p
⊢ ‖f‖ ≤ C
have hp' : 0 < p.toReal
Tactic: have hp' : 0 < p.toReal := ENNReal.toReal_pos this.ne' hp.ne
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 (↑f : (i : α) → E i))
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
this : 0 < p
hp' : 0 < p.toReal
⊢ ‖f‖ ≤ C
have inr : ∀ (s : Finset α), ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal
Tactic: apply norm_le_of_forall_sum_le hp' hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
⊢ Memℓp (E := E) f p
have obtain : ∀ (C : ℝ) (hCF : ∀ (k : ι), ‖F k‖ ≤ C), Memℓp (E := E) f p
Tactic: obtain ⟨C, hCF⟩ : ∃ C, ∀ k, ‖F k‖ ≤ C := hF.exists_norm_le.imp fun _ ↦ Set.forall_mem_range.1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp (E := E) f p
have inl : ∀ [_i : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] {F : ι → ↥(lp E ∞)} (hF : Bornology.IsBounded (Set.range F))
  (hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)) (hCF : ∀ (k : ι), ‖F k‖ ≤ C), Memℓp (E := E) f ∞
Tactic: rcases eq_top_or_lt_top p with (rfl | hp)
Cleared hypotheses: p, _i, F, hF, hf, hCF
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
inl :
  ∀ [_i : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] {F : ι → ↥(lp E ∞)} (hF : Bornology.IsBounded (Set.range F))
    (hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)) (hCF : ∀ (k : ι), ‖F k‖ ≤ C), Memℓp (E := E) f ∞
⊢ Memℓp (E := E) f p
have inr : ∀ (hp : p < ∞), Memℓp (E := E) f p
Tactic: rcases eq_top_or_lt_top p with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
f : (a : α) → E a
C : ℝ
_i : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
F : ι → ↥(lp E ∞)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) C
Tactic: use C
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) l (𝓝 f)
C : ℝ
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ∞
⊢ Memℓp (E := E) f p
have inr : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
Tactic: apply memℓp_gen'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑(F i) : (i : α) → E i)) atTop (𝓝 (↑f : (i : α) → E i))
⊢ Tendsto F atTop (𝓝 f)
have rw : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f i
Tactic: rw [Metric.nhds_basis_closedBall.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑(F i) : (i : α) → E i)) atTop (𝓝 (↑f : (i : α) → E i))
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f ε
have hε' : Membership.mem (γ := Filter (↥(lp E p) × ↥(lp E p))) (uniformity ↥(lp E p))
  {p_1 : ↥(lp E p) × ↥(lp E p) | ‖p_1.1 - p_1.2‖ < ε}
Tactic: have hε' : { p : lp E p × lp E p | ‖p.1 - p.2‖ < ε } ∈ uniformity (lp E p) :=
    NormedAddCommGroup.uniformity_basis_dist.mem_of_mem hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑(F i) : (i : α) → E i)) atTop (𝓝 (↑f : (i : α) → E i))
ε : ℝ
hε : 0 < ε
hε' :
  Membership.mem (γ := Filter (↥(lp E p) × ↥(lp E p))) (uniformity ↥(lp E p))
    {p_1 : ↥(lp E p) × ↥(lp E p) | ‖p_1.1 - p_1.2‖ < ε}
⊢ ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f ε
have refine : ∀ (x : ℕ),
  (∀ᶠ (l : ℕ) in atTop,
      Membership.mem (γ := SetRel ↥(lp E p) ↥(lp E p)) {p_1 : ↥(lp E p) × ↥(lp E p) | ‖p_1.1 - p_1.2‖ < ε} (F x, F l)) →
    F x ∈ Metric.closedBall f ε
Tactic: refine (hF.eventually_eventually hε').mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑(F i) : (i : α) → E i)) atTop (𝓝 (↑f : (i : α) → E i))
ε : ℝ
hε : 0 < ε
hε' :
  Membership.mem (γ := Filter (↥(lp E p) × ↥(lp E p))) (uniformity ↥(lp E p))
    {p_1 : ↥(lp E p) × ↥(lp E p) | ‖p_1.1 - p_1.2‖ < ε}
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, norm (E := ↥(lp E p)) ((fun (f : ↥(lp E p)) ↦ F n - f) (F l)) < ε
⊢ F n ∈ Metric.closedBall f ε
have rw : ‖F n - f‖ ≤ ε
Tactic: rw [mem_closedBall_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑(F i) : (i : α) → E i)) atTop (𝓝 (↑f : (i : α) → E i))
ε : ℝ
hε : 0 < ε
hε' :
  Membership.mem (γ := Filter (↥(lp E p) × ↥(lp E p))) (uniformity ↥(lp E p))
    {p_1 : ↥(lp E p) × ↥(lp E p) | ‖p_1.1 - p_1.2‖ < ε}
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, norm (E := ↥(lp E p)) ((fun (f : ↥(lp E p)) ↦ F n - f) (F l)) < ε
⊢ ‖F n - f‖ ≤ ε
have refine : Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑((fun (f : ↥(lp E p)) ↦ F n - f) (F i)) : (i : α) → E i)) atTop
  (𝓝 (↑(F n - f) : (i : α) → E i))
Tactic: refine norm_le_of_tendsto (hn.mono fun k hk => hk.le) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑(F i) : (i : α) → E i)) atTop (𝓝 (↑f : (i : α) → E i))
ε : ℝ
hε : 0 < ε
hε' :
  Membership.mem (γ := Filter (↥(lp E p) × ↥(lp E p))) (uniformity ↥(lp E p))
    {p_1 : ↥(lp E p) × ↥(lp E p) | ‖p_1.1 - p_1.2‖ < ε}
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, norm (E := ↥(lp E p)) ((fun (f : ↥(lp E p)) ↦ F n - f) (F l)) < ε
⊢ Tendsto (α := ℕ) (id fun (i : ℕ) ↦ (↑((fun (f : ↥(lp E p)) ↦ F n - f) (F i)) : (i : α) → E i)) atTop
    (𝓝 (↑(F n - f) : (i : α) → E i))
have rw : ∀ (x : α),
  Tendsto (fun (i : ℕ) ↦ id (fun (i : ℕ) ↦ (↑((fun (f : ↥(lp E p)) ↦ F n - f) (F i)) : (i : α) → E i)) i x) atTop
    (𝓝 ((↑(F n - f) : (i : α) → E i) x))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
inst_2 : ∀ (a : α), CompleteSpace.{u_4} (E a)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
⊢ ∃ (a : ↥(lp E p)), Tendsto F atTop (𝓝 a)
have obtain : ∀ (f : (i : α) → E i)
  (hf :
    Tendsto (Subtype.val (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E p) x) ∘ F) atTop
      (𝓝 f)),
  ∃ (a : ↥(lp E p)), Tendsto F atTop (𝓝 a)
Tactic: obtain ⟨f, hf⟩ := cauchySeq_tendsto_of_complete
      ((uniformContinuous_coe (p := p)).comp_cauchySeq hF)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst_1 : l.NeBot
_i : Fact (1 ≤ p)
inst_2 : ∀ (a : α), CompleteSpace.{u_4} (E a)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : (i : α) → E i
hf :
  Tendsto (Subtype.val (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E p) x) ∘ F) atTop
    (𝓝 f)
⊢ ∃ (a : ↥(lp E p)), Tendsto F atTop (𝓝 a)
have hf' : Memℓp (E := E) f p
Tactic: have hf' : Memℓp f p := memℓp_of_tendsto hF.isBounded_range hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ : α
hga₀b : Memℓp (E := fun (i : ι) ↦ ℝ) (g a₀) ∞
a : α
⊢ Memℓp (E := fun (i : ι) ↦ ℝ) (g a) ∞
have rcases : ∀ (M : ℝ) (hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M),
  Memℓp (E := fun (i : ι) ↦ ℝ) (g a) ∞
Tactic: rcases hga₀b with ⟨M, hM⟩
Cleared hypotheses: hga₀b