-- Mathlib/Analysis/Matrix.lean
theorem nnnorm_diagonal [DecidableEq n] (v : n → α) : ‖diagonal v‖₊ = ‖v‖₊

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ (Finset.univ.sup fun b => Finset.univ.sup fun b_1 => ‖diagonal v b b_1‖₊) = Finset.univ.sup fun b => ‖v b‖₊

Tactic:
congr 1 with i : 1

Result:
case e_f.h
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ (Finset.univ.sup fun b => ‖diagonal v i b‖₊) = ‖v i‖₊

Proof state:
case e_f.h
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ (Finset.univ.sup fun b => ‖diagonal v i b‖₊) = ‖v i‖₊

Tactic:
refine le_antisymm (Finset.sup_le fun j hj => ?_) ?_

Result:
case e_f.h.refine_1
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊

case e_f.h.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ ≤ Finset.univ.sup fun b => ‖diagonal v i b‖₊

Proof state:
case e_f.h.refine_1.inr
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ 0 ≤ ‖v i‖₊

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case e_f.h.refine_1.inr
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊

Tactic:
rw [diagonal_apply_ne _ hij, nnnorm_zero]

Result:
case e_f.h.refine_1.inr
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ 0 ≤ ‖v i‖₊

Proof state:
case e_f.h.refine_1.inl
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
hj : i ∈ Finset.univ
⊢ ‖diagonal v i i‖₊ ≤ ‖v i‖₊

Tactic:
rw [diagonal_apply_eq]

Result:
no goals

Proof state:
case e_f.h.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ ≤ Finset.univ.sup fun b => ‖diagonal v i b‖₊

Tactic:
refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))

Result:
case e_f.h.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ = ‖diagonal v i i‖₊

Proof state:
case e_f.h.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ = ‖diagonal v i i‖₊

Tactic:
rw [diagonal_apply_eq]

Result:
no goals

Proof state:
case e_f.h.refine_1
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊

Tactic:
obtain rfl | hij := eq_or_ne i j

Result:
case e_f.h.refine_1.inl
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
hj : i ∈ Finset.univ
⊢ ‖diagonal v i i‖₊ ≤ ‖v i‖₊

case e_f.h.refine_1.inr
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊

Proof state:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖v‖₊

Tactic:
simp_rw [nnnorm_def, Pi.nnnorm_def]

Result:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ (Finset.univ.sup fun b => Finset.univ.sup fun b_1 => ‖diagonal v b b_1‖₊) = Finset.univ.sup fun b => ‖v b‖₊