awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∞
hg : Memℓp (E := E) g ∞
inr :
  ∀ (A : ℝ) (hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A),
    BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)

Tactic:
obtain ⟨A, hA⟩ := hf.bddAbove

Premises used: Memℓp.bddAbove
-- 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 ∞
hg : Memℓp (E := E) g ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
inr :
  ∀ (B : ℝ) (hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖g i‖)) B),
    BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)

Tactic:
obtain ⟨B, hB⟩ := hg.bddAbove

Premises used: Memℓp.bddAbove
-- 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 ∞
hg : Memℓp (E := E) g ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖g i‖)) B
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)

Tactic:
⟨A + B, ?_⟩

Premises used: BddAbove, Set.Nonempty, HAdd.hAdd, Exists.intro
-- 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 ∞
hg : Memℓp (E := E) g ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖g i‖)) B
inr : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(f + g) i‖)) (A + B)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)

Tactic:
refine ⟨A + B, ?_⟩
-- 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 ∞
hg : Memℓp (E := E) g ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖g i‖)) B
i : α
⊢ (fun (i : α) ↦ ‖(f + g) i‖) i ≤ A + B

Tactic:
le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))

Premises used: add_le_add, norm_add_le, Exists.intro, rfl, le_trans
-- 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 ∞
hg : Memℓp (E := E) g ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖g i‖)) B
i : α
⊢ (fun (i : α) ↦ ‖(f + g) i‖) i ≤ A + B

Tactic:
exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))

Premises used: add_le_add, norm_add_le, Exists.intro, rfl, le_trans
-- 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
hp : 0 < p.toReal
inr : Summable (α := ℝ) fun (i : α) ↦ ‖(f + g) i‖ ^ p.toReal
⊢ Memℓp (E := E) (f + g) 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(f + g) i‖ ^ p.toReal

Tactic:
.of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left C)

Premises used: Summable.add, Summable.of_nonneg_of_le, Summable.mul_left, 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
inr : ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal
inr₁ : ∀ (i : α), ‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(f + g) i‖ ^ p.toReal

