awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
⊢ Monoid.exponent (DihedralGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ 0 2

Tactic:
Monoid.exponent_eq_zero_of_order_zero orderOf_r_one

Premises used: Nat.lcm, DihedralGroup.orderOf_r_one, Monoid.exponent_eq_zero_of_order_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
⊢ Monoid.exponent (DihedralGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ 0 2

Tactic:
exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one

Premises used: DihedralGroup.orderOf_r_one, Monoid.exponent_eq_zero_of_order_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
inr : Monoid.exponent (DihedralGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
inr₁ : @lcm _ Nat.instCommMonoidWithZero _ n 2 ∣ Monoid.exponent (DihedralGroup n)
⊢ Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
apply Nat.dvd_antisymm

Premises used: Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
inr : ∀ (g : DihedralGroup n), g ^ @lcm _ Nat.instCommMonoidWithZero _ n 2 = 1
⊢ Monoid.exponent (DihedralGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
apply Monoid.exponent_dvd_of_forall_pow_eq_one

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
inr : n / n.gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
⊢ r m ^ @lcm _ Nat.instCommMonoidWithZero _ n 2 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]

Premises used: DihedralGroup.orderOf_r, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n / n.gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)

Premises used: Nat.dvd_trans, dvd_lcm_left, GCDMonoid.gcd, Exists.intro, OfNat.ofNat, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
inr : n = n / n.gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ n m.val
⊢ n / n.gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
refine Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)

Premises used: Nat.dvd_trans, dvd_lcm_left, GCDMonoid.gcd, Exists.intro, OfNat.ofNat, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n = n / n.gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ n m.val

Tactic:
(Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel, Eq.symm, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n = n / n.gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ n m.val

Tactic:
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel, Eq.symm, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
inr : 2 ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
⊢ sr m ^ @lcm _ Nat.instCommMonoidWithZero _ n 2 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]

Premises used: DihedralGroup.orderOf_sr, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
dvd_lcm_right n 2

Premises used: dvd_lcm_right, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
exact dvd_lcm_right n 2

Premises used: dvd_lcm_right, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
inr : n ∣ Monoid.exponent (DihedralGroup n)
inr₁ : 2 ∣ Monoid.exponent (DihedralGroup n)
⊢ @lcm _ Nat.instCommMonoidWithZero _ n 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
apply lcm_dvd

Premises used: lcm_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
⊢ orderOf (G := DihedralGroup n) (r 1) ∣ Monoid.exponent (DihedralGroup n)

Tactic:
Monoid.order_dvd_exponent (r (1 : ZMod n))

Premises used: Monoid.order_dvd_exponent, DihedralGroup.r, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : n = orderOf (G := DihedralGroup n) (r 1)
⊢ n ∣ Monoid.exponent (DihedralGroup n)

Tactic:
convert! Monoid.order_dvd_exponent (r (1 : ZMod n))

Premises used: Monoid.order_dvd_exponent, DihedralGroup.r, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
⊢ n = orderOf (G := DihedralGroup n) (r 1)

Tactic:
orderOf_r_one.symm

Premises used: DihedralGroup.orderOf_r_one, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
⊢ n = orderOf (G := DihedralGroup n) (r 1)

Tactic:
exact orderOf_r_one.symm

Premises used: DihedralGroup.orderOf_r_one, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
⊢ orderOf (G := DihedralGroup n) (sr 0) ∣ Monoid.exponent (DihedralGroup n)

Tactic:
Monoid.order_dvd_exponent (sr (0 : ZMod n))

Premises used: Monoid.order_dvd_exponent, DihedralGroup.sr, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : 2 = orderOf (G := DihedralGroup n) (sr 0)
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
convert! Monoid.order_dvd_exponent (sr (0 : ZMod n))

Premises used: Monoid.order_dvd_exponent, DihedralGroup.sr, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
⊢ 2 = orderOf (G := DihedralGroup n) (sr 0)

Tactic:
(orderOf_sr 0).symm

Premises used: DihedralGroup.orderOf_sr, OfNat.ofNat, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
⊢ 2 = orderOf (G := DihedralGroup n) (sr 0)

Tactic:
exact (orderOf_sr 0).symm

Premises used: DihedralGroup.orderOf_sr, OfNat.ofNat, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
h : Ne (α := ℕ) 0 1
h_1 : Ne (α := ℕ) 0 2
h' : IsMulCommutative (DihedralGroup 0)
⊢ False

Tactic:
simpa using h'.is_comm.comm (r 1) (sr 0)

Premises used: DihedralGroup.r, DihedralGroup.sr, Std.Commutative.comm, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h : n + 3 ≠ 1
h_1 : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
⊢ HMul.hMul (α := DihedralGroup (n + 3)) (r 1) (sr 0) = HMul.hMul (α := DihedralGroup (n + 3)) (sr 0) (r 1)

Tactic:
have := h'.is_comm.comm (r 1) (sr 0)
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h : n + 3 ≠ 1
h_1 : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
this : HMul.hMul (α := DihedralGroup (n + 3)) (r 1) (sr 0) = HMul.hMul (α := DihedralGroup (n + 3)) (sr 0) (r 1)
⊢ 2 % (n + 3) = 0

Tactic:
rw [r_mul_sr, zero_sub, sr_mul_r, zero_add, sr.injEq, neg_eq_iff_add_eq_zero,
      one_add_one_eq_two, ← ZMod.val_eq_zero, ZMod.val_two_eq_two_mod] at this

Premises used: neg_eq_iff_add_eq_zero, DihedralGroup.sr.injEq, zero_add, one_add_one_eq_two, DihedralGroup.sr_mul_r, ZMod.val_two_eq_two_mod, DihedralGroup.r_mul_sr, ZMod.val_eq_zero, zero_sub
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h : n + 3 ≠ 1
h_1 : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
this : 2 % (n + 3) = 0
⊢ False

Tactic:
simpa using Nat.le_of_dvd Nat.zero_lt_two <| Nat.dvd_of_mod_eq_zero this

Premises used: Nat.dvd_of_mod_eq_zero, Nat.zero_lt_two, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
contrapose! : n ≠ 1 ∧ n ≠ 2 → ¬IsMulCommutative (DihedralGroup n)
⊢ IsMulCommutative (DihedralGroup n) → n = 1 ∨ n = 2

Tactic:
contrapose!
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h1 : n ≠ 1
h2 : n ≠ 2
⊢ ¬IsMulCommutative (DihedralGroup n)

Tactic:
not_commutative h1 h2

Premises used: DihedralGroup.not_commutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h1 : n ≠ 1
h2 : n ≠ 2
⊢ ¬IsMulCommutative (DihedralGroup n)

Tactic:
exact not_commutative h1 h2

Premises used: DihedralGroup.not_commutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
⊢ ∀ (a b : DihedralGroup 1), a * b = b * a

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
⊢ IsMulCommutative (DihedralGroup 1)

Tactic:
exact ⟨⟨by decide⟩⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
⊢ ∀ (a b : DihedralGroup 2), a * b = b * a

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
⊢ IsMulCommutative (DihedralGroup 2)

Tactic:
exact ⟨⟨by decide⟩⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
pos : ∀ (h2 : n = 2), False
neg : ∀ (h2 : ¬n = 2), False
⊢ False

Tactic:
by_cases h2 : n = 2
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False

Tactic:
simpa [exponent, card, h2] using h.exponent_eq_card

Premises used: DihedralGroup.card, DihedralGroup.exponent, IsCyclic.exponent_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False

Tactic:
not_commutative h1 h2 h.isMulCommutative

Premises used: IsCyclic.isMulCommutative, DihedralGroup.not_commutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False

Tactic:
exact not_commutative h1 h2 h.isMulCommutative

Premises used: IsCyclic.isMulCommutative, DihedralGroup.not_commutative
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (r i, sr j).1 (r i, sr j).2
⊢ Eq (α := { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 })
    ((fun (x : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n) ↦
        (match (motive :=
            ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n → { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 })
            x with
          | Sum.inl i => Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, r 0) ⋯
          | Sum.inr (Sum.inl j) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r 0, sr j) ⋯
          | Sum.inr (Sum.inr (Sum.inl k)) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2)
              (sr ((↑u⁻¹ : ZMod n) * k), sr ((↑u⁻¹ : ZMod n) * k)) ⋯
          | Sum.inr (Sum.inr (Sum.inr (i, j))) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r i, r j) ⋯ :
          { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }))
      ((fun (x : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }) ↦
          (match (motive :=
              { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } → ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n)
              x with
            | ⟨(sr i, r a), property⟩ => Sum.inl i
            | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
            | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
            | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))) :
            ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n))
        (Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r i, sr j) h)))
    (Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r i, sr j) h)

