awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hy : ¬y = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
have neg : (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]
-- 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
hy : ¬y = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
have neg : (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: try simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]
-- 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
hy : ¬y = 1
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have pos : ∀ (hxy : x = y),
  (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: by_cases hxy : x = y
-- 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
hy : ¬y = 1
pos :
  ∀ (hxy : x = y),
    (e : (a : G₁) → G₂) (x * y) =
      HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have neg : ∀ (hxy : ¬x = y),
  (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: by_cases hxy : x = y
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (hypothesis)
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
hy : ¬y = 1
hxy : ¬x = y
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have univ₂ : Eq (α := Finset G₂)
  (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
  univ
Tactic: have univ₂ : {e (x * y), e x, e y, (1 : G₂)} = Finset.univ := by
        simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (hypothesis)
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
hy : ¬y = 1
hxy : ¬x = y
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have hx₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
Tactic: rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
Cleared hypotheses: hx, hy, hxy, univ₂
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (hypothesis)
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
hy : ¬y = 1
hxy : ¬x = y
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
hx₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have hy₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
Tactic: rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
Cleared hypotheses: hx, hy, hxy, univ₂
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (hypothesis)
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
hy : ¬y = 1
hxy : ¬x = y
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
hx₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
hy₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have hxy₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
Cleared hypotheses: hx, hy, hxy, univ₂
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (hypothesis)
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 : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have hx₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂)
Tactic: rw [he] at hx hy
Cleared hypotheses: hx, hy, hxy, univ₂
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (hypothesis)
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 : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) ((e : (a : G₁) → G₂) 1 : G₂)
hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
hx₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂)
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have hy₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂)
Tactic: rw [he] at hx hy
Cleared hypotheses: hx, hy, hxy, univ₂
-- 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 : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂)
hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂)
hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have neg : HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂) = (e : (a : G₁) → G₂) (x * y)
Tactic: symm
-- 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 : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂)
hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂)
hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
⊢ HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂) = (e : (a : G₁) → G₂) (x * y)
have neg : HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂) ∉
  insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})
Tactic: apply eq_of_mem_insert_of_notMem <| univ₂.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
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
hy : ¬y = 1
hxy : ¬x = y
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have have : Eq (α := Finset G₂)
  (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
  univ
Tactic: classical
      have univ₂ : {e (x * y), e x, e y, (1 : G₂)} = Finset.univ := by
        simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))
      rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
      rw [he] at hx hy
      symm
      apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _
      simpa using mul_notMem_of_exponent_two h hx hy hxy
-- 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
hy : ¬y = 1
hxy : ¬x = y
have :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have neg : ∀
  (univ₂ :
    Eq (α := Finset G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
      univ),
  (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: classical
      have univ₂ : {e (x * y), e x, e y, (1 : G₂)} = Finset.univ := by
        simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))
      rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
      rw [he] at hx hy
      symm
      apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _
      simpa using mul_notMem_of_exponent_two h hx hy hxy
-- 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
hy : ¬y = 1
hxy : ¬x = y
have :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
neg :
  ∀
    (univ₂ :
      Eq (α := Finset G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
          (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
        univ),
    (e : (a : G₁) → G₂) (x * y) =
      HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have₁ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
neg₁ neg₂ :
  ∀
    (univ₂ :
      Eq (α := Finset G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
          (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
        univ),
    (e : (a : G₁) → G₂) (x * y) =
      HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have neg₃ : ∀ (hx : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) 1 : G₂))
  (hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) ((e : (a : G₁) → G₂) 1 : G₂))
  (hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂))
  (univ₂ :
    Eq (α := Finset G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
      univ),
  (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: classical
      have univ₂ : {e (x * y), e x, e y, (1 : G₂)} = Finset.univ := by
        simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))
      rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
      rw [he] at hx hy
      symm
      apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _
      simpa using mul_notMem_of_exponent_two h hx hy hxy
