awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ @lcm _ Nat.instCommMonoidWithZero _ n 2 = 1
have inr : 2 ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ @lcm _ Nat.instCommMonoidWithZero _ n 2 ∣ Monoid.exponent (DihedralGroup n)
have inr : n ∣ Monoid.exponent (DihedralGroup n)
Tactic: apply lcm_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
inr : n ∣ Monoid.exponent (DihedralGroup n)
⊢ @lcm _ Nat.instCommMonoidWithZero _ n 2 ∣ Monoid.exponent (DihedralGroup n)
have inr₁ : 2 ∣ Monoid.exponent (DihedralGroup n)
Tactic: apply lcm_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ n ∣ Monoid.exponent (DihedralGroup n)
have h : n = orderOf (G := DihedralGroup n) (r 1)
Tactic: convert! Monoid.order_dvd_exponent (r (1 : ZMod n))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)
have h : 2 = orderOf (G := DihedralGroup n) (sr 0)
Tactic: convert! Monoid.order_dvd_exponent (sr (0 : ZMod n))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
Goal:
n : ℕ
h : n + 3 ≠ 1
h_1 : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
⊢ False
have this : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
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)
⊢ False
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
⊢ IsMulCommutative (DihedralGroup n) → n = 1 ∨ n = 2
have contrapose! : n ≠ 1 ∧ n ≠ 2 → ¬IsMulCommutative (DihedralGroup n)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
⊢ False
have pos : ∀ (h2 : n = 2), False
Tactic: by_cases h2 : n = 2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
pos : ∀ (h2 : n = 2), False
⊢ False
have neg : ∀ (h2 : ¬n = 2), False
Tactic: by_cases h2 : n = 2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
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
⊢ 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)))
    (Subtype.mk (p := fun (p : DihedralGroup n × DihedralGroup n) ↦ Commute p.1 p.2) (sr i, sr j) h)
