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

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
⊢ w = w'
Tactic:
have h₁ := hmin _ h
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
⊢ w = w'
Tactic:
have hmin' := fun u (hu : u ≤d w') ↦ h.trans (hmin u (hu.trans h))
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
⊢ w = w'
Tactic:
have hb := balanced_of_min hw hmin
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
⊢ w = w'
Tactic:
have hb' := balanced_of_min hw' hmin'
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'
Tactic:
have hE := E_dom_eq hw hw' h₁ h
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'
Tactic:
exact lec_antisymm
  ((dom_iff_gec_of_balanced hw' hb hE.symm).mp h) ((dom_iff_gec_of_balanced hw hb' hE).mp h₁)
State after:
no goals