awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
refine : ‖F k‖ ^ p.toReal ≤ C ^ p.toReal
⊢ (G ∘ id fun (i : ι) ↦ (↑(F i) : (i : α) → E i)) k ≤ C ^ p.toReal

Tactic:
refine (lp.sum_rpow_le_norm_rpow hp'' (F k) s).trans ?_

Premises used: lp.sum_rpow_le_norm_rpow, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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‖
h₂ : 0 ≤ p.toReal
⊢ ‖F k‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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))
obtain : ∀ (i : ι) (hi : ‖F i‖ ≤ C), ‖f‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
obtain ⟨i, hi⟩ := hCF.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ 0 ≤ C

Tactic:
have hC : 0 ≤ C := (norm_nonneg _).trans hi
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
inr : ∀ (hp : p < ∞), ‖f‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
rcases eq_top_or_lt_top p with (rfl | hp)

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
inl : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
apply norm_le_of_forall_le hC

Premises used: lp.norm_le_of_forall_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C

Tactic:
norm_apply_le_of_tendsto hCF hf

Premises used: lp.norm_apply_le_of_tendsto
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C

Tactic:
exact norm_apply_le_of_tendsto hCF hf

Premises used: lp.norm_apply_le_of_tendsto
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 < ∞
⊢ 0 < p

Tactic:
have : 0 < p := zero_lt_one.trans_le _i.elim
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ 0 < p.toReal

Tactic:
have hp' : 0 < p.toReal := ENNReal.toReal_pos this.ne' hp.ne
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
inr : ∀ (s : Finset α), ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ‖f‖ ≤ C

Tactic:
apply norm_le_of_forall_sum_le hp' hC

Premises used: lp.norm_le_of_forall_sum_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
sum_rpow_le_of_tendsto hp.ne hCF hf

Premises used: lp.sum_rpow_le_of_tendsto, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
exact sum_rpow_le_of_tendsto hp.ne hCF hf

Premises used: lp.sum_rpow_le_of_tendsto, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 : ℝ), ∀ (k : ι), ‖F k‖ ≤ C

Tactic:
hF.exists_norm_le.imp fun _ ↦ Set.forall_mem_range.1

Premises used: Exists.imp, Bornology.IsBounded.exists_norm_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
obtain : ∀ (C : ℝ) (hCF : ∀ (k : ι), ‖F k‖ ≤ C), Memℓp (E := E) f p
⊢ 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

Premises used: Set.forall_mem_range, Exists.imp, Iff.mp, Bornology.IsBounded.exists_norm_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 ∞
inr : ∀ (hp : p < ∞), Memℓp (E := E) f p
⊢ Memℓp (E := E) f p

Tactic:
rcases eq_top_or_lt_top p with (rfl | hp)

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) C
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
use C
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
a : α
⊢ (fun (i : α) ↦ ‖f i‖) a ≤ C

Tactic:
norm_apply_le_of_tendsto (Eventually.of_forall hCF) hf a

Premises used: Filter.Eventually.of_forall, lp.norm_apply_le_of_tendsto
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
a : α
⊢ (fun (i : α) ↦ ‖f i‖) a ≤ C

Tactic:
exact norm_apply_le_of_tendsto (Eventually.of_forall hCF) hf a

Premises used: Filter.Eventually.of_forall, lp.norm_apply_le_of_tendsto
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 < ∞
inr : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
inr₁ : ℝ
⊢ Memℓp (E := E) f p

Tactic:
apply memℓp_gen'

Premises used: memℓp_gen'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 < ∞
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
sum_rpow_le_of_tendsto hp.ne (Eventually.of_forall hCF) hf

Premises used: lp.sum_rpow_le_of_tendsto, Filter.Eventually.of_forall, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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))
rw : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f i
⊢ Tendsto F atTop (𝓝 f)

Tactic:
rw [Metric.nhds_basis_closedBall.tendsto_right_iff]

Premises used: Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 < ε
⊢ 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ε
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 ε

Tactic:
(hF.eventually_eventually hε').mono ?_

Premises used: CauchySeq.eventually_eventually, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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‖ < ε}
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 ε
⊢ ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f ε

