awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.WithLp
Goal:
p : ℝ≥0∞
K : Type u_1
K' : Type u_2
K'' : Type u_3
V : Type u_4
V' : Type u_5
V'' : Type u_6
inst : Semiring K
inst_1 : Semiring K'
inst_2 : Semiring K''
σ : K →+* K'
σ' : K' →+* K
inst_3 : RingHomInvPair σ σ'
inst_4 : RingHomInvPair σ' σ
τ : K' →+* K''
τ' : K'' →+* K'
inst_5 : RingHomInvPair τ τ'
inst_6 : RingHomInvPair τ' τ
ρ : K →+* K''
ρ' : K'' →+* K
inst_7 : RingHomInvPair ρ ρ'
inst_8 : RingHomInvPair ρ' ρ
inst_9 : RingHomCompTriple σ τ ρ
inst_10 : RingHomCompTriple τ' σ' ρ'
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : AddCommGroup V'
inst_14 : Module K' V'
inst_15 : AddCommGroup V''
inst_16 : Module K'' V''
f : V ≃ₛₗ[σ] V'
g : V' ≃ₛₗ[τ] V''
⊢ Eq (α := LinearEquiv.{u_1, u_3, u_4, u_6} ρ (WithLp p V) (WithLp p V'')) (withLpCongr p (f.trans g))
    ((withLpCongr p f).trans (withLpCongr p g))

Tactic:
rfl

Premises used: LinearEquiv.withLpCongr, LinearEquiv.toEquiv, LinearEquiv.trans, rfl, WithLp.linearEquiv
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
rw rw₁ : Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0} ↔ Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
⊢ (if Eq (α := ℝ≥0∞) 0 0 then Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
    else Summable (α := ℝ) fun (i : α) ↦ HPow.hPow (β := ℝ) ‖f i‖ 0) ↔
    Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}

Tactic:
rw [if_pos rfl]

Premises used: if_pos, 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 : Set.Finite.{u_3} (α := α) {i : α | f i ≠ 0}
⊢ Memℓp (E := E) f 0

Tactic:
memℓp_zero_iff.2 hf

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

Tactic:
simp [Memℓp]

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

Tactic:
memℓp_infty_iff.2 hf

Premises used: Iff.mpr, memℓp_infty_iff
-- 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
rw : ∀ (hp : 0 < p ∧ p < ∞) {f : (i : α) → E i}, Memℓp (E := E) f p ↔ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
⊢ Memℓp (E := E) f p ↔ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
rw [ENNReal.toReal_pos_iff] at hp

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : (i : α) → E i
rw :
  (if p = ∞ then BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
    else Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔
    Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
rw₁ rw₂ : (Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
⊢ (if p = 0 then Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
    else
      if p = ∞ then BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
      else Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔
    Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
rw [if_neg hp.1.ne', if_neg hp.2.ne]

Premises used: LT.lt.ne', And.right, And.left, if_neg, LT.lt.ne
-- 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 : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
inl : ∀ (hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0), Memℓp (E := E) f 0
inr : ∀ (hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞), 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 : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 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 : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0
⊢ Summable (α := ℝ) fun (x : α) ↦ 1

Tactic:
simpa using hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0
⊢ Summable (α := ℝ) fun (x : α) ↦ 1

Tactic:
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0
H : Summable (α := ℝ) fun (x : α) ↦ 1
⊢ 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)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0
H : Summable (α := ℝ) fun (x : α) ↦ 1
⊢ Set.Finite.{u_3} (α := α) {i : α | f i ≠ 0}

Tactic:
exact (Set.Finite.of_summable_const (by simp) H).subset (Set.subset_univ _)

Premises used: Set.subset_univ, Set.Finite.subset, Set.Finite.of_summable_const
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞
⊢ Summable (α := ℝ) fun (x : α) ↦ 1

Tactic:
simpa using hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞
⊢ Summable (α := ℝ) fun (x : α) ↦ 1

Tactic:
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞
H : Summable (α := ℝ) fun (x : α) ↦ 1
⊢ 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)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞
H : Summable (α := ℝ) fun (x : α) ↦ 1
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
simpa using ((Set.Finite.of_summable_const (by simp) H).image fun i => ‖f i‖).bddAbove

Premises used: Norm.norm, Set.Finite.image, Set.Finite.bddAbove, Set.Finite.of_summable_const
-- 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 : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
hp : 0 < p.toReal
⊢ Memℓp (E := E) f p

Tactic:
(memℓp_gen_iff hp).2 hf

Premises used: Iff.mpr, memℓp_gen_iff
-- 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 : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
hp : 0 < p.toReal
⊢ Memℓp (E := E) f p

Tactic:
exact (memℓp_gen_iff hp).2 hf

Premises used: Iff.mpr, memℓp_gen_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
hf₁ : 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)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
h : HasSum (α := ℝ) (fun (i : α) ↦ ‖f i‖ ^ p.toReal) (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
use ⨆ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal

Premises used: Finset, ENNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
h : ∀ (i : α), 0 ≤ ‖f i‖ ^ p.toReal
h₁ :
  IsLUB (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)
    (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖f i‖ ^ p.toReal) (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)

Tactic:
apply hasSum_of_isLUB_of_nonneg

Premises used: hasSum_of_isLUB_of_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
b : α
⊢ 0 ≤ ‖f b‖ ^ p.toReal

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
h : BddAbove (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)
⊢ IsLUB (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)
    (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)

Tactic:
apply isLUB_ciSup

Premises used: isLUB_ciSup
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)) C
⊢ BddAbove (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)

