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)
f : (i : α) → E i
g : α → ℝ
hg : Summable (α := ℝ) fun (i : α) ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ ‖f i‖ ≤ ‖g i‖

Tactic:
exact hfg i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
f : (i : α) → E i
g : (i : α) → F i
hg : Memℓp (E := F) g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
⊢ Memℓp (E := E) f p

Tactic:
hg.norm.mono hfg

Premises used: Memℓp.mono, Memℓp.norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f 0
⊢ Set.Finite.{u_3} (α := α) {i : α | f i ≠ 0}

Tactic:
memℓp_zero_iff.1 hf

Premises used: memℓp_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
memℓp_infty_iff.1 hf

Premises used: memℓp_infty_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : (i : α) → E i
hf : Memℓp (E := E) f p
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
(memℓp_gen_iff hp).1 hf

Premises used: memℓp_gen_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
x : α → E
hx : Memℓp (E := fun (i : α) ↦ E) x 1
⊢ Summable (α := ℝ) fun (a : α) ↦ ‖x a‖

Tactic:
simpa using hx.summable

Premises used: Memℓp.summable
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (-f) 0
inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (-f) ∞
inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (-f) p
⊢ Memℓp (E := E) (-f) p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f 0
inl : Set.Finite.{u_3} (α := α) {i : α | (-f) i ≠ 0}
⊢ Memℓp (E := E) (-f) 0

Tactic:
apply memℓp_zero

Premises used: memℓp_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f 0
⊢ Set.Finite.{u_3} (α := α) {i : α | (-f) i ≠ 0}

Tactic:
simp [hf.finite_dsupport]

Premises used: Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(-f) i‖)

Tactic:
simpa using hf.bddAbove

Premises used: Memℓp.bddAbove
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
hp : 0 < p.toReal
inr : Summable (α := ℝ) fun (i : α) ↦ ‖(-f) i‖ ^ p.toReal
⊢ 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)
f : (i : α) → E i
hf : Memℓp (E := E) f p
hp : 0 < p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(-f) i‖ ^ p.toReal

Tactic:
simpa using hf.summable hp

Premises used: Memℓp.summable
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (E := E) (-f) p ↔ Memℓp (E := E) f p

Tactic:
⟨fun h => neg_neg f ▸ h.neg, Memℓp.neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, Memℓp.neg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
inl : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 0), Memℓp (E := E) f 0
inr : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 ∞), Memℓp (E := E) f ∞
inr₁ : ∀ (hp : 0 < p.toReal) (hfq : Memℓp (E := E) f 0) (hpq : 0 ≤ p), Memℓp (E := E) f p
inr₂ : ∀ (hfq : Memℓp (E := E) f ∞) (hpq : LE.le (α := ℝ≥0∞) ∞ ∞), Memℓp (E := E) f ∞
inr₃ : ∀ (hq : 0 < q.toReal) (hpq : q ≤ ∞), Memℓp (E := E) f ∞
inr₄ : ∀ (hq : 0 < q.toReal), 0 < p.toReal → ∀ (hpq' : q.toReal ≤ p.toReal), Memℓp (E := E) f p
⊢ Memℓp (E := E) f p

Tactic:
rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)

Premises used: ENNReal.trichotomy₂, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 0
⊢ Memℓp (E := E) f 0

Tactic:
hfq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 0
⊢ Memℓp (E := E) f 0

Tactic:
exact hfq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
inr :
  ∀ (C : ℝ) (hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C),
    BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
obtain ⟨C, hC⟩ := (hfq.finite_dsupport.image fun i => ‖f i‖).bddAbove