Tactic:
simpa [-r_zero, sub_eq_add_neg, neg_eq_iff_add_eq_zero, hu, eq_comm (a := i) (b := 0)]
          using h.eq

Premises used: neg_eq_iff_add_eq_zero, sub_eq_add_neg, eq_comm, Commute.eq, DihedralGroup.r_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, r j).1 (sr i, r j).2
⊢ Eq (α := { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 })
    ((fun (x : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n) ↦
        (match (motive :=
            ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n → { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 })
            x with
          | Sum.inl i => Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, r 0) ⋯
          | Sum.inr (Sum.inl j) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r 0, sr j) ⋯
          | Sum.inr (Sum.inr (Sum.inl k)) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2)
              (sr ((↑u⁻¹ : ZMod n) * k), sr ((↑u⁻¹ : ZMod n) * k)) ⋯
          | Sum.inr (Sum.inr (Sum.inr (i, j))) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r i, r j) ⋯ :
          { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }))
      ((fun (x : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }) ↦
          (match (motive :=
              { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } → ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n)
              x with
            | ⟨(sr i, r a), property⟩ => Sum.inl i
            | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
            | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
            | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))) :
            ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n))
        (Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, r j) h)))
    (Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, r j) h)

Tactic:
simpa [-r_zero, sub_eq_add_neg, eq_neg_iff_add_eq_zero, hu, eq_comm (a := j) (b := 0)]
          using h.eq

