Theorem: Weight.balanced_of_min' (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
⊢ balanced w
Tactic:
by_contra hb
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
⊢ False

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
⊢ False
Tactic:
obtain ⟨k, hk₁, hk₂⟩ := index_exists hw
State after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
⊢ False

State before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
⊢ False
Tactic:
obtain ⟨hE', hb', hc, hne⟩ :=
  exists_balanced_ltc w hb
    (E_trunc_eq_E_of_dom (hmin _ (trunc_normalized hw).2 w.trunc_dom) hw.1) hk₁
State after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ False

State before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ False
Tactic:
refine hne <| lec_antisymm hc <|
  (dom_iff_gec_of_balanced (trunc_normalized hw).1 hb' hE'.symm).mp <|
  w.trunc_dom.trans <| hmin _ ?_ <| (dom_of_gec hE' hc).trans w.trunc_dom
State after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ Monotone (Function.update (trunc w) k 1)

State before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ Monotone (Function.update (trunc w) k 1)
Tactic:
intro i j hij
State after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ Function.update (trunc w) k 1 i ≤ Function.update (trunc w) k 1 j

State before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ Function.update (trunc w) k 1 i ≤ Function.update (trunc w) k 1 j
Tactic:
simp only [Function.update_apply, trunc_apply]
State after:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (if i = k then 1 else min (w i) (E w)) ≤ if j = k then 1 else min (w j) (E w)

State before:
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (if i = k then 1 else min (w i) (E w)) ≤ if j = k then 1 else min (w j) (E w)
Tactic:
cases' eq_or_ne i k with hi hi <;> cases' eq_or_ne j k with hj hj <;> simp [hi, hj]
State after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
⊢ 1 ≤ w j ∧ 1 ≤ E w

case intro.intro.intro.intro.intro.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j = k
⊢ w i ≤ 1 ∨ E w ≤ 1

case intro.intro.intro.intro.intro.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
⊢ w i ≤ w j ∨ E w ≤ w j

State before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
⊢ 1 ≤ w j ∧ 1 ≤ E w
Tactic:
have : w j = Function.update w k 1 j := by simp only [Function.update_apply, hj, if_false]
State after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j ∧ 1 ≤ E w

State before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j ∧ 1 ≤ E w
Tactic:
refine ⟨?_, one_le_E w⟩
State after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j

State before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j
Tactic:
rw [(Function.update_same k 1 w).symm, this]
State after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ Function.update w k 1 k ≤ Function.update w k 1 j

State before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ Function.update w k 1 k ≤ Function.update w k 1 j
Tactic:
exact hk₂ (le_of_eq_of_le hi.symm hij)
State after:
no goals

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
⊢ w j = Function.update w k 1 j
Tactic:
simp only [Function.update_apply, hj, if_false]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j = k
⊢ w i ≤ 1 ∨ E w ≤ 1
Tactic:
exact Or.inl ((le_of_le_of_eq (hw.2 (le_of_le_of_eq hij hj)) hk₁).trans zero_le_one)
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
cases' le_or_lt w.E (w j) with h h
State after:
case intro.intro.intro.intro.intro.inr.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : E w ≤ w j
⊢ w i ≤ w j ∨ E w ≤ w j

case intro.intro.intro.intro.intro.inr.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : w j < E w
⊢ w i ≤ w j ∨ E w ≤ w j

State before:
case intro.intro.intro.intro.intro.inr.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : E w ≤ w j
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
exact Or.inr h
State after:
no goals

State before:
case intro.intro.intro.intro.intro.inr.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : w j < E w
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
exact Or.inl (hw.2 hij)
State after:
no goals