Premises used: Norm.norm, Set.Finite.image, Set.Finite.bddAbove, Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) (max 0 C)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
use max 0 C

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
i : α
pos : ∀ (hi : f i = 0), (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C
neg : ∀ (hi : ¬f i = 0), (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C

Tactic:
by_cases hi : f i = 0
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
i : α
hi : f i = 0
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C

Tactic:
simp [hi]
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
i : α
hi : ¬f i = 0
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C

Tactic:
(hC ⟨i, hi, rfl⟩).trans (le_max_right _ _)

Premises used: le_max_right, And.intro, Exists.intro, LE.le.trans, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
i : α
hi : ¬f i = 0
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C

Tactic:
exact (hC ⟨i, hi, rfl⟩).trans (le_max_right _ _)

Premises used: le_max_right, And.intro, Exists.intro, LE.le.trans, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp (E := E) f 0
hpq : 0 ≤ p
inr : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
⊢ 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
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp (E := E) f 0
hpq : 0 ≤ p
i : α
hi : i ∉ ⋯.toFinset (s := {i : α | f i ≠ 0})
⊢ f i = 0

Tactic:
simpa using hi
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp (E := E) f 0
hpq : 0 ≤ p
i : α
hi : i ∉ ⋯.toFinset (s := {i : α | f i ≠ 0})
⊢ f i = 0

Tactic:
have : f i = 0 := by simpa using hi
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp (E := E) f 0
hpq : 0 ≤ p
i : α
hi : i ∉ ⋯.toFinset (s := {i : α | f i ≠ 0})
this : f i = 0
⊢ ‖f i‖ ^ p.toReal = 0

Tactic:
simp [this, Real.zero_rpow hp.ne']

Premises used: Real.zero_rpow, LT.lt.ne'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp (E := E) f 0
hpq : 0 ≤ p
⊢ ∀ i ∉ ⋯.toFinset (s := {i : α | f i ≠ 0}), ‖f i‖ ^ p.toReal = 0

Tactic:
have : ∀ i ∉ hfq.finite_dsupport.toFinset, ‖f i‖ ^ p.toReal = 0 := by
      intro i hi
      have : f i = 0 := by simpa using hi
      simp [this, Real.zero_rpow hp.ne']
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp (E := E) f 0
hpq : 0 ≤ p
this : ∀ i ∉ ⋯.toFinset (s := {i : α | f i ≠ 0}), ‖f i‖ ^ p.toReal = 0
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
summable_of_ne_finset_zero this

Premises used: summable_of_ne_finset_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp (E := E) f 0
hpq : 0 ≤ p
this : ∀ i ∉ ⋯.toFinset (s := {i : α | f i ≠ 0}), ‖f i‖ ^ p.toReal = 0
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
exact summable_of_ne_finset_zero this

Premises used: summable_of_ne_finset_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f ∞
hpq : LE.le (α := ℝ≥0∞) ∞ ∞
⊢ Memℓp (E := E) f ∞

Tactic:
hfq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f ∞
hpq : LE.le (α := ℝ≥0∞) ∞ ∞
⊢ Memℓp (E := E) f ∞

Tactic:
exact hfq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
inr :
  ∀ (A : ℝ) (hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A),
    BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite

Premises used: Summable.tendsto_cofinite_zero, Memℓp.summable, Filter.Tendsto.bddAbove_range_of_cofinite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) (A ^ q.toReal⁻¹)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
use A ^ q.toReal⁻¹

Premises used: ENNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A
i : α
⊢ 0 ≤ ‖f i‖ ^ q.toReal

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A
i : α
⊢ 0 ≤ ‖f i‖ ^ q.toReal

Tactic:
have : 0 ≤ ‖f i‖ ^ q.toReal := by positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A
i : α
this : 0 ≤ ‖f i‖ ^ q.toReal
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ A ^ q.toReal⁻¹

Tactic:
simpa [← Real.rpow_mul, mul_inv_cancel₀ hq.ne'] using
      Real.rpow_le_rpow this (hA ⟨i, rfl⟩) (inv_nonneg.mpr hq.le)

Premises used: Iff.mpr, mul_inv_cancel₀, LT.lt.le, LT.lt.ne', inv_nonneg, Exists.intro, Real.rpow_le_rpow, Real.rpow_mul, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
inr : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
⊢ 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
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal

Tactic:
have hf' := hfq.summable hq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
.of_norm_bounded_eventually hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_)

Premises used: Set.Finite.subset, Summable.of_norm_bounded_eventually
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
inr : Set.Finite.{u_3} (α := α) {i : α | 1 ≤ ‖f i‖}
inr₁ : Subset.{u_3} (α := Set α) {x : α | (fun (i : α) ↦ ‖‖f i‖ ^ p.toReal‖ ≤ ‖f i‖ ^ q.toReal) x}ᶜ {i : α | 1 ≤ ‖f i‖}
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
refine .of_norm_bounded_eventually hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
⊢ Set.Finite.{u_3} (α := α) {x : α | 1 ≤ ‖f x‖ ^ q.toReal}

Tactic:
simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)

Premises used: Filter.Tendsto.eventually_lt_const, Summable.tendsto_cofinite_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
⊢ Set.Finite.{u_3} (α := α) {x : α | 1 ≤ ‖f x‖ ^ q.toReal}

Tactic:
have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by
        simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
H : Set.Finite.{u_3} (α := α) {x : α | 1 ≤ ‖f x‖ ^ q.toReal}
⊢ Set.Finite.{u_3} (α := α) {i : α | 1 ≤ ‖f i‖}

Tactic:
H.subset fun i hi => Real.one_le_rpow hi hq.le

Premises used: LT.lt.le, Set.Finite.subset, Real.one_le_rpow
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
H : Set.Finite.{u_3} (α := α) {x : α | 1 ≤ ‖f x‖ ^ q.toReal}
⊢ Set.Finite.{u_3} (α := α) {i : α | 1 ≤ ‖f i‖}

Tactic:
exact H.subset fun i hi => Real.one_le_rpow hi hq.le

Premises used: LT.lt.le, Set.Finite.subset, Real.one_le_rpow
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
i : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
i : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
have : 0 ≤ ‖f i‖ ^ p.toReal := by positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
i : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
this : 0 ≤ ‖f i‖ ^ p.toReal
⊢ ¬‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal

Tactic:
simp only [abs_of_nonneg, this] at hi

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
i : α
this : 0 ≤ ‖f i‖ ^ p.toReal
hi : ¬‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal
inr : ∀ (hi : ‖f i‖ < 1), ‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal
⊢ 1 ≤ ‖f i‖

Tactic:
contrapose! hi
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
i : α
this : 0 ≤ ‖f i‖ ^ p.toReal
hi : ‖f i‖ < 1
⊢ ‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal

Tactic:
Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'

Premises used: LT.lt.le, Real.rpow_le_rpow_of_exponent_ge', norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
i : α
this : 0 ≤ ‖f i‖ ^ p.toReal
hi : ‖f i‖ < 1
⊢ ‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal

Tactic:
exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'

Premises used: LT.lt.le, Real.rpow_le_rpow_of_exponent_ge', norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
inl : ∀ (hf : Memℓp (E := E) f 0) (hg : Memℓp (E := E) g 0), Memℓp (E := E) (f + g) 0
inr : ∀ (hf : Memℓp (E := E) f ∞) (hg : Memℓp (E := E) g ∞), Memℓp (E := E) (f + g) ∞
inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (f + g) p
⊢ Memℓp (E := E) (f + g) p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
inl : Set.Finite.{u_3} (α := α) {i : α | (f + g) i ≠ 0}
⊢ Memℓp (E := E) (f + g) 0

Tactic:
apply memℓp_zero

Premises used: memℓp_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
⊢ Set.Finite.{u_3} (α := α) {i : α | (f + g) i ≠ 0}

Tactic:
(hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_

Premises used: Set.Finite.union, Set.Finite.subset, Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
inl :
  ∀ (i : α),
    Membership.mem (γ := Set α) {i : α | (f + g) i ≠ 0} i →
      Membership.mem (γ := Set α) ({i : α | f i ≠ 0} ∪ {i : α | g i ≠ 0}) i
⊢ Set.Finite.{u_3} (α := α) {i : α | (f + g) i ≠ 0}

Tactic:
refine (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_

Premises used: Set.Finite.union, Set.Finite.subset, Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
i : α
inl : ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0
⊢ Membership.mem (γ := Set α) {i : α | (f + g) i ≠ 0} i →
    Membership.mem (γ := Set α) ({i : α | f i ≠ 0} ∪ {i : α | g i ≠ 0}) i

Tactic:
simp only [Pi.add_apply, Ne, Set.mem_union, Set.mem_setOf_eq]

Premises used: Set.mem_union, Ne, Set.mem_setOf_eq, Pi.add_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
i : α
inl : f i = 0 ∧ g i = 0 → f i + g i = 0
⊢ ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0

Tactic:
contrapose!
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
i : α
hf' : f i = 0
hg' : g i = 0
⊢ f i + g i = 0

Tactic:
simp [hf', hg']