Premises used: sub_eq_add_neg, eq_comm, eq_neg_iff_add_eq_zero, Commute.eq, DihedralGroup.r_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, sr j).1 (sr i, sr j).2
⊢ j - i = i - j

Tactic:
replace h := r.inj h
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h_1 : Commute (sr i, sr j).1 (sr i, sr j).2
h : j - i = i - j
⊢ i = j

Tactic:
rw [← neg_sub, neg_eq_iff_add_eq_zero, hu, sub_eq_zero] at h

Premises used: neg_sub, neg_eq_iff_add_eq_zero, sub_eq_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h_1 : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
rw : (↑u⁻¹ : ZMod n) * (2 * j) = j
⊢ Eq (α := { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 })
    ((fun (x : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n) ↦
        (match (motive :=
            ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n → { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 })
            x with
          | Sum.inl i => Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, r 0) ⋯
          | Sum.inr (Sum.inl j) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r 0, sr j) ⋯
          | Sum.inr (Sum.inr (Sum.inl k)) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2)
              (sr ((↑u⁻¹ : ZMod n) * k), sr ((↑u⁻¹ : ZMod n) * k)) ⋯
          | Sum.inr (Sum.inr (Sum.inr (i, j))) =>
            Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (r i, r j) ⋯ :
          { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }))
      ((fun (x : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }) ↦
          (match (motive :=
              { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } → ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n)
              x with
            | ⟨(sr i, r a), property⟩ => Sum.inl i
            | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
            | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
            | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))) :
            ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n))
        (Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, sr j) h_1)))
    (Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, sr j) h_1)

Tactic:
rw [Subtype.ext_iff, Prod.ext_iff, sr.injEq, sr.injEq, h, and_self, ← two_mul]

Premises used: DihedralGroup.sr.injEq, and_self, two_mul, Prod.ext_iff, Subtype.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h_1 : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ (↑u⁻¹ : ZMod n) * (2 * j) = j

Tactic:
u.inv_mul_cancel_left j

Premises used: Units.inv_mul_cancel_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h_1 : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ (↑u⁻¹ : ZMod n) * (2 * j) = j

Tactic:
exact u.inv_mul_cancel_left j

Premises used: Units.inv_mul_cancel_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
⊢ NeZero n

Tactic:
have hn' : NeZero n := ⟨hn.pos.ne'⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
hn' : NeZero n
simp_rw : n + (n + (n + n * n)) = n * (n + 3)
⊢ Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } = n * (n + 3)

Tactic:
simp_rw [Nat.card_congr (oddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]

Premises used: Nat.card_sum, Nat.card_congr, DihedralGroup.oddCommuteEquiv, Nat.card_prod, Nat.card_zmod
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ n + (n + (n + n * n)) = n * (n + 3)

Tactic:
ring
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : Odd n
rw : Nat.card (ConjClasses (DihedralGroup n)) = n * (n + 3) / (n * 2)
rw₁ :
  Nat.card (ConjClasses (DihedralGroup n)) =
    Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } / (n * 2)
rw₂ :
  Nat.card (ConjClasses (DihedralGroup n)) =
    Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } / (2 * n)
rw₃ :
  Nat.card (ConjClasses (DihedralGroup n)) =
    Nat.card (ConjClasses (DihedralGroup n)) * Nat.card (DihedralGroup n) / (2 * n)
