Theorem: Weight.lec_antisymm (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h₁ : w ≤ w'
h₂ : w' ≤ w
⊢ w = w'
Tactic:
ext j
State after:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h₁ : w ≤ w'
h₂ : w' ≤ w
j : Fin (Nat.succ n)
⊢ w j = w' j

State before:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h₁ : w ≤ w'
h₂ : w' ≤ w
j : Fin (Nat.succ n)
⊢ w j = w' j
Tactic:
exact le_antisymm ((lec_iff w w').mp h₁ j) ((lec_iff w' w).mp h₂ j)
State after:
no goals