Tactic:
use C
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
s : Finset α
⊢ (fun (s : Finset α) ↦ (∑ i ∈ s, ‖f i‖ ^ p.toReal : ℝ)) s ≤ C

Tactic:
hf s
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
s : Finset α
⊢ (fun (s : Finset α) ↦ (∑ i ∈ s, ‖f i‖ ^ p.toReal : ℝ)) s ≤ C

Tactic:
exact hf s
-- 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
hp : 0 < p.toReal
⊢ Memℓp (E := E) f p ↔ ∀ (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)

Tactic:
⟨fun hf ↦ ?_, memℓp_gen'⟩

Premises used: memℓp_gen', Iff.intro
-- 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
hp : 0 < p.toReal
refine :
  ∀ (hf : Memℓp (E := E) f p) (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)
⊢ Memℓp (E := E) f p ↔ ∀ (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)

Tactic:
refine ⟨fun hf ↦ ?_, 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
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
⊢ 0 < p

Tactic:
obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp

Premises used: ENNReal.toReal_pos_iff, Iff.mp
-- 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
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
hp₁ : 0 < p
⊢ p < ∞

Tactic:
obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp

Premises used: ENNReal.toReal_pos_iff, Iff.mp
-- 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
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
hp₁ : 0 < p
hp₂ : p < ∞
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
simp only [Memℓp, hp₁.ne', ↓reduceIte, hp₂.ne] at hf

Premises used: LT.lt.ne', reduceIte, Memℓp, LT.lt.ne
-- 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
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
i : α
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
positivity
-- 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
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
⊢ ∀ (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)

Tactic:
simpa [upperBounds] using isLUB_hasSum (by intro; positivity) hf.hasSum |>.1

Premises used: upperBounds, Summable.hasSum, And.left, isLUB_hasSum
-- 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
hp : 0 < p.toReal
⊢ Memℓp (E := E) f p ↔ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C

Tactic:
⟨fun hf ↦ ?_, fun ⟨C, _, hC⟩ ↦ memℓp_gen' hC⟩

Premises used: memℓp_gen', Iff.intro, _private.0.memℓp_gen_iff''.match_1, Memℓp
-- 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
hp : 0 < p.toReal
refine : ∀ (hf : Memℓp (E := E) f p), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ Memℓp (E := E) f p ↔ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C

Tactic:
refine ⟨fun hf ↦ ?_, fun ⟨C, _, hC⟩ ↦ memℓp_gen' hC⟩
-- 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
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
i : α
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
positivity
-- 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
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
⊢ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C

Tactic:
exact ⟨_, tsum_nonneg fun i ↦ (by positivity), memℓp_gen_iff' hp |>.mp hf⟩
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inl : Memℓp (E := E) 0 0
inr : Memℓp (E := E) 0 ∞
inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) 0 p
⊢ Memℓp (E := E) 0 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)
inl : Set.Finite.{u_3} (α := α) {i : α | Ne.{u_4 + 1} (α := E i) (0 i) 0}
⊢ Memℓp (E := E) 0 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)
⊢ Set.Finite.{u_3} (α := α) {i : α | Ne.{u_4 + 1} (α := E i) (0 i) 0}

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inr : BddAbove (α := ℝ) (Set.range fun (i : α) ↦ 0)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ norm.{u_4} (E := E i) (0 i))

Tactic:
simp only [norm_zero, Pi.zero_apply]

Premises used: norm_zero, Pi.zero_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ 0)

Tactic:
bddAbove_singleton.mono Set.range_const_subset

Premises used: Set.range_const_subset, bddAbove_singleton, BddAbove.mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ 0)

Tactic:
exact bddAbove_singleton.mono Set.range_const_subset

