awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ Set.Finite.{u_3} (α := α) {i_1 : α | Pi.single (M := E) i a i_1 ≠ 0}

Tactic:
(Set.finite_singleton i).subset ?_

Premises used: Set.Finite.subset, Set.finite_singleton
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
refine : Subset (α := Set α) {i_1 : α | Pi.single (M := E) i a i_1 ≠ 0} {i}
⊢ Set.Finite.{u_3} (α := α) {i_1 : α | Pi.single (M := E) i a i_1 ≠ 0}

Tactic:
refine (Set.finite_singleton i).subset ?_

Premises used: Set.Finite.subset, Set.finite_singleton
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
j : α
rw : ¬j = i → Pi.single (M := E) i a j = 0
⊢ ¬Pi.single (M := E) i a j = 0 → j = i

Tactic:
rw [not_imp_comm]

Premises used: not_imp_comm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
j : α
h : ¬j = i
⊢ Pi.single (M := E) i a j = 0

Tactic:
Pi.single_eq_of_ne h _

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p_1 q : ℝ≥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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
j : α
h : ¬j = i
⊢ Pi.single (M := E) i a j = 0

Tactic:
exact Pi.single_eq_of_ne h _

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ (↑(lp.single (E := E) p i a) : (i : α) → E i) = Pi.single (M := E) i a

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
j : α
⊢ (↑(lp.single (E := E) p i a) : (i : α) → E i) j = Pi.single (M := E) i a j

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ (↑(lp.single (E := E) p i a) : (i : α) → E i) i = a

Tactic:
Pi.single_eq_same _ _

Premises used: Function.update, Pi.single, dite, Pi.single_eq_same
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
j : α
hij : j ≠ i
⊢ Eq (α := E j) ((↑(lp.single (E := E) p i a) : (i : α) → E i) j : E j) (0 : E j)

Tactic:
Pi.single_eq_of_ne hij _

Premises used: Function.update, Pi.single_eq_of_ne, Pi.single, dite
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
⊢ Eq (α := ↥(lp E p)) (lp.single (E := E) p i 0) 0

Tactic:
ext <| Pi.single_zero _

Premises used: Pi.single_zero, lp.ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
a b : E i
⊢ lp.single (E := E) p i (a + b) = HAdd.hAdd (α := ↥(lp E p)) (lp.single (E := E) p i a) (lp.single (E := E) p i b)

Tactic:
ext <| Pi.single_add _ _ _

Premises used: Pi.single_add, lp.ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ Eq (α := ↥(lp E p)) (lp.single (E := E) p i (-a)) (-lp.single (E := E) p i a)

Tactic:
ext <| Pi.single_neg _ _

Premises used: lp.ext, Pi.single_neg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
p : ℝ≥0∞
i : α
a b : E i
⊢ lp.single (E := E) p i (a - b) = HSub.hSub (α := ↥(lp E p)) (lp.single (E := E) p i a) (lp.single (E := E) p i b)

Tactic:
ext <| Pi.single_sub _ _ _

Premises used: Pi.single_sub, lp.ext
-- 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)
inst_4 : DecidableEq α
p : ℝ≥0∞
i : α
c : 𝕜
a : E i
⊢ lp.single (E := E) p i (c • a) = HSMul.hSMul (β := ↥(lp E p)) c (lp.single (E := E) p i a)

Tactic:
ext <| Pi.single_smul _ _ _

Premises used: Pi.single_smul, lp.ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
inst : NormedRing 𝕜
inst_1 : DecidableEq α
i : α
h :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := 𝕜) ((↑((zeroBasis : (a : α) → ↥(lp (fun (x : α) ↦ 𝕜) 0)) i) : (i : α) → 𝕜) x : 𝕜)
      ((↑(lp.single (E := fun (x : α) ↦ 𝕜) 0 i 1) : (i : α) → 𝕜) x : 𝕜)
⊢ Eq (α := ↥(lp (fun (x : α) ↦ 𝕜) 0)) ((zeroBasis : (a : α) → ↥(lp (fun (x : α) ↦ 𝕜) 0)) i : ↥(lp (fun (x : α) ↦ 𝕜) 0))
    (lp.single (E := fun (x : α) ↦ 𝕜) 0 i 1 : ↥(lp (fun (x : α) ↦ 𝕜) 0))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
