-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_single (hp : 0 < p) (i : α) (x : E i) : ‖lp.single p i x‖ = ‖x‖

Proof state:
case top.refine_1.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
j : α
hij : i ≠ j
⊢ 0 ≤ ‖x‖

Tactic:
exact norm_nonneg _

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ 0 ≤ ‖Pi.single i x i‖

Tactic:
exact norm_nonneg _

Result:
no goals

Proof state:
case top
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
⊢ ‖lp.single ⊤ i x‖ = ‖x‖

Tactic:
simp only [norm_eq_ciSup, lp.coeFn_single]

Result:
case top
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
⊢ ⨆ i_1, ‖Pi.single i x i_1‖ = ‖x‖

Proof state:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ‖lp.single (↑p) 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]

Result:
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ 0 ≤ ‖Pi.single i x i‖

case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ∀ (b' : α), b' ≠ i → ‖↑(lp.single (↑p) i x) b'‖ ^ (↑p).toReal = 0

Proof state:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
j : α
hji : j ≠ i
⊢ ‖↑(lp.single (↑p) i x) j‖ ^ (↑p).toReal = 0

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

Result:
no goals

Proof state:
case top.refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
n : ℝ
hn : n < ‖x‖
⊢ ‖x‖ = ‖Pi.single i x i‖

Tactic:
rw [Pi.single_eq_same]

Result:
no goals

Proof state:
case top.refine_1.inl
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
⊢ ‖Pi.single i x i‖ ≤ ‖x‖

Tactic:
rw [Pi.single_eq_same]

Result:
no goals

Proof state:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ∀ (b' : α), b' ≠ i → ‖↑(lp.single (↑p) i x) b'‖ ^ (↑p).toReal = 0

Tactic:
intro j hji

Result:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
j : α
hji : j ≠ i
⊢ ‖↑(lp.single (↑p) i x) j‖ ^ (↑p).toReal = 0

Proof state:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
⊢ ‖lp.single (↑p) i x‖ = ‖x‖

Tactic:
have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp

Result:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ‖lp.single (↑p) i x‖ = ‖x‖

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p
i : α
x : E i
⊢ ‖lp.single p i x‖ = ‖x‖

Tactic:
haveI : Nonempty α := ⟨i⟩

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p
i : α
x : E i
this : Nonempty α
⊢ ‖lp.single p i x‖ = ‖x‖

Proof state:
case top
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
⊢ ⨆ i_1, ‖Pi.single 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 ?_⟩

Result:
case top.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
j : α
⊢ ‖Pi.single i x j‖ ≤ ‖x‖

case top.refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
n : ℝ
hn : n < ‖x‖
⊢ ‖x‖ = ‖Pi.single i x i‖

Proof state:
case top.refine_1.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
j : α
hij : i ≠ j
⊢ ‖Pi.single i x j‖ ≤ ‖x‖

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

Result:
case top.refine_1.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
j : α
hij : i ≠ j
⊢ 0 ≤ ‖x‖

Proof state:
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
⊢ 0 < (↑p).toReal

Tactic:
simpa using hp

Result:
no goals

Proof state:
case top.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
j : α
⊢ ‖Pi.single i x j‖ ≤ ‖x‖

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

Result:
case top.refine_1.inl
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
⊢ ‖Pi.single i x i‖ ≤ ‖x‖

case top.refine_1.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ⊤
j : α
hij : i ≠ j
⊢ ‖Pi.single i x j‖ ≤ ‖x‖