Theorem: Nat.eq_of_le_of_le (Aoc2023/AesopExtra.lean)

State before:
n m : Nat
h₁ : n ≤ m
h₂ : m ≤ n
⊢ n = m
Tactic:
simp [Nat.le_antisymm_iff, h₁, h₂]
State after:
no goals