𝕜 : Type u_1
α : Type u_3
inst : NormedRing 𝕜
inst_1 : DecidableEq α
i x : α
⊢ Eq.{u_1 + 1} (α := 𝕜) ((↑((zeroBasis : (a : α) → ↥(lp (fun (x : α) ↦ 𝕜) 0)) i) : (i : α) → 𝕜) x : 𝕜)
    ((↑(lp.single (E := fun (x : α) ↦ 𝕜) 0 i 1) : (i : α) → 𝕜) x : 𝕜)

Tactic:
simp [zeroBasis, Finsupp.single_apply, Pi.single, Function.update, eq_comm]

Premises used: Function.update, Pi.single, eq_comm, lp.zeroBasis, Finsupp.single_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 : (i : α) → E i
s : Finset α
⊢ norm (E := ↥(lp E p)) (∑ i ∈ s, lp.single (E := E) p i (f i)) ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal

Tactic:
(hasSum_norm hp (∑ i ∈ s, lp.single p i (f i))).unique ?_

Premises used: lp.single, lp.hasSum_norm, HasSum.unique, Finset.sum
-- 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 : (i : α) → E i
s : Finset α
refine :
  HasSum (α := ℝ)
    (fun (i : α) ↦ norm.{u_4} (E := E i) ((↑(∑ i ∈ s, lp.single (E := E) p i (f i)) : (i : α) → E i) i) ^ p.toReal)
    (∑ i ∈ s, ‖f i‖ ^ p.toReal)
⊢ norm (E := ↥(lp E p)) (∑ i ∈ s, lp.single (E := E) p i (f i)) ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal

Tactic:
refine (hasSum_norm hp (∑ i ∈ s, lp.single p i (f i))).unique ?_

Premises used: lp.single, lp.hasSum_norm, HasSum.unique, Finset.sum
-- 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 : (i : α) → E i
s : Finset α
simp : HasSum (α := ℝ) (fun (i : α) ↦ ‖if i ∈ s then f i else 0‖ ^ p.toReal) (∑ i ∈ s, ‖f i‖ ^ p.toReal)
⊢ HasSum (α := ℝ)
    (fun (i : α) ↦ norm.{u_4} (E := E i) ((↑(∑ i ∈ s, lp.single (E := E) p i (f i)) : (i : α) → E i) i) ^ p.toReal)
    (∑ i ∈ s, ‖f i‖ ^ p.toReal)

Tactic:
simp only [lp.coeFn_single, coeFn_sum, Finset.sum_apply, Finset.sum_pi_single]

Premises used: lp.coeFn_single, Finset.sum_apply, lp.coeFn_sum, Finset.sum_pi_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 α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
i : α
hi : i ∉ s
⊢ ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0

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

Premises used: Real.zero_rpow, LT.lt.ne', if_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 α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
⊢ ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0

