awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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} = 4
⊢ card (α := G) {x * y, x, y, 1} = Fintype.card G

Tactic:
rw [card_four']

Premises used: IsKleinFour.card_four'
-- 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, 1} + 1 = 4
hs₁ : x * y ∉ {x, y, 1}
⊢ card (α := G) {x * y, x, y, 1} = 4

Tactic:
rw [card_insert_of_notMem]

Premises used: Finset.card_insert_of_notMem
-- 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) {y, 1} + 1 + 1 = 4
hs₁ : x ∉ {y, 1}
⊢ card (α := G) {x, y, 1} + 1 = 4

Tactic:
rw [card_insert_of_notMem]

Premises used: Finset.card_insert_of_notMem
-- 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) {1} + 1 + 1 + 1 = 4
hs₁ : y ∉ {1}
⊢ card (α := G) {y, 1} + 1 + 1 = 4

Tactic:
rw [card_insert_of_notMem]

Premises used: Finset.card_insert_of_notMem
-- 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) {1} + 1 + 1 + 1 = 4
hs₁ : y ∉ {1}
hs₂ : x ∉ {y, 1}
hs₃ : x * y ∉ {x, y, 1}
⊢ card (α := G) {x * y, x, y, 1} = 4

Tactic:
repeat rw [card_insert_of_notMem]

Premises used: Finset.card_insert_of_notMem
-- 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
⊢ Monoid.exponent G = 2

Tactic:
simp
-- 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
⊢ x * y ∉ {x, y, 1}

Tactic:
simpa using mul_notMem_of_exponent_two (by simp) hx hy hxy

Premises used: mul_notMem_of_exponent_two
-- 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
⊢ x * y ∉ {x, y, 1}

Tactic:
on_goal 4 => simpa using mul_notMem_of_exponent_two (by simp) hx hy hxy

Premises used: mul_notMem_of_exponent_two
-- 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
⊢ card (α := G) {1} + 1 + 1 + 1 = 4

Tactic:
simp_all
-- 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
⊢ y ∉ {1}

Tactic:
simp_all
-- 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
⊢ x ∉ {y, 1}

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
apply : z ∉ {x, y, 1}
⊢ z = x * y

Tactic:
apply eq_of_mem_insert_of_notMem <| (eq_finset_univ hx hy hxy).symm ▸ mem_univ _

Premises used: Finset.eq_of_mem_insert_of_notMem
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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, 1}

Tactic:
simpa only [mem_singleton, mem_insert, not_or] using ⟨hzx, hzy, hz⟩

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
let₃ : z ∉ {x, y, 1}
⊢ z = x * y

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⟩

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or, Finset.eq_of_mem_insert_of_notMem
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
neg : ∀ (hx : ¬x = 1), e.toFun (x * y) = e.toFun x * e.toFun y
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
by_cases hx : x = 1
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
neg : ∀ (hy : ¬y = 1), e.toFun (x * y) = e.toFun x * e.toFun y
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
by_cases hy : y = 1
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
neg : ∀ (hy : ¬y = 1), e.toFun (x * y) = e.toFun x * e.toFun y
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
by_cases hy : y = 1
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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

Tactic:
try simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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

Tactic:
try simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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

Tactic:
try simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
neg :
  (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
neg :
  (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
try simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Premises used: Equiv.toFun_as_coe, mul_one, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)
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₂)
⊢ (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
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)

Tactic:
simp [hxy, mul_self, ← pow_two (e y), h ▸ Monoid.pow_exponent_eq_one (e y), he]

Premises used: pow_two, IsKleinFour.mul_self, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
⊢ 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:
simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))

Premises used: Finset.map_univ_equiv, Finset.map_insert
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
⊢ 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))
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
⊢ 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

Premises used: Function.Injective.ne_iff, Ne, Equiv.injective
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)
⊢ 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

Premises used: Function.Injective.ne_iff, Ne, Equiv.injective
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)
⊢ 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

Premises used: Function.Injective.ne_iff, Ne, Equiv.injective
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)
hxy₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
⊢ 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:
rw [← Ne, ← e.injective.ne_iff] at hx hy hxy

Premises used: Function.Injective.ne_iff, Ne, Equiv.injective
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
⊢ Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂)

Tactic:
rw [he] at hx hy
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)
⊢ Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂)

Tactic:
rw [he] at hx hy
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)
hy₁ : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂)
⊢ Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)

Tactic:
rw [he] at hx hy
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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₂)
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₂)
⊢ 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:
rw [he] at hx hy
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
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
neg :
  HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂) = (e : (a : G₁) → G₂) (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:
symm