Theorem: Fin.fin_two_eq_zero_of_ne_one (ExponentialRamsey/Prereq/RamseyPrereq.lean)

State before:
x : Fin 2
hx : x ≠ 1
⊢ x = 0
Tactic:
rwa [Fin.eq_zero_iff_ne_one]
State after:
no goals