Tactic:
have h : ∀ i ∉ s, ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 := fun i hi ↦ by
    simp [if_neg hi, 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 : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
i : α
hi : i ∈ s
rw rw₁ : ‖f i‖ ^ p.toReal = ‖f i‖ ^ p.toReal
⊢ ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal

Tactic:
rw [if_pos hi]

Premises used: if_pos
-- 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 : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
⊢ ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal

Tactic:
have h' : ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal := by
    intro i hi
    rw [if_pos hi]
-- 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 : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
h' : ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖if i ∈ s then f i else 0‖ ^ p.toReal) (∑ i ∈ s, ‖f i‖ ^ p.toReal)

Tactic:
simpa [Finset.sum_congr rfl h'] using hasSum_sum_of_ne_finset_zero h

Premises used: hasSum_sum_of_ne_finset_zero, 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
i : α
x : E i
⊢ Nonempty α

Tactic:
haveI : Nonempty α := ⟨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 α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
top : ⨆ (i_1 : α), ‖Pi.single (M := E) i x i_1‖ = ‖x‖
⊢ norm (E := ↥(lp E ∞)) (lp.single (E := E) ∞ i x) = ‖x‖

Tactic:
simp only [norm_eq_ciSup, lp.coeFn_single]

Premises used: lp.coeFn_single, lp.norm_eq_ciSup
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ ⨆ (i_1 : α), ‖Pi.single (M := E) i x i_1‖ = ‖x‖

Tactic:
ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, LT.lt.trans_eq, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
top : ∀ (j : α), ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
top₁ : ∀ (n : ℝ) (hn : n < ‖x‖), ‖x‖ = ‖Pi.single (M := E) i x i‖
⊢ ⨆ (i_1 : α), ‖Pi.single (M := E) i x i_1‖ = ‖x‖

Tactic:
refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, LT.lt.trans_eq, Exists.intro
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
j : α
top : ‖Pi.single (M := E) i x i‖ ≤ ‖x‖
top₁ : ∀ (hij : i ≠ j), ‖Pi.single (M := E) i x j‖ ≤ ‖x‖
⊢ ‖Pi.single (M := E) i x j‖ ≤ ‖x‖

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, 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 α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
top top₁ : ‖x‖ ≤ ‖x‖
⊢ ‖Pi.single (M := E) i x i‖ ≤ ‖x‖

Tactic:
rw [Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
j : α
hij : i ≠ j
top : 0 ≤ ‖x‖
⊢ ‖Pi.single (M := E) i x j‖ ≤ ‖x‖

Tactic:
rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]

Premises used: norm_zero, Pi.single_eq_of_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 α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
j : α
hij : i ≠ j
⊢ 0 ≤ ‖x‖

Tactic:
norm_nonneg _

Premises used: 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 α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
j : α
hij : i ≠ j
⊢ 0 ≤ ‖x‖

Tactic:
exact norm_nonneg _

Premises used: 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 α
i : α
x : E i
this : Nonempty α
hp : LT.lt (α := ℝ≥0∞) 0 ∞
n : ℝ
hn : n < ‖x‖
top top₁ : ‖x‖ = ‖x‖
⊢ ‖x‖ = ‖Pi.single (M := E) i x i‖

Tactic:
rw [Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
⊢ 0 < (↑p : ℝ≥0∞).toReal

Tactic:
simpa using hp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
⊢ 0 < (↑p : ℝ≥0∞).toReal

Tactic:
have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
rw : 0 ≤ ‖Pi.single (M := E) i x i‖
coe :
  ∀ (b' : α),
    b' ≠ i →
      norm (E := E b') ((↑(lp.single (E := E) (↑p : ℝ≥0∞) i x) : (i : α) → E i) b' : E b') ^ (↑p : ℝ≥0∞).toReal = 0
⊢ norm (E := ↥(lp E (↑p : ℝ≥0∞))) (lp.single (E := E) (↑p : ℝ≥0∞) i x) = ‖x‖

Tactic:
rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]

Premises used: lp.coeFn_single, LT.lt.ne', one_div, tsum_eq_single, lp.norm_eq_tsum_rpow, Pi.single_eq_same, Real.rpow_rpow_inv
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
⊢ 0 ≤ ‖Pi.single (M := E) i x i‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
⊢ 0 ≤ ‖Pi.single (M := E) i x i‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
E : α → Type u_4
p_1 : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : DecidableEq α
i : α
x : E i
this_1 : Nonempty α
p : ℝ≥0
hp : 0 < (↑p : ℝ≥0∞)
this : 0 < (↑p : ℝ≥0∞).toReal
j : α
hji : j ≠ i
coe : ‖Pi.single (M := E) i x j‖ ^ (↑p : ℝ≥0∞).toReal = 0
coe₁ : norm.{u_4} (E := E j) 0 ^ (↑p : ℝ≥0∞).toReal = 0
coe₂ : HPow.hPow (α := ℝ) 0 (↑p : ℝ≥0∞).toReal = 0
coe₃ coe₄ : Eq (α := ℝ) 0 0
⊢ norm (E := E j) ((↑(lp.single (E := E) (↑p : ℝ≥0∞) i x) : (i : α) → E i) j : E j) ^ (↑p : ℝ≥0∞).toReal = 0

Tactic:
rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']

Premises used: lp.coeFn_single, norm_zero, Pi.single_eq_of_ne, 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
i : α
x : E i
this : Nonempty α
top : ∀ (hp : LT.lt (α := ℝ≥0∞) 0 ∞), norm (E := ↥(lp E ∞)) (lp.single (E := E) ∞ i x) = ‖x‖
coe : ∀ (p : ℝ≥0) (hp : 0 < (↑p : ℝ≥0∞)), norm (E := ↥(lp E (↑p : ℝ≥0∞))) (lp.single (E := E) (↑p : ℝ≥0∞) i x) = ‖x‖
⊢ norm (E := ↥(lp E p)) (lp.single (E := E) p i x) = ‖x‖

Tactic:
induction p with
  | top =>
    simp only [norm_eq_ciSup, lp.coeFn_single]
    refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
    · obtain rfl | hij := Decidable.eq_or_ne i j
      · rw [Pi.single_eq_same]
      · rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]
        exact norm_nonneg _
    · rw [Pi.single_eq_same]
  | coe p =>
    have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
    rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
    · exact norm_nonneg _
    · intro j hji
      rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt, lp.coeFn_single, norm_zero, LT.lt.trans_eq, one_div, tsum_eq_single, Exists.intro, lp.norm_eq_ciSup, Pi.single_eq_same, norm_nonneg, 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 α
inst_2 : Fact (1 ≤ p)
i : α
⊢ Isometry (α := E i) (β := ↥(lp E p)) (lp.single (E := E) p i)

Tactic:
AddMonoidHomClass.isometry_of_norm (lp.singleAddMonoidHom (E := E) p i) fun _ ↦
    lp.norm_single (zero_lt_one.trans_le Fact.out) _ _

Premises used: AddMonoidHomClass.isometry_of_norm, lp.single, zero_lt_one, lp.singleAddMonoidHom, LT.lt.trans_le, lp.norm_single, 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)
i : α
x : E i
⊢ Eq (α := ↥(lp E p)) ((singleContinuousAddMonoidHom E p i : (a : E i) → ↥(lp E p)) x : ↥(lp E p))
    (lp.single (E := E) p i x : ↥(lp E p))

Tactic:
rfl

Premises used: lp.single, 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)
inst_4 : DecidableEq α
inst_5 : Fact (1 ≤ p)
i : α
x : E i
⊢ Eq (α := ↥(lp E p)) ((singleContinuousLinearMap 𝕜 E p i : (a : E i) → ↥(lp E p)) x : ↥(lp E p))
    (lp.single (E := E) p i x : ↥(lp E p))

Tactic:
rfl

Premises used: lp.single, 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 α
⊢ ‖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

Tactic:
((hasSum_norm hp f).sub (hasSum_norm hp (f - ∑ i ∈ s, lp.single p i (f i)))).unique ?_

Premises used: HSub.hSub, lp.single, lp.hasSum_norm, HasSum.unique, Subtype.val, Finset.sum, HasSum.sub
-- 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 α
refine :
  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)
