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

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
⊢ w ≤ w' ↔ w' ≤ w
Tactic:
refine ⟨fun h ↦ (lec_iff _ _).mpr (fun j ↦ ?_), dom_of_gec hE⟩
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
⊢ w' j ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
⊢ w' j ≤ w j
Tactic:
have hw₃ := eval_f_tw w j
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - (d - 1) * w 0 - w j
⊢ w' j ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - (d - 1) * w 0 - w j
⊢ w' j ≤ w j
Tactic:
simp only [hw₁, mul_zero, tsub_zero] at hw₃
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
⊢ w' j ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
⊢ w' j ≤ w j
Tactic:
have h' := h (tw n d j)
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : f w (tw n d j) ≤ f w' (tw n d j)
⊢ w' j ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : f w (tw n d j) ≤ f w' (tw n d j)
⊢ w' j ≤ w j
Tactic:
rw [hw₃, eval_f_tw w' j, hE, Nat.sub_sub, add_comm, ← Nat.sub_sub] at h'
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : E w' - w j ≤ E w' - w' j - (d - 1) * w' 0
⊢ w' j ≤ w j

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
hw₃ : f w (tw n d j) = E w - w j
h' : E w' - w j ≤ E w' - w' j - (d - 1) * w' 0
⊢ w' j ≤ w j
Tactic:
exact (tsub_le_tsub_iff_left (hw'₂ j)).mp (h'.trans $ Nat.sub_le _ _)
State after:
no goals