-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_equiv_symm_single (i : ι) (b : β i) :
    ‖(WithLp.equiv p (∀ i, β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

Proof state:
case top
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ⨆ i_1, ‖Pi.single i b i_1‖₊ = ‖b‖₊

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_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
⊢ ‖Pi.single i b j‖₊ ≤ ‖b‖₊

case top.refine_2
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
n : ℝ≥0
hn : n < ‖b‖₊
⊢ ‖b‖₊ = ‖Pi.single i b i‖₊

Proof state:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
⊢ ‖(WithLp.equiv (↑p) ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

Tactic:
have hp0 : (p : ℝ) ≠ 0 :=
  mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'

Result:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖(WithLp.equiv (↑p) ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
⊢ ‖(WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

Tactic:
haveI : Nonempty ι := ⟨i⟩

Result:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
⊢ ‖(WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

Proof state:
case top.refine_1.inr
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
hij : i ≠ j
⊢ 0 ≤ ‖b‖₊

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case top.refine_1
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
⊢ ‖Pi.single i b j‖₊ ≤ ‖b‖₊

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

Result:
case top.refine_1.inl
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ‖Pi.single i b i‖₊ ≤ ‖b‖₊

case top.refine_1.inr
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
hij : i ≠ j
⊢ ‖Pi.single i b j‖₊ ≤ ‖b‖₊

Proof state:
case top
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ‖(WithLp.equiv ⊤ ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

Tactic:
simp_rw [nnnorm_eq_ciSup, WithLp.equiv_symm_pi_apply]

Result:
case top
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ⨆ i_1, ‖Pi.single i b i_1‖₊ = ‖b‖₊

Proof state:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖(WithLp.equiv (↑p) ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊

Tactic:
rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i,
  WithLp.equiv_symm_pi_apply, Pi.single_eq_same, ← NNReal.rpow_mul, one_div,
  mul_inv_cancel₀ hp0, NNReal.rpow_one]

Result:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ∀ (x : ι), x ≠ i → ‖(WithLp.equiv (↑p) ((i : ι) → β i)).symm (Pi.single i b) x‖₊ ^ ↑p = 0

Proof state:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ∀ (x : ι), x ≠ i → ‖(WithLp.equiv (↑p) ((i : ι) → β i)).symm (Pi.single i b) x‖₊ ^ ↑p = 0

Tactic:
intro j hij

Result:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
j : ι
hij : j ≠ i
⊢ ‖(WithLp.equiv (↑p) ((i : ι) → β i)).symm (Pi.single i b) j‖₊ ^ ↑p = 0

Proof state:
case top.refine_1.inl
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ‖Pi.single i b i‖₊ ≤ ‖b‖₊

Tactic:
rw [Pi.single_eq_same]

Result:
no goals

Proof state:
case top.refine_1.inr
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
hij : i ≠ j
⊢ ‖Pi.single i b j‖₊ ≤ ‖b‖₊

Tactic:
rw [Pi.single_eq_of_ne' hij, nnnorm_zero]

Result:
case top.refine_1.inr
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
hij : i ≠ j
⊢ 0 ≤ ‖b‖₊

Proof state:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
j : ι
hij : j ≠ i
⊢ ‖(WithLp.equiv (↑p) ((i : ι) → β i)).symm (Pi.single i b) j‖₊ ^ ↑p = 0

Tactic:
rw [WithLp.equiv_symm_pi_apply, Pi.single_eq_of_ne hij, nnnorm_zero, NNReal.zero_rpow hp0]

Result:
no goals

Proof state:
case top.refine_2
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
n : ℝ≥0
hn : n < ‖b‖₊
⊢ ‖b‖₊ = ‖Pi.single i b i‖₊

Tactic:
rw [Pi.single_eq_same]

Result:
no goals