Cleared hypotheses: hx, hy, hxy
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - ((↑n : ZMod (2 * n)) + j - i)) = xa (i + ((↑n : ZMod (2 * n)) + k - j))
have xa : xa (k - (↑n : ZMod (2 * n)) - j + i) = xa (k + (↑n : ZMod (2 * n)) - j + i)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ HMul.hMul (α := ZMod (2 * n)) 2 (↑n : ZMod (2 * n)) = 0
have norm_cast : Eq (α := ZMod (2 * n)) (↑(2 * n) : ZMod (2 * n)) 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (↑n : ZMod (2 * n)) - j + i) = xa (k + (↑n : ZMod (2 * n)) - j + i)
have this : HMul.hMul (α := ZMod (2 * n)) 2 (↑n : ZMod (2 * n)) = 0
Tactic: have : (2 * n : ZMod (2 * n)) = 0 := by norm_cast; simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Fintype.card (QuaternionGroup n) = 4 * n
have rw : n + n + (n + n) = 4 * n
Tactic: rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a (↑0 : ZMod (2 * n))
have zero : HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a 0
Tactic: rw [Nat.cast_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n k : ℕ
IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
⊢ HPow.hPow (α := QuaternionGroup n) (a 1) (k + 1) = a (↑(k + 1) : ZMod (2 * n))
have succ : a (HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1) = a (↑(k + 1) : ZMod (2 * n))
Tactic: rw [pow_succ, IH, a_mul_a]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n k : ℕ
IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
⊢ a (HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1) = a (↑(k + 1) : ZMod (2 * n))
have succ : HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1 = (↑(k + 1) : ZMod (2 * n))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n k : ℕ
IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
⊢ HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1 = (↑(k + 1) : ZMod (2 * n))
have succ : Eq (α := ZMod (2 * n)) (↑(k + 1) : ZMod (2 * n)) (↑(k + 1) : ZMod (2 * n))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n k : ℕ
⊢ HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
have zero : HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a (↑0 : ZMod (2 * n))
Tactic: induction k with
  | zero => rw [Nat.cast_zero]; rfl
  | succ k IH =>
    rw [pow_succ, IH, a_mul_a]
    congr 1
    norm_cast
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n k : ℕ
zero : HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a (↑0 : ZMod (2 * n))
⊢ HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
have succ : ∀ (k : ℕ) (IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))),
  HPow.hPow (α := QuaternionGroup n) (a 1) (k + 1) = a (↑(k + 1) : ZMod (2 * n))
Tactic: induction k with
  | zero => rw [Nat.cast_zero]; rfl
  | succ k IH =>
    rw [pow_succ, IH, a_mul_a]
    congr 1
    norm_cast
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ HPow.hPow (β := ℕ) (xa i) 4 = 1
have calc : HPow.hPow (β := ℕ) (xa i) 4 = a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n)))
Tactic: calc xa i ^ 4
      = a (n + n) := by simp [pow_succ, add_sub_assoc, sub_sub_cancel]
    _ = a ↑(2 * n) := by simp [Nat.cast_add, two_mul]
    _ = 1 := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
i : ZMod (2 * n)
calc : HPow.hPow (β := ℕ) (xa i) 4 = a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n)))
⊢ HPow.hPow (β := ℕ) (xa i) 4 = 1
have calc₁ : a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n))) = a (↑(2 * n) : ZMod (2 * n))
Tactic: calc xa i ^ 4
      = a (n + n) := by simp [pow_succ, add_sub_assoc, sub_sub_cancel]
    _ = a ↑(2 * n) := by simp [Nat.cast_add, two_mul]
    _ = 1 := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
i : ZMod (2 * n)
calc : HPow.hPow (β := ℕ) (xa i) 4 = a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n)))
calc₁ : a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n))) = a (↑(2 * n) : ZMod (2 * n))
⊢ HPow.hPow (β := ℕ) (xa i) 4 = 1
have calc₂ : Eq (α := QuaternionGroup n) (a (↑(2 * n) : ZMod (2 * n))) 1
Tactic: calc xa i ^ 4
      = a (n + n) := by simp [pow_succ, add_sub_assoc, sub_sub_cancel]
    _ = a ↑(2 * n) := by simp [Nat.cast_add, two_mul]
    _ = 1 := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = HPow.hPow (α := ℕ) (β := ℕ) 2 2
have this : Fact (Nat.Prime 2)
Tactic: haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ orderOf (xa i) = HPow.hPow (α := ℕ) (β := ℕ) 2 2
have hnot : ¬xa i ^ HPow.hPow (α := ℕ) (β := ℕ) 2 1 = 1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
hnot : ¬xa i ^ HPow.hPow (α := ℕ) (β := ℕ) 2 1 = 1
⊢ orderOf (xa i) = HPow.hPow (α := ℕ) (β := ℕ) 2 2
have hfin : xa i ^ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 1 1) = 1
Tactic: apply orderOf_eq_prime_pow
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : xa i ^ HPow.hPow (α := ℕ) (β := ℕ) 2 1 = 1
⊢ False
have h₁ : Eq (α := QuaternionGroup n) (a (↑n : ZMod (2 * n))) 1
Tactic: simp only [pow_one, xa_sq] at h
Cleared hypotheses: h