exact lec_antisymm
  ((dom_iff_gec_of_balanced hw' hb hE.symm).mp h) ((dom_iff_gec_of_balanced hw hb' hE).mp h₁)
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'
no goals