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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
⊢ balanced w
Tactic:
by_contra hb
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
hb : ¬balanced w
⊢ False

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

State before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hmin : ∀ u ≤ w, w ≤ u
hb : ¬balanced w
hE' : E (Function.update (trunc w) 0 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) 0 1)
hc : trunc w ≤ Function.update (trunc w) 0 1
hne : trunc w ≠ Function.update (trunc w) 0 1
⊢ False
Tactic:
exact hne (lec_antisymm hc <| (dom_iff_gec_of_balanced (trunc_zero hw) hb' hE'.symm).mp <|
            (trunc_dom w).trans <| hmin _  <| (dom_of_gec hE' hc).trans $ trunc_dom w)
State after:
no goals