awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Exponent
Goal:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : Monoid M₁
inst_1 : Monoid M₂
inst_2 : FunLike F M₁ M₂
inst_3 : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
refine : ∀ (m₂ : M₂), m₂ ^ exponent M₁ = 1
⊢ exponent M₂ ∣ exponent M₁

Tactic:
refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : Monoid M₁
inst_1 : Monoid M₂
inst_2 : FunLike F M₁ M₂
inst_3 : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
m₂ : M₂
obtain : ∀ (m₁ : M₁), HPow.hPow (α := M₂) ((f : (a : M₁) → M₂) m₁ : M₂) (exponent M₁) = 1
⊢ m₂ ^ exponent M₁ = 1

Tactic:
obtain ⟨m₁, rfl⟩ := hf m₂

Premises used: rfl
-- Module: Mathlib.GroupTheory.Exponent
Goal:
F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : Monoid M₁
inst_1 : Monoid M₂
inst_2 : FunLike F M₁ M₂
inst_3 : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
m₁ : M₁
rw : Eq.{u_3 + 1} (α := M₂) ((f : (a : M₁) → M₂) (m₁ ^ exponent M₁) : M₂) (1 : M₂)
rw₁ : Eq.{u_3 + 1} (α := M₂) ((f : (a : M₁) → M₂) 1 : M₂) (1 : M₂)
rw₂ rw₃ : Eq.{u_3 + 1} (α := M₂) 1 1
⊢ HPow.hPow (α := M₂) ((f : (a : M₁) → M₂) m₁ : M₂) (exponent M₁) = 1

Tactic:
rw [← map_pow, pow_exponent_eq_one, map_one]

Premises used: map_pow, map_one, Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) = Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)

Tactic:
dvd_antisymm ?_ ?_

Premises used: dvd_antisymm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
refine_1 : exponent ((i : ι) → M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
refine_2 : (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) ∣ exponent ((i : ι) → M i)
⊢ exponent ((i : ι) → M i) = Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)

Tactic:
refine dvd_antisymm ?_ ?_

Premises used: dvd_antisymm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)

Tactic:
exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
refine_1 : ∀ (m : (i : ι) → M i), HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) = 1
⊢ exponent ((i : ι) → M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)

Tactic:
refine exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
refine_1 : ∀ (i : ι), HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) i = 1 i
⊢ HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) = 1

Tactic:
ext i
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
refine_1 : orderOf (m i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
⊢ HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) i = 1 i

Tactic:
rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]

Premises used: Pi.one_apply, Pi.pow_apply, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
refine_1 : exponent.{u_2} (M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
⊢ orderOf (m i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)

Tactic:
apply dvd_trans (Monoid.order_dvd_exponent (m i))

Premises used: Monoid.order_dvd_exponent, dvd_trans
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ exponent.{u_2} (M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)

Tactic:
Finset.dvd_lcm (mem_univ i)

Premises used: Finset.mem_univ, Finset.dvd_lcm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ exponent.{u_2} (M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)

Tactic:
exact Finset.dvd_lcm (mem_univ i)

Premises used: Finset.mem_univ, Finset.dvd_lcm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
apply : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → exponent.{u_2} (M i) ∣ exponent ((i : ι) → M i)
⊢ (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) ∣ exponent ((i : ι) → M i)

Tactic:
apply Finset.lcm_dvd fun i _ ↦ ?_

Premises used: Finset.lcm_dvd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ exponent.{u_2} (M i) ∣ exponent ((i : ι) → M i)

Tactic:
MonoidHom.exponent_dvd (f := Pi.evalMonoidHom (M ·) i) (Function.surjective_eval i)

Premises used: Function.surjective_eval, MonoidHom.exponent_dvd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ exponent.{u_2} (M i) ∣ exponent ((i : ι) → M i)

Tactic:
exact MonoidHom.exponent_dvd (f := Pi.evalMonoidHom (M ·) i) (Function.surjective_eval i)

Premises used: Function.surjective_eval, MonoidHom.exponent_dvd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
⊢ exponent (M₁ × M₂) = @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
dvd_antisymm ?_ (lcm_dvd ?_ ?_)

Premises used: lcm_dvd, dvd_antisymm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
refine_1 : exponent (M₁ × M₂) ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
refine_2 : exponent M₁ ∣ exponent (M₁ × M₂)
refine_3 : exponent M₂ ∣ exponent (M₁ × M₂)
⊢ exponent (M₁ × M₂) = @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)

Premises used: lcm_dvd, dvd_antisymm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
⊢ exponent (M₁ × M₂) ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
exponent_dvd_of_forall_pow_eq_one fun g ↦ ?_

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
refine_1 : ∀ (g : M₁ × M₂), g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂) = 1
⊢ exponent (M₁ × M₂) ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
refine exponent_dvd_of_forall_pow_eq_one fun g ↦ ?_

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
refine_1 : (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).1 = 1.1
refine_1₁ : (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).2 = 1.2
⊢ g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂) = 1

