Theorem: Weight.trunc_pair_eq_pair (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ pair (trunc w) a = pair w a
Tactic:
simp only [pair, trunc_apply]
State after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ ∑ x : Fin (Nat.succ n), a x * min (w x) (E w) = ∑ j : Fin (Nat.succ n), a j * w j

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ ∑ x : Fin (Nat.succ n), a x * min (w x) (E w) = ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
congr
State after:
case e_f
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ (fun x => a x * min (w x) (E w)) = fun j => a j * w j

State before:
case e_f
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ (fun x => a x * min (w x) (E w)) = fun j => a j * w j
Tactic:
ext j
State after:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ a j * min (w j) (E w) = a j * w j

State before:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ a j * min (w j) (E w) = a j * w j
Tactic:
simp only [mul_eq_mul_left_iff, min_eq_left_iff]
State after:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ w j ≤ E w ∨ a j = 0

State before:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ w j ≤ E w ∨ a j = 0
Tactic:
cases' le_or_lt (w j) w.E with h' h'
State after:
case e_f.h.inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : w j ≤ E w
⊢ w j ≤ E w ∨ a j = 0

case e_f.h.inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : E w < w j
⊢ w j ≤ E w ∨ a j = 0

State before:
case e_f.h.inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : w j ≤ E w
⊢ w j ≤ E w ∨ a j = 0
Tactic:
exact Or.inl h'
State after:
no goals

State before:
case e_f.h.inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : E w < w j
⊢ w j ≤ E w ∨ a j = 0
Tactic:
exact Or.inr <| Nat.eq_zero_of_le_zero (h j h')
State after:
no goals