awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ :=
  fun (i : α) ↦
    ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
i : α
hi : i ∈ s
⊢ F i = ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
have simp : norm.{u_4} (E := E i) 0 ^ p.toReal = 0
Tactic: simp only [F, coeFn_sum, lp.single_apply, if_pos hi, sub_self, coeFn_sub,
      Pi.sub_apply, Finset.sum_apply, Finset.sum_pi_single, sub_eq_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ :=
  fun (i : α) ↦
    ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
⊢ HasSum (α := ℝ)
    (fun (b : α) ↦
      ‖(↑f : (i : α) → E i) b‖ ^ p.toReal -
        ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) b‖ ^ p.toReal)
    (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
have hF' : ∀ i ∈ s, F i = ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: have hF' : ∀ i ∈ s, F i = ‖f i‖ ^ p.toReal := by
    intro i hi
    simp only [F, coeFn_sum, lp.single_apply, if_pos hi, sub_self, coeFn_sub,
      Pi.sub_apply, Finset.sum_apply, Finset.sum_pi_single, sub_eq_self]
    simp [Real.zero_rpow hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ :=
  fun (i : α) ↦
    ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
hF' : ∀ i ∈ s, F i = ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ HasSum (α := ℝ)
    (fun (b : α) ↦
      ‖(↑f : (i : α) → E i) b‖ ^ p.toReal -
        ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) b‖ ^ p.toReal)
    (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
have this : HasSum F (∑ i ∈ s, F i)
Tactic: have : HasSum F (∑ i ∈ s, F i) := hasSum_sum_of_ne_finset_zero 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 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ :=
  fun (i : α) ↦
    ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
hF' : ∀ i ∈ s, F i = ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
this : HasSum F (∑ i ∈ s, F i)
⊢ HasSum (α := ℝ)
    (fun (b : α) ↦
      ‖(↑f : (i : α) → E i) b‖ ^ p.toReal -
        ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) b‖ ^ p.toReal)
    (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
have rwa : ∀ (this : HasSum F (∑ x ∈ s, ‖(↑f : (i : α) → E i) x‖ ^ p.toReal)),
  HasSum (α := ℝ)
    (fun (b : α) ↦
      ‖(↑f : (i : α) → E i) b‖ ^ p.toReal -
        ‖(↑(f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)) : (i : α) → E i) b‖ ^ p.toReal)
    (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
Tactic: rwa [Finset.sum_congr rfl hF'] 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 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal =
    ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
have linarith : ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal <
    ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal →
  ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal -
        (‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) +
      (‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal -
        ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) =
    0
Tactic: linarith [lp.norm_sub_norm_compl_sub_single hp f s]
-- 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 : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
linarith :
  ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal <
      ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal →
    ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal -
          (‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) +
        (‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal -
          ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) =
      0
⊢ ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal =
    ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
have linarith₁ : ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal <
    ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal →
  ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
        ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal +
      -(‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i)‖ ^ p.toReal -
          ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) =
    0
Tactic: linarith [lp.norm_sub_norm_compl_sub_single hp f s]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
⊢ HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑f : (i : α) → E i) i)) f
have hp₀ : 0 < p
Tactic: have hp₀ : 0 < p := zero_lt_one.trans_le Fact.out
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
⊢ HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑f : (i : α) → E i) i)) f
have hp' : 0 < p.toReal
Tactic: have hp' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
⊢ HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑f : (i : α) → E i) i)) f
have this : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
Tactic: have := lp.hasSum_norm hp' f
-- 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 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
⊢ HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑f : (i : α) → E i) i)) f
have rw : ∀
  (this :
    ∀ ε > 0,
      ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
        dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε),
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f < ε
Tactic: rw [HasSum, Metric.tendsto_nhds] 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 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
    dist (∑ b ∈ x, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f < ε
have refine : ∀ (x : Finset α),
  dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal →
    dist (∑ b ∈ x, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f < ε
Tactic: refine (this _ (Real.rpow_pos_of_pos hε p.toReal)).mono ?_
-- 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 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f < ε
have rw : dist (∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f ^ p.toReal < ε ^ p.toReal
Tactic: rw [← Real.rpow_lt_rpow_iff dist_nonneg (le_of_lt hε) hp']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f ^ p.toReal < ε ^ p.toReal
have hs₁ : dist (‖f‖ ^ p.toReal) (∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) < ε ^ p.toReal
Tactic: rw [dist_comm] at hs
Cleared hypotheses: hs
-- 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 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (‖f‖ ^ p.toReal) (∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f ^ p.toReal < ε ^ p.toReal
have simp : ∀ (hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal| < ε ^ p.toReal),
  ‖∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b) - f‖ ^ p.toReal < ε ^ p.toReal
Tactic: simp only [dist_eq_norm, Real.norm_eq_abs] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal| < ε ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b) - f‖ ^ p.toReal < ε ^ p.toReal
have H : ‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal =
  ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: have H : ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal =
      ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖f i‖ ^ p.toReal := by
    simpa only [coeFn_neg, Pi.neg_apply, lp.single_neg, Finset.sum_neg_distrib, neg_sub_neg,
      norm_neg, _root_.norm_neg] using lp.norm_compl_sum_single hp' (-f) s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal| < ε ^ p.toReal
H :
  ‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal =
    ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b) - f‖ ^ p.toReal < ε ^ p.toReal
have hs₁ : |‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal| < ε ^ p.toReal
Tactic: rw [← H] at hs
Cleared hypotheses: hs, H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
inst_2 : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal| < ε ^ p.toReal
H :
  ‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal =
    ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b) - f‖ ^ p.toReal < ε ^ p.toReal
have this₁ : |‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal| =
  ‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal
Tactic: have : |‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal| =
      ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal := by
    simp only [Real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm]
-- 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 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
⊢ f = g
have h₁ : ∀ (x : ↥(lp E p)), Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
have this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x
Tactic: have := lp.hasSum_single hp x
-- 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 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
have h₁ : Eq.{u_5 + 1} (α := F)
  (∑' (b : α),
    Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
      (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
  (∑' (b : α),
    Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
      (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
Tactic: rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
-- 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 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x
⊢ Eq.{u_5 + 1} (α := F)
    (∑' (b : α),
      Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
        (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
    (∑' (b : α),
      Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
        (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
have h₁ : ∀ (i : α),
  Eq.{u_5 + 1} (α := F)
    (Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
      (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) i)
    (Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
      (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) i)
Tactic: congr! 2 with i
-- 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 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
have h₁ : ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x),
  Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
Tactic: classical
  have := lp.hasSum_single hp x
  rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
  congr! 2 with i
  exact DFunLike.congr_fun (h i) (x i)
-- 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 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
h₁ h₂ h₃ :
  ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x),
    Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
have h₄ : ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x),
  Eq.{u_5 + 1} (α := F)
    (∑' (b : α),
      Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
        (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
    (∑' (b : α),
      Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
        (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
Tactic: classical
  have := lp.hasSum_single hp x
  rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
  congr! 2 with i
  exact DFunLike.congr_fun (h i) (x i)
-- 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 : DecidableEq α
F : Type u_5
inst_2 : AddCommMonoid F
inst_3 : TopologicalSpace F
inst_4 : T2Space F
inst_5 : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
h₁ h₂ h₃ :
  ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x),
    Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
h₄ :
  ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x),
    Eq.{u_5 + 1} (α := F)
      (∑' (b : α),
        Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
          (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
      (∑' (b : α),
        Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
          (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) b)
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)
have h₅ : ∀ (this : HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x) (i : α),
  Eq.{u_5 + 1} (α := F)
    (Function.comp (β := ↥(lp E p)) (⇑f : (a : ↥(lp E p)) → F)
      (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) i)
    (Function.comp (β := ↥(lp E p)) (⇑g : (a : ↥(lp E p)) → F)
      (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) i)
Tactic: classical
  have := lp.hasSum_single hp x
  rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
  congr! 2 with i
  exact DFunLike.congr_fun (h i) (x i)
-- 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_1 q_1 : ℝ≥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)
p q r : ℝ≥0∞
h : p ≤ q
x x_1 : ↥(lp E p)
⊢ Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x + x_1) : PreLp E)
      ⋯ =
    HAdd.hAdd (α := ↥(lp E q))
      (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x : PreLp E) ⋯)
      (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x_1 : PreLp E) ⋯)
have h₁ : ∀ (x_2 : α),
  (↑(Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x + x_1) : PreLp E)
            sorry) :
        (i : α) → E i)
      x_2 =
    (↑(HAdd.hAdd (α := ↥(lp E q))
            (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x : PreLp E)
              sorry)
            (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
              (↑x_1 : PreLp E) sorry)) :
        (i : α) → E i)
      x_2
Tactic: ext
-- 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_1 q_1 : ℝ≥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)
p q r : ℝ≥0∞
h : p ≤ q
x : 𝕜
x_1 : ↥(lp E p)
⊢ Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x • x_1) : PreLp E)
      ⋯ =
    HSMul.hSMul (α := 𝕜) (β := ↥(lp E q)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑x_1 : PreLp E) ⋯)
have h₁ : ∀ (x_2 : α),
  (↑(Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x) (↑(x • x_1) : PreLp E)
            sorry) :
        (i : α) → E i)
      x_2 =
    (↑(HSMul.hSMul (α := 𝕜) (β := ↥(lp E q)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
            (Subtype.mk (p := fun (x : PreLp E) ↦ Membership.mem (γ := AddSubgroup (PreLp E)) (lp E q) x)
              (↑x_1 : PreLp E) sorry)) :
        (i : α) → E i)
      x_2
Tactic: ext