awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
hj : exponent.{u_2} (M j) = 0
rw : ∀ (hj : ¬ExponentExists.{u_2} (M j)), ¬ExponentExists ((i : ι) → M i)
rw₁ rw₂ rw₃ : ∀ (hj : ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : M j), g ^ n = 1), ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
rw₄ : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (_ : 0 < n), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
⊢ exponent ((i : ι) → M i) = 0
have h : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (hn : 0 < n) (this : ∃ (g : M j), g ^ n ≠ 1),
  ∃ (g : (i : ι) → M i), g ^ n ≠ 1
Tactic: classical
  rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
  push Not at hj ⊢
  peel hj with n hn _
  obtain ⟨m, hm⟩ := this
  refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
  simpa using congr_fun h j
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
hj : exponent.{u_2} (M j) = 0
rw : ∀ (hj : ¬ExponentExists.{u_2} (M j)), ¬ExponentExists ((i : ι) → M i)
rw₁ rw₂ rw₃ : ∀ (hj : ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : M j), g ^ n = 1), ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
rw₄ : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (_ : 0 < n), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
h :
  ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (hn : 0 < n) (this : ∃ (g : M j), g ^ n ≠ 1),
    ∃ (g : (i : ι) → M i), g ^ n ≠ 1
⊢ exponent ((i : ι) → M i) = 0
have h₁ : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (hn : 0 < n) (m : M j) (hm : m ^ n ≠ 1),
  ∃ (g : (i : ι) → M i), g ^ n ≠ 1
Tactic: classical
  rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
  push Not at hj ⊢
  peel hj with n hn _
  obtain ⟨m, hm⟩ := this
  refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
  simpa using congr_fun h j
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
hj : exponent.{u_2} (M j) = 0
rw : ∀ (hj : ¬ExponentExists.{u_2} (M j)), ¬ExponentExists ((i : ι) → M i)
rw₁ rw₂ rw₃ : ∀ (hj : ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : M j), g ^ n = 1), ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
rw₄ : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (_ : 0 < n), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
h :
  ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (hn : 0 < n) (this : ∃ (g : M j), g ^ n ≠ 1),
    ∃ (g : (i : ι) → M i), g ^ n ≠ 1
h₁ :
  ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (hn : 0 < n) (m : M j) (hm : m ^ n ≠ 1),
    ∃ (g : (i : ι) → M i), g ^ n ≠ 1
⊢ exponent ((i : ι) → M i) = 0
have h₂ : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (hn : 0 < n) (m : M j) (hm : m ^ n ≠ 1)
  (h : Pi.mulSingle (M := M) j m ^ n = 1), m ^ n = 1