Tactic:
ext1
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
refine_1 : orderOf g.1 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
⊢ (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).1 = 1.1

Tactic:
rw [Prod.pow_fst, Prod.fst_one, ← orderOf_dvd_iff_pow_eq_one]

Premises used: Prod.fst_one, orderOf_dvd_iff_pow_eq_one, Prod.pow_fst
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
dvd_trans (Monoid.order_dvd_exponent (g.1)) <| dvd_lcm_left _ _

Premises used: Monoid.order_dvd_exponent, dvd_trans, Prod.fst, dvd_lcm_left
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
exact dvd_trans (Monoid.order_dvd_exponent (g.1)) <| dvd_lcm_left _ _

Premises used: Monoid.order_dvd_exponent, dvd_trans, Prod.fst, dvd_lcm_left
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
refine_1 : orderOf g.2 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
⊢ (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).2 = 1.2

Tactic:
rw [Prod.pow_snd, Prod.snd_one, ← orderOf_dvd_iff_pow_eq_one]

Premises used: Prod.pow_snd, Prod.snd_one, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.2 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
dvd_trans (Monoid.order_dvd_exponent (g.2)) <| dvd_lcm_right _ _

Premises used: dvd_lcm_right, Monoid.order_dvd_exponent, dvd_trans, Prod.snd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.2 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)

Tactic:
exact dvd_trans (Monoid.order_dvd_exponent (g.2)) <| dvd_lcm_right _ _

Premises used: dvd_lcm_right, Monoid.order_dvd_exponent, dvd_trans, Prod.snd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
⊢ exponent M₁ ∣ exponent (M₁ × M₂)

Tactic:
MonoidHom.exponent_dvd (f := MonoidHom.fst M₁ M₂) Prod.fst_surjective

Premises used: Prod.fst_surjective, MonoidHom.exponent_dvd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
⊢ exponent M₁ ∣ exponent (M₁ × M₂)

Tactic:
exact MonoidHom.exponent_dvd (f := MonoidHom.fst M₁ M₂) Prod.fst_surjective

Premises used: Prod.fst_surjective, MonoidHom.exponent_dvd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)

Tactic:
MonoidHom.exponent_dvd (f := MonoidHom.snd M₁ M₂) Prod.snd_surjective

Premises used: MonoidHom.exponent_dvd, Prod.snd_surjective
-- Module: Mathlib.GroupTheory.Exponent
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)

Tactic:
exact MonoidHom.exponent_dvd (f := MonoidHom.snd M₁ M₂) Prod.snd_surjective

Premises used: MonoidHom.exponent_dvd, Prod.snd_surjective
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
hG : Monoid.exponent G = 2
hx : orderOf.{u} (G := G) 1 = 2
⊢ False

Tactic:
norm_num at hx
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
h : ∀ (g : G), orderOf g ∣ 2
a b : G
⊢ ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1

Tactic:
simp_rw [orderOf_dvd_iff_pow_eq_one] at h

Premises used: orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
rw : a * (a * b) * b = a * (b * a) * b
⊢ Commute a b

Tactic:
rw [commute_iff_eq, ← mul_right_inj a, ← mul_left_inj b]

Premises used: mul_left_inj, commute_iff_eq, mul_right_inj
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
⊢ a * (a * b) * b = HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2

Tactic:
simp [pow_two, mul_assoc]

Premises used: pow_two, mul_assoc
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
rw : 1 * HPow.hPow (β := ℕ) b 2 = 1
rw₁ : HMul.hMul (α := G) 1 1 = 1
rw₂ rw₃ : Eq.{u + 1} (α := G) 1 1
⊢ HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2 = 1

Tactic:
rw [h, h, mul_one]

Premises used: mul_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
rw rw₁ : Eq.{u + 1} (α := G) 1 1
⊢ 1 = HPow.hPow (β := ℕ) (a * b) 2

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
⊢ HPow.hPow (β := ℕ) (a * b) 2 = a * (b * a) * b

Tactic:
simp [pow_two, mul_assoc]

Premises used: pow_two, mul_assoc
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
a₁ : a * (a * b) * b = HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2
a₂ : HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2 = 1
a₃ : 1 = HPow.hPow (β := ℕ) (a * b) 2
a₄ : HPow.hPow (β := ℕ) (a * b) 2 = a * (b * a) * b
⊢ a * (a * b) * b = a * (b * a) * b

