rintro ⟨h1, h2⟩
case mp
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) → x ≠ 1 ∧ x ^ 2 = 1
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1 ∧ x ^ 2 = 1