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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
⊢ ∃ k w', w = w' + k • 1 ∧ normalized w'
Tactic:
have h : ∀ i, w 0 ≤ w i := fun _ ↦ hw bot_le
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ ∃ k w', w = w' + k • 1 ∧ normalized w'

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ ∃ k w', w = w' + k • 1 ∧ normalized w'
Tactic:
refine ⟨w 0, fun i ↦ w i - w 0, ?_, ?_, fun i j hij ↦ ?_⟩
State after:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ w = (fun i => w i - w 0) + w 0 • 1

case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ (fun i => w i - w 0) 0 = 0

case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (fun i => w i - w 0) i ≤ (fun i => w i - w 0) j

State before:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ w = (fun i => w i - w 0) + w 0 • 1
Tactic:
ext i
State after:
case refine_1.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i : Fin (Nat.succ n)
⊢ w i = ((fun i => w i - w 0) + w 0 • 1) i

State before:
case refine_1.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i : Fin (Nat.succ n)
⊢ w i = ((fun i => w i - w 0) + w 0 • 1) i
Tactic:
simp only [ge_iff_le, add_apply, smul_apply, one_apply, mul_one, Nat.sub_add_cancel (h i)]
State after:
no goals

State before:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ (fun i => w i - w 0) 0 = 0
Tactic:
exact Nat.sub_self (w 0)
State after:
no goals

State before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (fun i => w i - w 0) i ≤ (fun i => w i - w 0) j
Tactic:
simpa only [ge_iff_le, tsub_le_iff_right, Nat.sub_add_cancel (h j)] using hw hij
State after:
no goals