have h₁ : j - i = i - j
Tactic: replace h := r.inj h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
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
⊢ 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)
have h₁ : i = j
Tactic: rw [← neg_sub, neg_eq_iff_add_eq_zero, hu, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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
⊢ 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)
have rw : (↑u⁻¹ : ZMod n) * (2 * j) = j
Tactic: rw [Subtype.ext_iff, Prod.ext_iff, sr.injEq, sr.injEq, h, and_self, ← two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
Goal:
n : ℕ
hn : Odd n
⊢ Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } = n * (n + 3)
have hn' : NeZero n
Tactic: have hn' : NeZero n := ⟨hn.pos.ne'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } = n * (n + 3)
have simp_rw : n + (n + (n + n * n)) = n * (n + 3)
Tactic: simp_rw [Nat.card_congr (oddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
have rw : Nat.card (ConjClasses (DihedralGroup n)) = n * (n + 3) / (n * 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)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : Odd n
rw : Nat.card (ConjClasses (DihedralGroup n)) = n * (n + 3) / (n * 2)
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
have rw₁ : Nat.card (ConjClasses (DihedralGroup n)) =
  Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } / (n * 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)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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)
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
have rw₂ : Nat.card (ConjClasses (DihedralGroup n)) =
  Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } / (2 * n)
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)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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)
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
have rw₃ : Nat.card (ConjClasses (DihedralGroup n)) =
  Nat.card (ConjClasses (DihedralGroup n)) * Nat.card (DihedralGroup n) / (2 * n)
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)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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)
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
have rw₄ : Nat.card (ConjClasses (DihedralGroup n)) = Nat.card (ConjClasses (DihedralGroup n)) * (2 * n) / (2 * n)
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)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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)
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
have rw₅ : Nat.card (ConjClasses (DihedralGroup n)) = Nat.card (ConjClasses (DihedralGroup n))
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)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
⊢ Eq (α := Subgroup (DihedralGroup n)) (Subgroup.center (DihedralGroup n)) ⊥
have simp : ∀ (x : DihedralGroup n), (∀ (g : DihedralGroup n), g * x = x * g) → x = 1
Tactic: simp only [Subgroup.eq_bot_iff_forall, Subgroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * r i = r i * g
⊢ r i = 1
have heq : i + i = i - i
Tactic: have heq := sr.inj (h (sr i))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
Goal:
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
⊢ sr i = 1
have heq : i - 1 = i + 1
Tactic: have heq := sr.inj (h (r 1))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
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
⊢ sr i = 1
have this : Fact (1 < n)
Tactic: have : Fact (1 < n) := ⟨by grind⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
⊢ Nat.card.{u_1} (Additive G) = 4
have rw : Nat.card.{u_1} (Additive G) = Nat.card G
Tactic: rw [← IsKleinFour.card_four (G := G)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : IsAddKleinFour G
⊢ Nat.card.{u_1} (Multiplicative G) = 4
have rw : Nat.card.{u_1} (Multiplicative G) = Nat.card G
Tactic: rw [← IsAddKleinFour.card_four (G := G)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
x : G
⊢ x * x = 1
have rw : x = x⁻¹
Tactic: rw [mul_eq_one_iff_eq_inv, inv_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
x : G
rw : x = x⁻¹
⊢ x * x = 1
have rw₁ : x = x
Tactic: rw [mul_eq_one_iff_eq_inv, inv_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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
⊢ Eq (α := Finset G) {x * y, x, y, 1} univ
have hs : card (α := G) {x * y, x, y, 1} = Fintype.card G
Tactic: apply Finset.eq_univ_of_card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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
⊢ card (α := G) {x * y, x, y, 1} = Fintype.card G
have hs : card (α := G) {x * y, x, y, 1} = 4
Tactic: rw [card_four']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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
⊢ card (α := G) {x * y, x, y, 1} = 4
have hs : card (α := G) {x, y, 1} + 1 = 4
Tactic: rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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, 1} + 1 = 4
⊢ card (α := G) {x * y, x, y, 1} = 4
have hs₁ : x * y ∉ {x, y, 1}
Tactic: rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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
⊢ card (α := G) {x, y, 1} + 1 = 4
have hs : card (α := G) {y, 1} + 1 + 1 = 4
Tactic: rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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) {y, 1} + 1 + 1 = 4
⊢ card (α := G) {x, y, 1} + 1 = 4
have hs₁ : x ∉ {y, 1}
Tactic: rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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
⊢ card (α := G) {y, 1} + 1 + 1 = 4
have hs : card (α := G) {1} + 1 + 1 + 1 = 4
Tactic: rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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) {1} + 1 + 1 + 1 = 4
⊢ card (α := G) {y, 1} + 1 + 1 = 4
have hs₁ : y ∉ {1}
Tactic: rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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
⊢ card (α := G) {x * y, x, y, 1} = 4
have hs : card (α := G) {1} + 1 + 1 + 1 = 4
Tactic: repeat rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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) {1} + 1 + 1 + 1 = 4
⊢ card (α := G) {x * y, x, y, 1} = 4
have hs₁ : y ∉ {1}
Tactic: repeat rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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) {1} + 1 + 1 + 1 = 4
hs₁ : y ∉ {1}
⊢ card (α := G) {x * y, x, y, 1} = 4
have hs₂ : x ∉ {y, 1}
Tactic: repeat rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
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) {1} + 1 + 1 + 1 = 4
hs₁ : y ∉ {1}
hs₂ : x ∉ {y, 1}
⊢ card (α := G) {x * y, x, y, 1} = 4
have hs₃ : x * y ∉ {x, y, 1}
Tactic: repeat rw [card_insert_of_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
x_1 : Fintype G := Fintype.ofFinite G
⊢ z = x * y
have apply : z ∉ {x, y, 1}
Tactic: apply eq_of_mem_insert_of_notMem <| (eq_finset_univ hx hy hxy).symm ▸ mem_univ _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
let let₁ let₂ : z = x * y
⊢ z = x * y
have let₃ : z ∉ {x, y, 1}
Tactic: classical
  let _ := Fintype.ofFinite G
  apply eq_of_mem_insert_of_notMem <| (eq_finset_univ hx hy hxy).symm ▸ mem_univ _
  simpa only [mem_singleton, mem_insert, not_or] using ⟨hzx, hzy, hz⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
have pos : ∀ (hx : x = 1), e.toFun (x * y) = e.toFun x * e.toFun y
Tactic: by_cases hx : x = 1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
pos : ∀ (hx : x = 1), e.toFun (x * y) = e.toFun x * e.toFun y
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
have neg : ∀ (hx : ¬x = 1), e.toFun (x * y) = e.toFun x * e.toFun y
Tactic: by_cases hx : x = 1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : x = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
have pos : ∀ (hy : y = 1), e.toFun (x * y) = e.toFun x * e.toFun y
Tactic: by_cases hy : y = 1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : x = 1
pos : ∀ (hy : y = 1), e.toFun (x * y) = e.toFun x * e.toFun y
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
have neg : ∀ (hy : ¬y = 1), e.toFun (x * y) = e.toFun x * e.toFun y
Tactic: by_cases hy : y = 1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
have pos : ∀ (hy : y = 1), e.toFun (x * y) = e.toFun x * e.toFun y
Tactic: by_cases hy : y = 1