Tactic:
refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left C)
-- 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
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
b : α
⊢ 0 ≤ ‖(f + g) 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)
f g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
⊢ ‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
(Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans ?_

Premises used: norm_add_le, LT.lt.le, Real.rpow_le_rpow, LE.le.trans, 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
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
inr : (‖f i‖ + ‖g i‖) ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
⊢ ‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
refine (Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans ?_

Premises used: norm_add_le, LT.lt.le, Real.rpow_le_rpow, LE.le.trans, 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
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
inr :
  (‖f i‖ + ‖g i‖) ^ p.toReal ≤
    (if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
dsimp only [C]
-- 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
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
pos : ∀ (h : p.toReal < 1), (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 1 * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
neg :
  ∀ (h : ¬p.toReal < 1),
    (‖f i‖ + ‖g i‖) ^ p.toReal ≤ HPow.hPow (α := ℝ) 2 (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤
    (if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
split_ifs with h
-- 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
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
h : p.toReal < 1
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 1 * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
simpa using NNReal.coe_le_coe.2 (NNReal.rpow_add_le_add_rpow ‖f i‖₊ ‖g i‖₊ hp.le h.le)

Premises used: Iff.mpr, NNNorm.nnnorm, LT.lt.le, NNReal.rpow_add_le_add_rpow, NNReal.coe_le_coe
-- 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
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
h : ¬p.toReal < 1
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
⊢ 1 ≤ p.toReal

Tactic:
simp only [not_lt] at h

Premises used: not_lt
-- 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
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
h : 1 ≤ p.toReal
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ HPow.hPow (α := ℝ) 2 (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
simpa [Fin.sum_univ_succ] using
        Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg Finset.univ h fun i _ => (F i).coe_nonneg

Premises used: Finset.univ, Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg, NNReal.coe_nonneg, Fin.sum_univ_succ
-- 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
rw : Memℓp (E := E) (f + -g) p
⊢ Memℓp (E := E) (f - g) p

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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
⊢ Memℓp (E := E) (f + -g) p

Tactic:
hf.add hg.neg

Premises used: Memℓp.add, Memℓp.neg
-- 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
⊢ Memℓp (E := E) (f + -g) p

Tactic:
exact hf.add hg.neg

Premises used: Memℓp.add, Memℓp.neg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (E := E) (f i) p
haveI : ∀ (this : DecidableEq ι), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
⊢ Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p

Tactic:
haveI : DecidableEq ι := Classical.decEq _
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (E := E) (f i) p
this : DecidableEq ι
revert : ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
⊢ Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p

Tactic:
revert hf
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
refine_1 :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Memℓp (E := E) (f i) p),
    Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p) →
        ∀ (hf : ∀ i ∈ insert a s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a_3 : α) ↦ ∑ i ∈ insert a s, f i a_3) p
⊢ ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Memℓp (E := E) (f i) p),
    Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p

Tactic:
simp only [zero_mem_ℓp', Finset.sum_empty, imp_true_iff]

Premises used: zero_mem_ℓp', imp_true_iff, Finset.sum_empty
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s_1 : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (E := E) (f i_1) p
refine_2 : Memℓp (E := E) (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p
⊢ Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ insert i s, f i a) p

Tactic:
simp only [his, Finset.sum_insert, not_false_iff]

Premises used: Finset.sum_insert, not_false_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s_1 : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (E := E) (f i_1) p
⊢ Memℓp (E := E) (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p

Tactic:
(hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, Memℓp.add
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s_1 : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (E := E) (f i_1) p
⊢ Memℓp (E := E) (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p

Tactic:
exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, Memℓp.add
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥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)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (c • f) 0
inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (c • f) ∞
inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (c • f) p
⊢ Memℓp (E := E) (c • f) p

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

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f 0
inl : Set.Finite.{u_3} (α := α) {i : α | (c • f) i ≠ 0}
⊢ Memℓp (E := E) (c • f) 0

Tactic:
apply memℓp_zero

Premises used: memℓp_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f 0
⊢ Set.Finite.{u_3} (α := α) {i : α | (c • f) i ≠ 0}

Tactic:
hf.finite_dsupport.subset fun i => (?_ : ¬c • f i = 0 → ¬f i = 0)

Premises used: Set.Finite.subset, Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f 0
inl : ∀ (i : α), ¬c • f i = 0 → ¬f i = 0
⊢ Set.Finite.{u_3} (α := α) {i : α | (c • f) i ≠ 0}

Tactic:
refine hf.finite_dsupport.subset fun i => (?_ : ¬c • f i = 0 → ¬f i = 0)

Premises used: Set.Finite.subset, Memℓp.finite_dsupport
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f 0
i : α
⊢ ¬c • f i = 0 → ¬f i = 0

Tactic:
not_imp_not.mpr fun hf' => hf'.symm ▸ smul_zero c

Premises used: Iff.mpr, smul_zero, Eq.rec, Eq.symm, not_imp_not
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f 0
i : α
⊢ ¬c • f i = 0 → ¬f i = 0

Tactic:
exact not_imp_not.mpr fun hf' => hf'.symm ▸ smul_zero c

Premises used: Iff.mpr, not_imp_not
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
inr :
  ∀ (A : ℝ) (hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A), Memℓp (E := E) (c • f) ∞
⊢ Memℓp (E := E) (c • f) ∞

Tactic:
obtain ⟨A, hA⟩ := hf.bddAbove

Premises used: Memℓp.bddAbove
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
⊢ Memℓp (E := E) (c • f) ∞

Tactic:
memℓp_infty ⟨‖c‖ * A, ?_⟩

Premises used: Norm.norm, HMul.hMul, memℓp_infty, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
inr : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(c • f) i‖)) (‖c‖ * A)
⊢ Memℓp (E := E) (c • f) ∞

Tactic:
refine memℓp_infty ⟨‖c‖ * A, ?_⟩

Premises used: Norm.norm, HMul.hMul, memℓp_infty, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
inr : ‖c • f i‖ ≤ ‖c‖ * A
⊢ (fun (i : α) ↦ ‖(c • f) i‖) i ≤ ‖c‖ * A

Tactic:
dsimp only [Pi.smul_apply]

Premises used: Pi.smul_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
⊢ ‖c • f i‖ ≤ ‖c‖ * A

Tactic:
(norm_smul_le _ _).trans ?_

Premises used: norm_smul_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
inr : ‖c‖ * ‖f i‖ ≤ ‖c‖ * A
⊢ ‖c • f i‖ ≤ ‖c‖ * A

Tactic:
refine (norm_smul_le _ _).trans ?_

Premises used: norm_smul_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
inr : ‖f i‖ ≤ A
⊢ ‖c‖ * ‖f i‖ ≤ ‖c‖ * A

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
⊢ ‖f i‖ ≤ A

Tactic:
hA ⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
⊢ ‖f i‖ ≤ A

Tactic:
exact hA ⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥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)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
inr : Summable (α := ℝ) fun (i : α) ↦ ‖(c • f) i‖ ^ p.toReal
⊢ Memℓp (E := E) (c • f) p

Tactic:
apply memℓp_gen

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

Tactic:
dsimp only [Pi.smul_apply]

Premises used: Pi.smul_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥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)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ (↑(‖c‖₊ ^ p.toReal) : ℝ) * ‖f i‖ ^ p.toReal

Tactic:
have := (hf.summable hp).mul_left (↑(‖c‖₊ ^ p.toReal) : ℝ)
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥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)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
this : Summable (α := ℝ) fun (i : α) ↦ (↑(‖c‖₊ ^ p.toReal) : ℝ) * ‖f i‖ ^ p.toReal
inr :
  ∀ (this : Summable (α := ℝ≥0) fun (a : α) ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal),
    Summable (α := ℝ≥0) fun (a : α) ↦ ‖c • f a‖₊ ^ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖c • f i‖ ^ p.toReal

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul, NNReal.summable_coe,
      ← NNReal.mul_rpow] at this ⊢

Premises used: NNReal.summable_coe, NNReal.coe_rpow, coe_nnnorm, NNReal.coe_mul, NNReal.mul_rpow