Premises used: Set.range_const_subset, bddAbove_singleton, BddAbove.mono
-- 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
inr : Summable (α := ℝ) fun (i : α) ↦ norm.{u_4} (E := E i) (0 i) ^ p.toReal
⊢ Memℓp (E := E) 0 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)
hp : 0 < p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ norm.{u_4} (E := E i) (0 i) ^ p.toReal

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

Premises used: Real.zero_rpow, LT.lt.ne', summable_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp (E := E) (fun (i : α) ↦ 0) p

Tactic:
zero_memℓp

Premises used: zero_memℓp
-- 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
inl : Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) 0 ↔ Memℓp (E := E) f 0
inr : Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) ∞ ↔ Memℓp (E := E) f ∞
inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) p ↔ Memℓp (E := E) f p
⊢ Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) p ↔ Memℓp (E := E) f p

Tactic:
obtain (rfl | rfl | hp) := p.trichotomy

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
⊢ Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) 0 ↔ Memℓp (E := E) f 0

Tactic:
simp [memℓp_zero_iff]

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

Tactic:
simp [memℓp_infty_iff]

Premises used: memℓp_infty_iff
-- 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
hp : 0 < p.toReal
⊢ Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) p ↔ Memℓp (E := E) f p

Tactic:
simp [memℓp_gen_iff hp]

Premises used: memℓp_gen_iff
-- 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 : Memℓp (E := fun (i : α) ↦ ℝ) g p
hfg : ∀ (i : α), ‖f i‖ ≤ g i
⊢ ∀ (i : α), ‖f i‖ ≤ ‖g i‖

Tactic:
replace hfg (i) : ‖f i‖ ≤ ‖g i‖ := (hfg i).trans (Real.le_norm_self _)
-- 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 : Memℓp (E := fun (i : α) ↦ ℝ) g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
inl : ∀ (hg : Memℓp (E := fun (i : α) ↦ ℝ) g 0), Memℓp (E := E) f 0
inr : ∀ (hg : Memℓp (E := fun (i : α) ↦ ℝ) g ∞), Memℓp (E := E) f ∞
inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) f p
⊢ Memℓp (E := E) f p

Tactic:
obtain (rfl | rfl | hp) := p.trichotomy

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
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp (E := fun (i : α) ↦ ℝ) g 0
inl : ∀ (hg : Set.Finite.{u_3} (α := α) {i : α | 0 < ‖g i‖}), Set.Finite.{u_3} (α := α) {i : α | 0 < ‖f i‖}
⊢ Memℓp (E := E) f 0

Tactic:
simp_rw [memℓp_zero_iff, ← norm_pos_iff] at hg ⊢

Premises used: norm_pos_iff, memℓp_zero_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Set.Finite.{u_3} (α := α) {i : α | 0 < ‖g i‖}
⊢ Set.Finite.{u_3} (α := α) {i : α | 0 < ‖f i‖}

Tactic:
hg.subset fun i hi ↦ hi.trans_le <| hfg i

Premises used: Set.Finite.subset, LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Set.Finite.{u_3} (α := α) {i : α | 0 < ‖g i‖}
⊢ Set.Finite.{u_3} (α := α) {i : α | 0 < ‖f i‖}

Tactic:
refine hg.subset fun i hi ↦ hi.trans_le <| hfg i

Premises used: Set.Finite.subset
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp (E := fun (i : α) ↦ ℝ) g ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖g i‖)

Tactic:
rw [memℓp_infty_iff] at hg ⊢

Premises used: memℓp_infty_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖g i‖)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
hg.range_mono _ hfg

Premises used: BddAbove.range_mono
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖g i‖)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)

Tactic:
exact hg.range_mono _ hfg

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

Tactic:
rw [memℓp_gen_iff hp] at hg ⊢

Premises used: memℓp_gen_iff
-- 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
apply : ∀ (i : α), ‖‖f i‖ ^ p.toReal‖ ≤ ‖g i‖ ^ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal

Tactic:
apply hg.of_norm_bounded fun i ↦ ?_

Premises used: Summable.of_norm_bounded
-- 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 : α
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
positivity
-- 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 : α
rw : ‖f i‖ ^ p.toReal ≤ ‖g i‖ ^ p.toReal
⊢ ‖‖f i‖ ^ p.toReal‖ ≤ ‖g i‖ ^ p.toReal

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)]

Premises used: abs_of_nonneg, Real.norm_eq_abs
-- 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 : α
h₁ : ‖f i‖ ≤ ‖g i‖
⊢ ‖f i‖ ^ p.toReal ≤ ‖g i‖ ^ 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)
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:
hfg i