Tactic:
calc
    a * (a * b) * b = a ^ 2 * b ^ 2 := by simp [pow_two, mul_assoc]
    _ = 1 := by rw [h, h, mul_one]
    _ = (a * b) ^ 2 := by rw [h]
    _ = a * (b * a) * b := by simp [pow_two, mul_assoc]

Premises used: HMul.hMul
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
hG : Monoid.exponent G = 2
a b : G
⊢ a * b = b * a

Tactic:
Commute.of_orderOf_dvd_two (fun g => hG ▸ Monoid.order_dvd_exponent g) a b

Premises used: SemiconjBy, Commute, Commute.of_orderOf_dvd_two
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : H.Normal
⊢ Monoid.exponent.{u} (G ⧸ H) ∣ Monoid.exponent G

Tactic:
MonoidHom.exponent_dvd (QuotientGroup.mk'_surjective H)

Premises used: MonoidHom.exponent_dvd, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
hG : Monoid.exponent G = 2
x : G
⊢ x⁻¹ = x

Tactic:
inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hG ▸ Monoid.pow_exponent_eq_one x

Premises used: pow_two, Eq.rec, Monoid.pow_exponent_eq_one, inv_eq_of_mul_eq_one_left
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
x : G
hx : orderOf x = 2
⊢ x⁻¹ = x

Tactic:
inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hx ▸ pow_orderOf_eq_one x

Premises used: pow_two, Eq.rec, pow_orderOf_eq_one, inv_eq_of_mul_eq_one_left
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
x y : G
hx : orderOf x = 2
hy : orderOf y = 2
hxy : x ≠ y
simp : ¬y = 1 ∧ ¬x = 1 ∧ ¬x = y
⊢ x * y ∉ {x, y, 1}

Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff, mul_eq_left, mul_eq_right,
    mul_eq_one_iff_eq_inv, inv_eq_self_of_orderOf_eq_two hy, not_or]

Premises used: mul_eq_right, mul_eq_one_iff_eq_inv, not_or, Set.mem_singleton_iff, inv_eq_self_of_orderOf_eq_two, mul_eq_left, Set.mem_insert_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
x y : G
hx : orderOf x = 2
hy : orderOf y = 2
hxy : x ≠ y
⊢ ¬y = 1 ∧ ¬x = 1 ∧ ¬x = y

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
h : Monoid.exponent G = 2
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}

Tactic:
mul_notMem_of_orderOf_eq_two (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one x) hx)
    (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one y) hy) hxy

Premises used: orderOf_eq_prime, Eq.rec, mul_notMem_of_orderOf_eq_two, Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
⊢ Eq (α := ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
    ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
            if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        ((directSumNeZeroMulHom p n :
            (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
          0) :
      ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
    (0 : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))

Tactic:
simp
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
zero :
  Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      0)
    0
zero₁ zero₂ : Eq (α := ⨁ (i : ι), ZMod (p i ^ n i)) 0 0
⊢ Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
              if h : n i = 0 then 0
              else
                DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          0) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (0 : ⨁ (i : ι), ZMod (p i ^ n i))

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
of :
  Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          x) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))
⊢ Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
              if h : n i = 0 then 0
              else
                DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
              (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
            x)) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))

Tactic:
rw [DirectSum.toAddMonoid_of]

Premises used: DirectSum.toAddMonoid_of
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
pos :
  ∀ (h : n i = 0),
    Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
      ((directSumNeZeroMulHom p n :
            (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
          ((0 : (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) x) :
        ⨁ (i : ι), ZMod (p i ^ n i))
      (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
          x :
        ⨁ (i : ι), ZMod (p i ^ n i))
neg :
  ∀ (h : ¬n i = 0),
    Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
      ((directSumNeZeroMulHom p n :
            (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
          (((DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
                ZMod
                    (p (↑(Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) : ι) ^
                      n (↑(Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) : ι)) →+
                  ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) :
              (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
            x) :
        ⨁ (i : ι), ZMod (p i ^ n i))
      (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
          x :
        ⨁ (i : ι), ZMod (p i ^ n i))
⊢ Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          x) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
rw : HPow.hPow (β := ℕ) (p i) 0 = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ p i ^ n i = 1

Tactic:
rw [h, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
⊢ Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((0 : (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) x) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))

Tactic:
simp [(ZMod.subsingleton_iff.2 <| by rw [h, pow_zero]).elim x 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
M : Type u
inst : AddCommGroup M
inst_1 : Module ℤ M
inst_2 : Module.Finite ℤ M
hM : IsTorsion ℤ M
rcases :
  ∀ (ι : Type) (w : Fintype ι) (p : ι → ℤ) (h : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ)
    (l : M ≃ₗ[ℤ] ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)), Finite M
⊢ Finite M

Tactic:
rcases Module.equiv_directSum_of_isTorsion hM with ⟨ι, _, p, h, e, ⟨l⟩⟩

Premises used: Module.equiv_directSum_of_isTorsion