Tactic:
refine (hF.eventually_eventually hε').mono ?_

Premises used: CauchySeq.eventually_eventually, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)) < ε
rw : ‖F n - f‖ ≤ ε
⊢ F n ∈ Metric.closedBall f ε

Tactic:
rw [mem_closedBall_iff_norm]

Premises used: mem_closedBall_iff_norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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‖ ≤ ε

Tactic:
norm_le_of_tendsto (hn.mono fun k hk => hk.le) ?_

Premises used: LT.lt.le, lp.norm_le_of_tendsto, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)) < ε
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))
⊢ ‖F n - f‖ ≤ ε

Tactic:
refine norm_le_of_tendsto (hn.mono fun k hk => hk.le) ?_

Premises used: LT.lt.le, lp.norm_le_of_tendsto, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)) < ε
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))
⊢ 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:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)) < ε
a : α
⊢ Tendsto (fun (i : ℕ) ↦ id (fun (i : ℕ) ↦ (↑((fun (f : ↥(lp E p)) ↦ F n - f) (F i)) : (i : α) → E i)) i a) atTop
    (𝓝 ((↑(F n - f) : (i : α) → E i) a))

Tactic:
(hf.apply_nhds a).const_sub (F n a)

Premises used: Filter.Tendsto.const_sub, Filter.Tendsto.apply_nhds, Subtype.val
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)) < ε
a : α
⊢ Tendsto (fun (i : ℕ) ↦ id (fun (i : ℕ) ↦ (↑((fun (f : ↥(lp E p)) ↦ F n - f) (F i)) : (i : α) → E i)) i a) atTop
    (𝓝 ((↑(F n - f) : (i : α) → E i) a))

Tactic:
exact (hf.apply_nhds a).const_sub (F n a)

Premises used: Filter.Tendsto.const_sub, Filter.Tendsto.apply_nhds, Subtype.val
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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)
⊢ ∃ (a : ↥(lp E p)), Tendsto F atTop (𝓝 a)

Tactic:
obtain ⟨f, hf⟩ := cauchySeq_tendsto_of_complete
      ((uniformContinuous_coe (p := p)).comp_cauchySeq hF)

Premises used: cauchySeq_tendsto_of_complete, lp.uniformContinuous_coe, UniformContinuous.comp_cauchySeq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
⊢ Memℓp (E := E) f p

Tactic:
have hf' : Memℓp f p := memℓp_of_tendsto hF.isBounded_range hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
hf' : Memℓp (E := E) f p
⊢ ∃ (a : ↥(lp E p)), Tendsto F atTop (𝓝 a)

Tactic:
⟨⟨f, hf'⟩, tendsto_lp_of_tendsto_pi hF hf⟩

Premises used: Subtype.mk, Exists.intro, lp.tendsto_lp_of_tendsto_pi
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
hf' : Memℓp (E := E) f p
⊢ ∃ (a : ↥(lp E p)), Tendsto F atTop (𝓝 a)

Tactic:
exact ⟨⟨f, hf'⟩, tendsto_lp_of_tendsto_pi hF hf⟩
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 : α
rcases :
  ∀ (M : ℝ) (hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M),
    Memℓp (E := fun (i : ι) ↦ ℝ) (g a) ∞
⊢ Memℓp (E := fun (i : ι) ↦ ℝ) (g a) ∞

Tactic:
rcases hga₀b with ⟨M, hM⟩
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a i‖)) ((↑K : ℝ) * dist a a₀ + M)
⊢ Memℓp (E := fun (i : ι) ↦ ℝ) (g a) ∞

Tactic:
use ↑K * dist a a₀ + M

Premises used: Dist.dist
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ |g a i| = |g a i - g a₀ i + g a₀ i|

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ |g a i - g a₀ i + g a₀ i| ≤ |g a i - g a₀ i| + |g a₀ i|

Tactic:
abs_add_le _ _

Premises used: abs_add_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
h₁ : |g a i - g a₀ i| ≤ (↑K : ℝ) * dist a a₀
h₂ : |g a₀ i| ≤ M
⊢ |g a i - g a₀ i| + |g a₀ i| ≤ (↑K : ℝ) * dist a a₀ + M

Tactic:
gcongr