awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
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)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
inl : ∀ (hp : Ne (α := ℝ≥0∞) 0 0) (f : ↥(lp E 0)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have inr : ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) (f : ↥(lp E ∞)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hp, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
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)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
inl : ∀ (hp : Ne (α := ℝ≥0∞) 0 0) (f : ↥(lp E 0)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
inr : ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) (f : ↥(lp E ∞)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have inr₁ : ∀ (hp : 0 < p.toReal), ‖c • f‖ ≤ ‖c‖ * ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have inr : IsEmpty α → ‖c • f‖ ≤ ‖c‖ * ‖f‖
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
inr : IsEmpty α → ‖c • f‖ ≤ ‖c‖ * ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have inr₁ : Nonempty α → ‖c • f‖ ≤ ‖c‖ * ‖f‖
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
h : Nonempty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have hfc : IsLUB ((fun (b : ℝ) ↦ ‖c‖ * b) '' Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) (‖c‖ * ‖f‖)
Tactic: have hfc := (lp.isLUB_norm f).mul_left (norm_nonneg c)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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)
c : 𝕜
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
h : Nonempty α
hfc : IsLUB ((fun (b : ℝ) ↦ ‖c‖ * b) '' Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have hfc₁ : IsLUB (Set.range fun (x : α) ↦ ‖c‖ * ‖(↑f : (i : α) → E i) x‖) (‖c‖ * ‖f‖)
Tactic: simp_rw [← Set.range_comp, Function.comp_def] at hfc
Cleared hypotheses: hfc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
Tactic: have coe_nnnorm : ∀ f : lp E p, ↑‖f‖₊ = ‖f‖ := fun _ => rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
this : ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have rwa : ∀ (this : ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊), ‖c • f‖ ≤ ‖c‖ * ‖f‖
Tactic: rwa [NNReal.rpow_le_rpow_iff hp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have inr : ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
Tactic: suffices ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal by
      rwa [NNReal.rpow_le_rpow_iff hp] at this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun (f : ↥(lp E p)) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯ }
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
⊢ ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
have inr : ∀ (inst : NNNorm ↥(lp E p)) (coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖),
  ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
Tactic: clear_value inst
Cleared hypotheses: inst, coe_nnnorm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
⊢ ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
have inr : ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
Tactic: rw [NNReal.mul_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
have hLHS : HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
Tactic: have hLHS := lp.hasSum_norm hp (c • f)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hLHS : HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
have hRHS : HasSum (fun (i : α) ↦ ‖c‖ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)
Tactic: have hRHS := (lp.hasSum_norm hp f).mul_left (‖c‖ ^ p.toReal)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hLHS : HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
hRHS : HasSum (fun (i : α) ↦ ‖c‖ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
have hRHS₁ : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
Tactic: simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul,
      NNReal.hasSum_coe] at hRHS hLHS
Cleared hypotheses: hLHS, hRHS
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hLHS : HasSum (fun (i : α) ↦ ‖(↑(c • f) : (i : α) → E i) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
hRHS : HasSum (fun (i : α) ↦ ‖c‖ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)
hRHS₁ :
  HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
have hLHS₁ : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
Tactic: simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul,
      NNReal.hasSum_coe] at hRHS hLHS
Cleared hypotheses: hLHS, hRHS
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
have inr : ∀ (i : α), ‖(↑(c • f) : (i : α) → E i) i‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖₊ ^ p.toReal
Tactic: refine hasSum_mono hLHS hRHS fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
⊢ ‖(↑(c • f) : (i : α) → E i) i‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) i‖₊ ^ p.toReal
have inr : ‖c • (↑f : (i : α) → E i) i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖(↑f : (i : α) → E i) i‖₊) ^ p.toReal
Tactic: rw [← NNReal.mul_rpow, lp.coeFn_smul, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst_1 : (i : α) → NormedAddCommGroup (E i)
inst_2 : NormedRing 𝕜
inst_3 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_4 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp_1 : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), (↑‖f‖₊ : ℝ) = ‖f‖
hRHS : HasSum (fun (a : α) ↦ ‖c‖₊ ^ p.toReal * ‖(↑f : (i : α) → E i) a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun (a : α) ↦ ‖(↑(c • f) : (i : α) → E i) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
⊢ ‖c • (↑f : (i : α) → E i) i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖(↑f : (i : α) → E i) i‖₊) ^ p.toReal
have inr : ‖c • (↑f : (i : α) → E i) i‖₊ ≤ ‖c‖₊ * ‖(↑f : (i : α) → E i) i‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
⊢ ∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i =
    HAdd.hAdd (α := E) (∑' (i : α), (↑f : (i : α) → (fun (x : α) ↦ E) i) i)
      (∑' (i : α), (↑g : (i : α) → (fun (x : α) ↦ E) i) i)
have rw : Eq.{u_5 + 1} (α := E) (∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i)
  (∑' (b : α), ((↑f : (i : α) → (fun (x : α) ↦ E) i) b + (↑g : (i : α) → (fun (x : α) ↦ E) i) b))
Tactic: rw [← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
rw :
  Eq.{u_5 + 1} (α := E) (∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i)
    (∑' (b : α), ((↑f : (i : α) → (fun (x : α) ↦ E) i) b + (↑g : (i : α) → (fun (x : α) ↦ E) i) b))
⊢ ∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i =
    HAdd.hAdd (α := E) (∑' (i : α), (↑f : (i : α) → (fun (x : α) ↦ E) i) i)
      (∑' (i : α), (↑g : (i : α) → (fun (x : α) ↦ E) i) i)
have hf : Summable (↑f : (i : α) → (fun (x : α) ↦ E) i)
Tactic: rw [← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
f g : ↥(lp (fun (x : α) ↦ E) 1)
rw :
  Eq.{u_5 + 1} (α := E) (∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i)
    (∑' (b : α), ((↑f : (i : α) → (fun (x : α) ↦ E) i) b + (↑g : (i : α) → (fun (x : α) ↦ E) i) b))
hf : Summable (↑f : (i : α) → (fun (x : α) ↦ E) i)
⊢ ∑' (i : α), (↑(f + g) : (i : α) → (fun (x : α) ↦ E) i) i =
    HAdd.hAdd (α := E) (∑' (i : α), (↑f : (i : α) → (fun (x : α) ↦ E) i) i)
      (∑' (i : α), (↑g : (i : α) → (fun (x : α) ↦ E) i) i)
have hg : Summable (↑g : (i : α) → (fun (x : α) ↦ E) i)
Tactic: rw [← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E_1 : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E_1 i)
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : CompleteSpace E
c : 𝕜
f : ↥(lp (fun (x : α) ↦ E) 1)
⊢ ∑' (i : α), (↑(c • f) : (i : α) → (fun (x : α) ↦ E) i) i =
    HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (∑' (i : α), (↑f : (i : α) → (fun (x : α) ↦ E) i) i)
have simp : ∑' (i : α), (c • (↑f : (i : α) → E)) i =
  HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (∑' (i : α), (↑f : (i : α) → E) i)
Tactic: simp only [coeFn_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
⊢ ‖c • f‖ = ‖c‖ * ‖f‖
have inl : ‖HSMul.hSMul (α := 𝕜) 0 f‖ = norm.{u_1} (E := 𝕜) 0 * ‖f‖
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
inl : ‖HSMul.hSMul (α := 𝕜) 0 f‖ = norm.{u_1} (E := 𝕜) 0 * ‖f‖
⊢ ‖c • f‖ = ‖c‖ * ‖f‖
have inr : ∀ (hc : c ≠ 0), ‖c • f‖ = ‖c‖ * ‖f‖
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c • f‖ = ‖c‖ * ‖f‖
have inr : ‖c‖ * ‖f‖ ≤ ‖c • f‖
Tactic: refine le_antisymm (norm_const_smul_le hp c f) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖
have this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
Tactic: have := mul_le_mul_of_nonneg_left (norm_const_smul_le hp c⁻¹ (c • f)) (norm_nonneg c)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖
have inr : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)), ‖c‖ * ‖f‖ ≤ ‖c • f‖
Tactic: rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
inr : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)), ‖c‖ * ‖f‖ ≤ ‖c • f‖
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖
have inr₁ : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c‖ * (‖c‖⁻¹ * ‖c • f‖)), ‖c‖ * ‖f‖ ≤ ‖c • f‖
Tactic: rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedDivisionRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hc : c ≠ 0
this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)
inr : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)), ‖c‖ * ‖f‖ ≤ ‖c • f‖
inr₁ : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c‖ * (‖c‖⁻¹ * ‖c • f‖)), ‖c‖ * ‖f‖ ≤ ‖c • f‖
⊢ ‖c‖ * ‖f‖ ≤ ‖c • f‖
have inr₂ : ∀ (this : ‖c‖ * ‖f‖ ≤ ‖c • f‖), ‖c‖ * ‖f‖ ≤ ‖c • f‖
Tactic: rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
⊢ Memℓp (E := E) (star f) p
have inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (star f) 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (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) (star f) 0
⊢ Memℓp (E := E) (star f) p
have inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (star f) ∞
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (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) (star f) 0
inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (star f) ∞
⊢ Memℓp (E := E) (star f) p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (star f) p
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f 0
⊢ Memℓp (E := E) (star f) 0
have inl : Set.Finite.{u_3} (α := α) {i : α | star f i ≠ 0}
Tactic: apply memℓp_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
hp : 0 < p.toReal
⊢ Memℓp (E := E) (star f) p
have inr : Summable (α := ℝ) fun (i : α) ↦ ‖star f i‖ ^ p.toReal
Tactic: apply memℓp_gen
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (1 ≤ p)
f : ↥(lp E p)
⊢ ‖star f‖ = ‖f‖
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (f : ↥(lp E 0)), ‖star f‖ = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, hp, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (1 ≤ p)
f : ↥(lp E p)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (f : ↥(lp E 0)), ‖star f‖ = ‖f‖
⊢ ‖star f‖ = ‖f‖
have inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : ↥(lp E ∞)), ‖star f‖ = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, hp, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (1 ≤ p)
f : ↥(lp E p)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (f : ↥(lp E 0)), ‖star f‖ = ‖f‖
inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f : ↥(lp E ∞)), ‖star f‖ = ‖f‖
⊢ ‖star f‖ = ‖f‖
have inr₁ : ∀ (h : 0 < p.toReal), ‖star f‖ = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : (i : α) → StarAddMonoid (E i)
inst_2 : ∀ (i : α), NormedStarGroup.{u_4} (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
f : ↥(lp E 0)
⊢ ‖star f‖ = ‖f‖
have inl : False
Tactic: exfalso