Theorem: Weight.normalized_of_sorted (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
⊢ normalized (sorted w)
Tactic:
have hm := sorted_is_Monotone w
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ normalized (sorted w)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ normalized (sorted w)
Tactic:
have h₁ : w.sorted ((Tuple.sort w)⁻¹ 0) = 0
State after:
case h₁
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ sorted w ((Tuple.sort w)⁻¹ 0) = 0

n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
h₁ : sorted w ((Tuple.sort w)⁻¹ 0) = 0
⊢ normalized (sorted w)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
h₁ : sorted w ((Tuple.sort w)⁻¹ 0) = 0
⊢ normalized (sorted w)
Tactic:
exact ⟨Nat.eq_zero_of_le_zero (le_of_le_of_eq (hm (Fin.zero_le _)) h₁), sorted_is_Monotone w⟩
State after:
no goals

State before:
case h₁
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ sorted w ((Tuple.sort w)⁻¹ 0) = 0
Tactic:
rwa [sorted, Weight.comp, Function.comp_apply, Equiv.Perm.apply_inv_self]
State after:
no goals