Tactic: classical
  rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
  push Not at hj ⊢
  peel hj with n hn _
  obtain ⟨m, hm⟩ := this
  refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
  simpa using congr_fun h j
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂)
⊢ exponent M₂ ∣ exponent M₁
have refine : ∀ (m₂ : M₂), m₂ ^ exponent M₁ = 1
Tactic: refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂
⊢ m₂ ^ exponent M₁ = 1
have obtain : ∀ (m₁ : M₁), HPow.hPow (α := M₂) ((f : (a : M₁) → M₂) m₁ : M₂) (exponent M₁) = 1
Tactic: obtain ⟨m₁, rfl⟩ := hf m₂
Cleared hypotheses: m₂
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₁
⊢ HPow.hPow (α := M₂) ((f : (a : M₁) → M₂) m₁ : M₂) (exponent M₁) = 1
have rw : Eq.{u_3 + 1} (α := M₂) ((f : (a : M₁) → M₂) (m₁ ^ exponent M₁) : M₂) (1 : M₂)
Tactic: rw [← map_pow, pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂)
⊢ HPow.hPow (α := M₂) ((f : (a : M₁) → M₂) m₁ : M₂) (exponent M₁) = 1
have rw₁ : Eq.{u_3 + 1} (α := M₂) ((f : (a : M₁) → M₂) 1 : M₂) (1 : M₂)
Tactic: rw [← map_pow, pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂)
⊢ HPow.hPow (α := M₂) ((f : (a : M₁) → M₂) m₁ : M₂) (exponent M₁) = 1
have rw₂ : Eq.{u_3 + 1} (α := M₂) 1 1
Tactic: rw [← map_pow, pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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)
have refine_1 : exponent ((i : ι) → M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
Tactic: refine dvd_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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)
⊢ exponent ((i : ι) → M i) = Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
have refine_2 : (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) ∣ exponent ((i : ι) → M i)
Tactic: refine dvd_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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)
have refine_1 : ∀ (m : (i : ι) → M i), HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) = 1
Tactic: refine exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
⊢ HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) = 1
have refine_1 : ∀ (i : ι), HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) i = 1 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ HPow.hPow (β := ℕ) m (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) i = 1 i
have refine_1 : orderOf (m i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
Tactic: rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ orderOf (m i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
have refine_1 : exponent.{u_2} (M i) ∣ Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)
Tactic: apply dvd_trans (Monoid.order_dvd_exponent (m i))
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : ι → Type u_2
inst_1 : (i : ι) → Monoid (M i)
⊢ (Finset.lcm univ fun (x : ι) ↦ exponent.{u_2} (M x)) ∣ exponent ((i : ι) → M i)
have apply : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → exponent.{u_2} (M i) ∣ exponent ((i : ι) → M i)
Tactic: apply Finset.lcm_dvd fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂)
have refine_1 : exponent (M₁ × M₂) ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
Tactic: refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂)
⊢ exponent (M₁ × M₂) = @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
have refine_2 : exponent M₁ ∣ exponent (M₁ × M₂)
Tactic: refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂)
⊢ exponent (M₁ × M₂) = @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
have refine_3 : exponent M₂ ∣ exponent (M₁ × M₂)
Tactic: refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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₂)
have refine_1 : ∀ (g : M₁ × M₂), g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂) = 1
Tactic: refine exponent_dvd_of_forall_pow_eq_one fun g ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
⊢ g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂) = 1
have refine_1 : (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).1 = 1.1
Tactic: ext1
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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
⊢ g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂) = 1
have refine_1₁ : (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).2 = 1.2
Tactic: ext1
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
⊢ (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).1 = 1.1
have refine_1 : orderOf g.1 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
Tactic: rw [Prod.pow_fst, Prod.fst_one, ← orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Monoid M₁
inst_1 : Monoid M₂
g : M₁ × M₂
⊢ (g ^ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)).2 = 1.2
have refine_1 : orderOf g.2 ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (exponent M₁) (exponent M₂)
Tactic: rw [Prod.pow_snd, Prod.snd_one, ← orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
h : ∀ (g : G), orderOf g ∣ 2
a b : G
⊢ Commute a b
have h₁ : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
Tactic: simp_rw [orderOf_dvd_iff_pow_eq_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
⊢ Commute a b
have rw : a * (a * b) * b = a * (b * a) * b
Tactic: rw [commute_iff_eq, ← mul_right_inj a, ← mul_left_inj b]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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 2 * HPow.hPow (β := ℕ) b 2 = 1
have rw : 1 * HPow.hPow (β := ℕ) b 2 = 1
Tactic: rw [h, h, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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
⊢ HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2 = 1
have rw₁ : HMul.hMul (α := G) 1 1 = 1
Tactic: rw [h, h, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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
⊢ HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2 = 1
have rw₂ : Eq.{u + 1} (α := G) 1 1
Tactic: rw [h, h, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
inst_1 : IsCancelMul G
a b : G
h : ∀ (g : G), HPow.hPow (β := ℕ) g 2 = 1
⊢ 1 = HPow.hPow (β := ℕ) (a * b) 2
have rw : Eq.{u + 1} (α := G) 1 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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 = a * (b * a) * b
have a₁ : a * (a * b) * b = HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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 * (a * b) * b = a * (b * a) * b
have a₂ : HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) b 2 = 1
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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 * (a * b) * b = a * (b * a) * b
have a₃ : 1 = HPow.hPow (β := ℕ) (a * b) 2
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
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 * (a * b) * b = a * (b * a) * b
have a₄ : HPow.hPow (β := ℕ) (a * b) 2 = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Group G
x y : G
hx : orderOf x = 2
hy : orderOf y = 2
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}
have simp : ¬y = 1 ∧ ¬x = 1 ∧ ¬x = y
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]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
x y : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))
hx :
  (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))
        x) =
    x
hy :
  (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))
        y) =
    y
⊢ (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))
        (x + y)) =
    x + y
have add : (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 : ι)))
    (HAdd.hAdd (α := ⨁ (i : ι), ZMod (p i ^ n i)) (β := ⨁ (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))
          x :
        ⨁ (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))
          y :
        ⨁ (i : ι), ZMod (p i ^ n i))) =
  x + y
Tactic: rw [map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
x : ⨁ (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))
        x) =
    x
have zero : 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: induction x using DirectSum.induction_on with
    | zero => simp
    | of i x =>
      rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of, DirectSum.toAddMonoid_of,
        dif_neg i.prop]
    | add x y hx hy => rw [map_add, map_add, hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
⊢ 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))
have 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
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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
⊢ 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))
have zero₁ : Eq (α := ⨁ (i : ι), ZMod (p i ^ n i)) 0 0
Tactic: rw [map_zero, map_zero]