Theorem: ex_1_2_11_ii (AlgebraI/Subgroups.lean)

State before:
n : ℕ
hn : 3 ≤ n
⊢ ¬Std.Commutative fun x x_1 => x * x_1
Tactic:
rintro ⟨h⟩
State after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
⊢ False

State before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
⊢ False
Tactic:
have := h (r 1) (sr 0)
State after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : r 1 * sr 0 = sr 0 * r 1
⊢ False

State before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : r 1 * sr 0 = sr 0 * r 1
⊢ False
Tactic:
simp only [r_mul_sr, zero_sub, sr_mul_r, zero_add, sr.injEq] at this
State after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : -1 = 1
⊢ False

State before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : -1 = 1
⊢ False
Tactic:
rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two, ← ZMod.val_eq_zero, ZMod.val_ofNat_of_lt hn] at this
State after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : 2 = 0
⊢ False

State before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : 2 = 0
⊢ False
Tactic:
contradiction
State after:
no goals