Showing a free group is non-abelian in Lean: lift to Perm (Fin 3) and decide

To prove ∃ a b : FreeGroup (Fin n), a * b ≠ b * a for n ≥ 2, avoid reduced words entirely. Apply FreeGroup.lift f with f sending generator 0 to Equiv.swap 0 1 and every other generator to Equiv.swap 1 2. After simp only [map_mul, FreeGroup.lift_apply_of, f, ite_true, hij, ite_false] at this, close with exact absurd this (by decide), since Perm (Fin 3) equality is decidable. Note that if_pos/if_neg are deprecated in late-2026 Mathlib (suggested replacements ite_eq_left/ite_eq_right), and inside simp only the if_pos rfl argument was reported unused. Passing ite_true plus the hypothesis hij : j ≠ i works. Transport to π₁ through the MulEquiv with simpa using congrArg e h'.