rw₄ : Nat.card (ConjClasses (DihedralGroup n)) = Nat.card (ConjClasses (DihedralGroup n)) * (2 * n) / (2 * n)
rw₅ rw₆ : Nat.card (ConjClasses (DihedralGroup n)) = Nat.card (ConjClasses (DihedralGroup n))
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2

Tactic:
rw [← Nat.mul_div_mul_left _ 2 hn.pos, ← card_commute_odd hn, mul_comm,
    card_comm_eq_card_conjClasses_mul_card, nat_card, Nat.mul_div_left _ (mul_pos two_pos hn.pos)]

Premises used: card_comm_eq_card_conjClasses_mul_card, DihedralGroup.card_commute_odd, two_pos, Odd.pos, Nat.mul_div_mul_left, DihedralGroup.nat_card, Nat.mul_div_left, mul_pos, mul_comm, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
simp : ∀ (x : DihedralGroup n), (∀ (g : DihedralGroup n), g * x = x * g) → x = 1
⊢ Eq (α := Subgroup (DihedralGroup n)) (Subgroup.center (DihedralGroup n)) ⊥

Tactic:
simp only [Subgroup.eq_bot_iff_forall, Subgroup.mem_center_iff]

Premises used: Subgroup.mem_center_iff, Subgroup.eq_bot_iff_forall
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * r i = r i * g
⊢ i + i = i - i

Tactic:
have heq := sr.inj (h (sr i))
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * r i = r i * g
heq : i + i = i - i
⊢ r i = 1

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
⊢ i - 1 = i + 1

Tactic:
have heq := sr.inj (h (r 1))
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
⊢ 1 < n

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
⊢ Fact (1 < n)

Tactic:
have : Fact (1 < n) := ⟨by grind⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
this : Fact (1 < n)
⊢ sr i = 1

Tactic:
simp [sub_eq_iff_eq_add, add_assoc, ZMod.add_self_eq_zero_iff_eq_zero hodd] at heq

Premises used: ZMod.add_self_eq_zero_iff_eq_zero, add_assoc, sub_eq_iff_eq_add
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
⊢ Nat.card (ZMod 2 × ZMod 2) = 4

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
⊢ AddMonoid.exponent (ZMod 2 × ZMod 2) = 2

Tactic:
simp [AddMonoid.exponent_prod]

Premises used: AddMonoid.exponent_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
rw : Nat.card.{u_1} (Additive G) = Nat.card G
⊢ Nat.card.{u_1} (Additive G) = 4

Tactic:
rw [← IsKleinFour.card_four (G := G)]

Premises used: IsKleinFour.card_four
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
⊢ Nat.card.{u_1} (Additive G) = Nat.card G

Tactic:
congr!
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
⊢ AddMonoid.exponent.{u_1} (Additive G) = 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : IsAddKleinFour G
rw : Nat.card.{u_1} (Multiplicative G) = Nat.card G
⊢ Nat.card.{u_1} (Multiplicative G) = 4

Tactic:
rw [← IsAddKleinFour.card_four (G := G)]

Premises used: IsAddKleinFour.card_four
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : IsAddKleinFour G
⊢ Nat.card.{u_1} (Multiplicative G) = Nat.card G

Tactic:
congr!
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : IsAddKleinFour G
⊢ Monoid.exponent.{u_1} (Multiplicative G) = 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
⊢ Nat.card G ≠ 0

Tactic:
simp [IsKleinFour.card_four]

Premises used: IsKleinFour.card_four
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
inst_2 : IsKleinFour G
⊢ Fintype.card G = 4

Tactic:
Nat.card_eq_fintype_card (α := G).symm ▸ IsKleinFour.card_four

Premises used: Eq.rec, Eq.symm, IsKleinFour.card_four, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
h : IsCyclic G
⊢ False

Tactic:
simpa using h.exponent_eq_card

Premises used: IsCyclic.exponent_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
x : G
⊢ Monoid.exponent G = 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
x : G
rw : x = x⁻¹
rw₁ rw₂ : x = x
⊢ x * x = 1

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_eq_self]

Premises used: mul_eq_one_iff_eq_inv, IsKleinFour.inv_eq_self
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
inst_2 : Fintype G
inst_3 : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hs : card (α := G) {x * y, x, y, 1} = Fintype.card G
⊢ Eq (α := Finset G) {x * y, x, y, 1} univ

Tactic:
apply Finset.eq_univ_of_card

Premises used: Finset.eq_univ_of_card