awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} ∅
neg : Eq (α := ℕ) 0 (sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1})
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have neg₁ : Eq (α := ℕ) 0 (sInf ∅)
Tactic: rw [Monoid.exponent_eq_zero_iff.mpr h, this, Nat.sInf_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} ∅
neg : Eq (α := ℕ) 0 (sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1})
neg₁ : Eq (α := ℕ) 0 (sInf ∅)
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have neg₂ : Eq (α := ℕ) 0 0
Tactic: rw [Monoid.exponent_eq_zero_iff.mpr h, this, Nat.sInf_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
⊢ exponent G = 0 ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1
have rw : (¬∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1
Tactic: rw [exponent_eq_zero_iff, ExponentExists]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
⊢ (¬∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1
have push : (∀ (n : ℕ) (_ : 0 < n), ∃ (g : G), g ^ n ≠ 1) ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1
Tactic: push Not
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
g : G
⊢ g ^ exponent G = 1
have pos : ∀ (h : ExponentExists G), g ^ exponent G = 1
Tactic: by_cases h : ExponentExists G
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
g : G
pos : ∀ (h : ExponentExists G), g ^ exponent G = 1
⊢ g ^ exponent G = 1
have neg : ∀ (h : ¬ExponentExists G), g ^ exponent G = 1
Tactic: by_cases h : ExponentExists G
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1
have pos : g ^ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h = 1
Tactic: simp_rw [exponent, dif_pos h]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1
have neg : HPow.hPow (β := ℕ) g
    (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) =
  1
Tactic: simp_rw [exponent, dif_neg h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
g : G
h : ¬ExponentExists G
neg :
  HPow.hPow (β := ℕ) g
      (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) =
    1
⊢ g ^ exponent G = 1
have neg₁ : HPow.hPow (β := ℕ) g 0 = 1
Tactic: simp_rw [exponent, dif_neg h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
g : G
⊢ g ^ exponent G = 1
have pos : ∀ (h : ExponentExists G), g ^ exponent G = 1
Tactic: classical
  by_cases h : ExponentExists G
  · simp_rw [exponent, dif_pos h]
    exact (Nat.find_spec h).2 g
  · simp_rw [exponent, dif_neg h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
g : G
pos : ∀ (h : ExponentExists G), g ^ exponent G = 1
⊢ g ^ exponent G = 1
have neg : ∀ (h : ¬ExponentExists G), g ^ exponent G = 1
Tactic: classical
  by_cases h : ExponentExists G
  · simp_rw [exponent, dif_pos h]
    exact (Nat.find_spec h).2 g
  · simp_rw [exponent, dif_neg h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))
have rw : g ^ n = g ^ n
Tactic: rw [Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n
have rw : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) sorry ≤ n
Tactic: rw [exponent, dif_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
rw : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n
⊢ exponent G ≤ n
have hc : ExponentExists G
Tactic: rw [exponent, dif_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n
have h : 0 < n ∧ ∀ (g : G), g ^ n = 1
Tactic: apply Nat.find_min'
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n
have rw : (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) ≤ n
Tactic: classical
  rw [exponent, dif_pos]
  · apply Nat.find_min'
    exact ⟨hpos, hG⟩
  · exact ⟨n, hpos, hG⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
rw : (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) ≤ n
⊢ exponent G ≤ n
have rw₁ : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) sorry ≤ n
Tactic: classical
  rw [exponent, dif_pos]
  · apply Nat.find_min'
    exact ⟨hpos, hG⟩
  · exact ⟨n, hpos, hG⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
rw : (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) ≤ n
rw₁ : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) ⋯ ≤ n
⊢ exponent G ≤ n
have hc : ExponentExists G
Tactic: classical
  rw [exponent, dif_pos]
  · apply Nat.find_min'
    exact ⟨hpos, hG⟩
  · exact ⟨n, hpos, hG⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ (g : G), g ^ m ≠ 1
have by_contra! : ∀ (h : ∀ (g : G), g ^ m = 1), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ False
have hcon : exponent G ≤ m
Tactic: have hcon : exponent G ≤ m := exponent_min' m hpos h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
⊢ exponent G = 1 ↔ Subsingleton G
have a_eq_b : ∀ (eq_one : exponent G = 1) (a b : G), a = b
Tactic: refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
a_eq_b : ∀ (eq_one : exponent G = 1) (a b : G), a = b
⊢ exponent G = 1 ↔ Subsingleton G
have le : ∀ (h : Subsingleton G), exponent G ≤ 1
Tactic: refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
a_eq_b : ∀ (eq_one : exponent G = 1) (a b : G), a = b
le : ∀ (h : Subsingleton G), exponent G ≤ 1
⊢ exponent G = 1 ↔ Subsingleton G
have ge : ∀ (h : Subsingleton G), 1 ≤ exponent G
Tactic: refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a = b
have a_eq_b : HPow.hPow (β := ℕ) a 1 = b
Tactic: rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
eq_one : exponent G = 1
a b : G
a_eq_b : HPow.hPow (β := ℕ) a 1 = b
⊢ a = b
have a_eq_b₁ : HPow.hPow (β := ℕ) a 1 = HPow.hPow (β := ℕ) b 1
Tactic: rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
eq_one : exponent G = 1
a b : G
a_eq_b : HPow.hPow (β := ℕ) a 1 = b
a_eq_b₁ : HPow.hPow (β := ℕ) a 1 = HPow.hPow (β := ℕ) b 1
⊢ a = b
have a_eq_b₂ : a ^ exponent G = b ^ exponent G
Tactic: rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
eq_one : exponent G = 1
a b : G
a_eq_b : HPow.hPow (β := ℕ) a 1 = b
a_eq_b₁ : HPow.hPow (β := ℕ) a 1 = HPow.hPow (β := ℕ) b 1
a_eq_b₂ : a ^ exponent G = b ^ exponent G
⊢ a = b
have a_eq_b₃ : 1 = b ^ exponent G
Tactic: rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
eq_one : exponent G = 1
a b : G
a_eq_b : HPow.hPow (β := ℕ) a 1 = b
a_eq_b₁ : HPow.hPow (β := ℕ) a 1 = HPow.hPow (β := ℕ) b 1
a_eq_b₂ : a ^ exponent G = b ^ exponent G
a_eq_b₃ : 1 = b ^ exponent G
⊢ a = b
have a_eq_b₄ : Eq.{u + 1} (α := G) 1 1
Tactic: rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : Subsingleton G
⊢ exponent G ≤ 1
have le : ∀ (g : G), HPow.hPow (β := ℕ) g 1 = 1
Tactic: apply exponent_min' _ Nat.one_pos
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : Subsingleton G
⊢ 0 < exponent G
have ge : ∀ (g : G), HPow.hPow (β := ℕ) g 1 = 1
Tactic: apply exponent_pos_of_exists 1 Nat.one_pos
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
have inl : exponent G ∣ 0 ↔ ∀ (g : G), HPow.hPow (β := ℕ) g 0 = 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hpos)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
inl : exponent G ∣ 0 ↔ ∀ (g : G), HPow.hPow (β := ℕ) g 0 = 1
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
have inr : ∀ (hpos : n > 0), exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hpos)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
have inr : exponent G ∣ n → ∀ (g : G), g ^ n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
inr : exponent G ∣ n → ∀ (g : G), g ^ n = 1
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
have inr₁ : (∀ (g : G), g ^ n = 1) → exponent G ∣ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
h : exponent G ∣ n
g : G
⊢ g ^ n = 1
have inr : ∀ (h : n % exponent G = 0) (g : G), g ^ n = 1
Tactic: rw [Nat.dvd_iff_mod_eq_zero] at h
Cleared hypotheses: h, g
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
⊢ g ^ n = 1
have inr : g ^ (n % exponent G) = 1
Tactic: rw [pow_eq_mod_exponent, h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
inr : g ^ (n % exponent G) = 1
⊢ g ^ n = 1
have inr₁ : HPow.hPow (β := ℕ) g 0 = 1
Tactic: rw [pow_eq_mod_exponent, h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
inr : g ^ (n % exponent G) = 1
inr₁ : HPow.hPow (β := ℕ) g 0 = 1
⊢ g ^ n = 1
have inr₂ : Eq.{u + 1} (α := G) 1 1
Tactic: rw [pow_eq_mod_exponent, h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ∣ n
have inr : ∀ (h : ¬exponent G ∣ n), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : ¬exponent G ∣ n
⊢ False
have h₁ : 0 < n % exponent G
Tactic: rw [Nat.dvd_iff_mod_eq_zero, ← Ne, ← pos_iff_ne_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
⊢ False
have h₂ : n % exponent G < exponent G
Tactic: have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ exponent G ≤ n % exponent G
have apply : ∀ (g : G), g ^ (n % exponent G) = 1
Tactic: apply exponent_min' _ h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ False
have h₃ : exponent G ≤ n % exponent G
Tactic: have h₃ : exponent G ≤ n % exponent G := by
      apply exponent_min' _ h
      simp_rw [← pow_eq_mod_exponent]
      exact hG
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n
have simp_rw : (∀ (g : G), g ^ n = 1) ↔ ∀ (g : G), orderOf g ∣ n
Tactic: simp_rw [exponent_dvd_iff_forall_pow_eq_one, orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
inst_1 : Fintype G
⊢ Finset.lcm.{0, u} (β := G) Finset.univ orderOf ∣ exponent G
have a : ∀ (b : G), Membership.mem (γ := Finset G) Finset.univ b → orderOf b ∣ exponent G
Tactic: apply Finset.lcm_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have this : Fact (Nat.Prime p)
Tactic: haveI := Fact.mk hp
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have inl : ∀ (h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
inl :
  ∀ (h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p 0
Tactic: rw [h, pow_zero, orderOf_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw : orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p 0
⊢ orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₁ : orderOf.{u} (G := G) 1 = 1
Tactic: rw [h, pow_zero, orderOf_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw : orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p 0
rw₁ : orderOf.{u} (G := G) 1 = 1
⊢ orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [h, pow_zero, orderOf_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
⊢ False
have h₁ : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [ht] at h
Cleared hypotheses: h, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
⊢ False
have apply : Eq (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: apply h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
⊢ Eq (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have rw : Eq (α := ℕ) ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
rw : Eq (α := ℕ) ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have rw₁ : Eq (α := ℕ) ((0 : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
rw : Eq (α := ℕ) ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw₁ : Eq (α := ℕ) ((0 : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have he : 0 < exponent G
Tactic: have he : 0 < exponent G :=
    Ne.bot_lt fun ht => by
      rw [ht] at h
      apply h
      rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
he : 0 < exponent G
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have h₁ : p ∈ (exponent G).factorization.support
Tactic: rw [← Finsupp.mem_support_iff] at h
Cleared hypotheses: h, he
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
key : ¬exponent G ∣ exponent G / p
⊢ ∃ (g : G), g ^ (exponent G / p) ≠ 1
have rwa : ∀ (key : ¬∀ (g : G), g ^ (exponent G / p) = 1), ∃ (g : G), g ^ (exponent G / p) ≠ 1
Tactic: rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
key : ¬exponent G ∣ exponent G / p
rwa : ∀ (key : ¬∀ (g : G), g ^ (exponent G / p) = 1), ∃ (g : G), g ^ (exponent G / p) ≠ 1
⊢ ∃ (g : G), g ^ (exponent G / p) ≠ 1
have rwa₁ : ∀ (key : ∃ (x : G), ¬x ^ (exponent G / p) = 1), ∃ (g : G), g ^ (exponent G / p) ≠ 1
Tactic: rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
⊢ ∃ (g : G), g ^ (exponent G / p) ≠ 1
have suffices : ¬exponent G ∣ exponent G / p
Tactic: suffices key : ¬exponent G ∣ exponent G / p by
      rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (g : G) (hg : g ^ (exponent G / p) ≠ 1),
  ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: obtain ⟨g, hg⟩ : ∃ g : G, g ^ (exponent G / p) ≠ 1 := by
    suffices key : ¬exponent G ∣ exponent G / p by
      rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key
    exact fun hd =>
      hp.one_lt.not_ge
        ((mul_le_iff_le_one_left he).mp <|
          Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_primeFactors h) hd)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (k : ℕ) (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k),
  ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ordProj_dvd _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : ∀ (t : ℕ) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
  ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have inr : orderOf (g ^ k) = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine ⟨g ^ k, ?_⟩