awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
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
simp : norm.{u_4} (E := E i) 0 ^ p.toReal = 0
⊢ F i = ‖(↑f : (i : α) → E i) i‖ ^ p.toReal

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]

Premises used: sub_self, Finset.sum_apply, sub_eq_self, lp.coeFn_sub, if_pos, lp.coeFn_sum, Finset.sum_pi_single, lp.single_apply, Pi.sub_apply
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ norm.{u_4} (E := E i) 0 ^ p.toReal = 0

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

Premises used: Real.zero_rpow, LT.lt.ne'
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
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 ∈ 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']
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 F (∑ i ∈ s, F i)

Tactic:
have : HasSum F (∑ i ∈ s, F i) := hasSum_sum_of_ne_finset_zero hF
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
rwa rwa₁ rwa₂ 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)
⊢ 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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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
⊢ ‖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

Tactic:
linarith [lp.norm_sub_norm_compl_sub_single hp f s]

Premises used: lp.norm_sub_norm_compl_sub_single
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
⊢ 0 < p

Tactic:
have hp₀ : 0 < p := zero_lt_one.trans_le Fact.out
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ 0 < p.toReal

Tactic:
have hp' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
have := lp.hasSum_norm hp' f
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
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 < ε
⊢ HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑f : (i : α) → E i) i)) f

Tactic:
rw [HasSum, Metric.tendsto_nhds] at this ⊢

Premises used: Metric.tendsto_nhds, HasSum, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 < ε

Tactic:
(this _ (Real.rpow_pos_of_pos hε p.toReal)).mono ?_

Premises used: Real.rpow_pos_of_pos, Filter.Eventually.mono, ENNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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 < ε
⊢ ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
    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 ?_

Premises used: Real.rpow_pos_of_pos, Filter.Eventually.mono, ENNReal.toReal
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
rw : dist (∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f ^ p.toReal < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b)) f < ε

Tactic:
rw [← Real.rpow_lt_rpow_iff dist_nonneg (le_of_lt hε) hp']

Premises used: dist_nonneg, le_of_lt, Real.rpow_lt_rpow_iff
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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 (‖f‖ ^ p.toReal) (∑ b ∈ s, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) < ε ^ p.toReal

Tactic:
rw [dist_comm] at hs

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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
⊢ dist (∑ 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 ⊢

Premises used: dist_eq_norm, 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)
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
⊢ ‖∑ 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:
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

Premises used: lp.single_neg, lp.norm_compl_sum_single, lp.norm_neg, norm_neg, neg_sub_neg, lp.coeFn_neg, Finset.sum_neg_distrib, Pi.neg_apply, Neg.neg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ ‖∑ 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
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ |‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal| < ε ^ p.toReal

Tactic:
rw [← H] at hs
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
hs₁ : |‖∑ i ∈ s, lp.single (E := E) p i ((↑f : (i : α) → E i) i) - f‖ ^ p.toReal| < ε ^ p.toReal
⊢ ‖∑ 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:
rw [← H] at hs
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ |‖∑ 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:
simp only [Real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm]

Premises used: Real.abs_rpow_of_nonneg, abs_norm, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
⊢ |‖∑ 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]
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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_1 :
  ∀ ε > 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
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
⊢ ‖∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b) - f‖ ^ p.toReal < ε ^ p.toReal

Tactic:
this ▸ hs

Premises used: ENNReal.ofNNReal, Eq.rec, WithTop.some
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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_1 :
  ∀ ε > 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
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
⊢ ‖∑ b ∈ s, lp.single (E := E) p b ((↑f : (i : α) → E i) b) - f‖ ^ p.toReal < ε ^ p.toReal

Tactic:
exact this ▸ hs
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
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)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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)
⊢ HasSum (fun (i : α) ↦ lp.single (E := E) p i ((↑x : (i : α) → E i) i)) x

Tactic:
have := lp.hasSum_single hp x
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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)
⊢ Eq.{u_5 + 1} (α := F) ((f : (a : ↥(lp E p)) → F) x : F) ((g : (a : ↥(lp E p)) → F) x : F)

Tactic:
rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]

Premises used: ContinuousMap.continuous, HasSum.map, ContinuousAddMonoidHom.toContinuousMap, HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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)
⊢ 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:
congr! 2 with i
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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:
DFunLike.congr_fun (h i) (x i)

Premises used: DFunLike.congr_fun, lp.single, Subtype.val
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
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
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:
exact DFunLike.congr_fun (h i) (x i)

Premises used: DFunLike.congr_fun, Subtype.val