⊢ ‖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

Tactic:
refine ((hasSum_norm hp f).sub (hasSum_norm hp (f - ∑ i ∈ s, lp.single p i (f i)))).unique ?_

Premises used: HSub.hSub, lp.single, lp.hasSum_norm, HasSum.unique, Subtype.val, Finset.sum, HasSum.sub
-- 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
i : α
hi : i ∉ s
this :
  ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑f : (i : α) → E i) i - if i ∈ s then (↑f : (i : α) → E i) i else 0‖ ^ p.toReal =
    0
⊢ F i = 0

Tactic:
simpa only [coeFn_sub, coeFn_sum, lp.coeFn_single, Pi.sub_apply, Finset.sum_apply,
        Finset.sum_pi_single, F] using this

Premises used: lp.coeFn_single, Finset.sum_apply, lp.coeFn_sub, lp.coeFn_sum, Finset.sum_pi_single, 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
i : α
hi : i ∉ s
suffices :
  ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑f : (i : α) → E i) i - if i ∈ s then (↑f : (i : α) → E i) i else 0‖ ^ p.toReal =
    0
⊢ F i = 0

Tactic:
suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by
      simpa only [coeFn_sub, coeFn_sum, lp.coeFn_single, Pi.sub_apply, Finset.sum_apply,
        Finset.sum_pi_single, F] using this
-- 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
i : α
hi : i ∉ s
⊢ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal -
      ‖(↑f : (i : α) → E i) i - if i ∈ s then (↑f : (i : α) → E i) i else 0‖ ^ p.toReal =
    0

Tactic:
simp only [if_neg hi, sub_zero, sub_self]

Premises used: sub_self, sub_zero, if_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 α
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
⊢ ∀ i ∉ s, F i = 0

Tactic:
have hF : ∀ i ∉ s, F i = 0 := by
    intro i hi
    suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by
      simpa only [coeFn_sub, coeFn_sum, lp.coeFn_single, Pi.sub_apply, Finset.sum_apply,
        Finset.sum_pi_single, F] using this
    simp only [if_neg hi, sub_zero, sub_self]