awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
pos :
  ∀ (hy : orderOf y = 0),
    ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
have neg : ∀ (hy : ¬orderOf y = 0),
  ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
Tactic: by_cases hy : orderOf y = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
have pos : ∀ (hy : orderOf y = 0),
  ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
Tactic: by_cases hy : orderOf y = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
pos :
  ∀ (hy : orderOf y = 0),
    ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
have neg : ∀ (hy : ¬orderOf y = 0),
  ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
Tactic: by_cases hy : orderOf y = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
⊢ exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p
have refine_1 : ∀ (hG : exponent G = p) (g : G) (hg : g ≠ 1), orderOf g = p
Tactic: refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
refine_1 : ∀ (hG : exponent G = p) (g : G) (hg : g ≠ 1), orderOf g = p
⊢ exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p
have refine_2 : ∀ (h : ∀ (g : G), g ≠ 1 → orderOf g = p), exponent G ∣ p
Tactic: refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
refine_1 : ∀ (hG : exponent G = p) (g : G) (hg : g ≠ 1), orderOf g = p
refine_2 : ∀ (h : ∀ (g : G), g ≠ 1 → orderOf g = p), exponent G ∣ p
⊢ exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p
have refine_3 : ∀ (h : ∀ (g : G), g ≠ 1 → orderOf g = p), p ∣ exponent G
Tactic: refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : g ≠ 1
⊢ orderOf g = p
have hg₁ : ¬orderOf g = 1
Tactic: rw [Ne, ← orderOf_eq_one_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ exponent G ∣ p
have refine_2 : ∀ (g : G), orderOf g ∣ p
Tactic: rw [exponent_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
⊢ orderOf g ∣ p
have pos : ∀ (hg : g = 1), orderOf g ∣ p
Tactic: by_cases hg : g = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
pos : ∀ (hg : g = 1), orderOf g ∣ p
⊢ orderOf g ∣ p
have neg : ∀ (hg : ¬g = 1), orderOf g ∣ p
Tactic: by_cases hg : g = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
hg : ¬g = 1
⊢ orderOf g ∣ p
have neg : p ∣ p
Tactic: rw [h g hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G
have refine_3 : ∀ (g : G) (hg : g ≠ 1), p ∣ exponent G
Tactic: obtain ⟨g, hg⟩ := exists_ne (1 : G)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite
have refine_1 : ∀ (he : exponent G ≠ 0), (Set.range.{0, u + 1} (ι := G) orderOf).Finite
Tactic: refine ⟨fun he => ?_, fun he => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
refine_1 : ∀ (he : exponent G ≠ 0), (Set.range.{0, u + 1} (ι := G) orderOf).Finite
⊢ exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite
have refine_2 : ∀ (he : (Set.range.{0, u + 1} (ι := G) orderOf).Finite), exponent G ≠ 0
Tactic: refine ⟨fun he => ?_, fun he => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ (Set.range.{0, u + 1} (ι := G) orderOf).Finite
have refine_1 : ∀ (h : ¬(Set.range.{0, u + 1} (ι := G) orderOf).Finite), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h_1 : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range.{0, u + 1} (ι := G) orderOf).Finite
⊢ False
have refine_1 : ∀ (t : G) (het : exponent G < orderOf t), False
Tactic: obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
⊢ exponent G ≠ 0
have refine_2 : ∀ (t : Finset ℕ) (ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf)
  (exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite),
  exponent G ≠ 0
Tactic: lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
⊢ 0 < t.prod id
have refine : ∀ (a : ℕ) (ha : a ∈ t), 0 < id a
Tactic: refine Finset.prod_pos fun a ha => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
a : ℕ
ha : a ∈ t
⊢ 0 < id a
have ha₁ : a ∈ Set.range.{0, u + 1} (ι := G) orderOf
Tactic: rw [← Finset.mem_coe, ht] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
a : ℕ
ha : a ∈ Set.range.{0, u + 1} (ι := G) orderOf
⊢ 0 < id a
have obtain : ∀ (k : G), 0 < id (orderOf k)
Tactic: obtain ⟨k, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
⊢ exponent G ≠ 0
have htpos : 0 < t.prod id
Tactic: have htpos : 0 < t.prod id := by
      refine Finset.prod_pos fun a ha => ?_
      rw [← Finset.mem_coe, ht] at ha
      obtain ⟨k, rfl⟩ := ha
      exact h k
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
h_1 : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
htpos : 0 < t.prod id
this : exponent G ∣ t.prod id
h : exponent G = 0
⊢ False
have this₁ : t.prod id = 0
Tactic: rw [h, zero_dvd_iff] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
htpos : 0 < t.prod id
⊢ exponent G ≠ 0
have refine_2 : exponent G ∣ t.prod id
Tactic: suffices exponent G ∣ t.prod id by
      intro h
      rw [h, zero_dvd_iff] at this
      exact htpos.ne' this
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
htpos : 0 < t.prod id
⊢ exponent G ∣ t.prod id
have refine_2 : ∀ (g : G), orderOf g ∣ t.prod id
Tactic: rw [exponent_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∣ t.prod id
have apply : orderOf g ∈ t
Tactic: apply Finset.dvd_prod_of_mem id (?_ : orderOf g ∈ _)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : (↑t : Set ℕ) = Set.range.{0, u + 1} (ι := G) orderOf
exponent_ne_zero_iff_range_orderOf_finite : ∀ (h : ∀ (g : G), 0 < orderOf g), exponent G ≠ 0 ↔ (↑t : Set ℕ).Finite
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∈ t
have rw : orderOf g ∈ Set.range.{0, u + 1} (ι := G) orderOf
Tactic: rw [← Finset.mem_coe, ht]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
have this : exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite
Tactic: have := exponent_ne_zero_iff_range_orderOf_finite h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
have rwa : ∀ (this : ¬exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite),
  exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
Tactic: rwa [Ne, not_iff_comm, Iff.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite
rwa :
  ∀ (this : ¬exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite),
    exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
⊢ exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
have rwa₁ : ∀ (this : ¬(Set.range.{0, u + 1} (ι := G) orderOf).Finite ↔ exponent G = 0),
  exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
Tactic: rwa [Ne, not_iff_comm, Iff.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite
rwa :
  ∀ (this : ¬exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite),
    exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
rwa₁ :
  ∀ (this : ¬(Set.range.{0, u + 1} (ι := G) orderOf).Finite ↔ exponent G = 0),
    exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
⊢ exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
have rwa₂ : ∀ (this : exponent G = 0 ↔ ¬(Set.range.{0, u + 1} (ι := G) orderOf).Finite),
  exponent G = 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Infinite
Tactic: rwa [Ne, not_iff_comm, Iff.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
H : Type u_1
inst_1 : Monoid H
e : G →* H
e_inj : Function.Injective.{u + 1, u_1 + 1} (α := G) (β := H) (⇑e : (a : G) → H)
g : G
⊢ Eq.{u_1 + 1} (α := H) ((e : (a : G) → H) (g ^ exponent H) : H) ((e : (a : G) → H) 1 : H)
have rw : HPow.hPow (α := H) ((e : (a : G) → H) g : H) (exponent H) = (e : (a : G) → H) 1
Tactic: rw [map_pow, pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
H : Type u_1
inst_1 : Monoid H
e : G →* H
e_inj : Function.Injective.{u + 1, u_1 + 1} (α := G) (β := H) (⇑e : (a : G) → H)
g : G
rw : HPow.hPow (α := H) ((e : (a : G) → H) g : H) (exponent H) = (e : (a : G) → H) 1
⊢ Eq.{u_1 + 1} (α := H) ((e : (a : G) → H) (g ^ exponent H) : H) ((e : (a : G) → H) 1 : H)
have rw₁ : Eq.{u_1 + 1} (α := H) (1 : H) ((e : (a : G) → H) 1 : H)
Tactic: rw [map_pow, pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
H : Type u_1
inst_1 : Monoid H
e : G →* H
e_inj : Function.Injective.{u + 1, u_1 + 1} (α := G) (β := H) (⇑e : (a : G) → H)
g : G
rw : HPow.hPow (α := H) ((e : (a : G) → H) g : H) (exponent H) = (e : (a : G) → H) 1
rw₁ : Eq.{u_1 + 1} (α := H) (1 : H) ((e : (a : G) → H) 1 : H)
⊢ Eq.{u_1 + 1} (α := H) ((e : (a : G) → H) (g ^ exponent H) : H) ((e : (a : G) → H) 1 : H)
have rw₂ : Eq.{u_1 + 1} (α := H) 1 1
Tactic: rw [map_pow, pow_exponent_eq_one, map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
⊢ g ^ exponent.{u} ↥S = 1
have this : Subtype.mk (p := fun (x : G) ↦ x ∈ S) g g_in_s ^ exponent.{u} ↥S = 1
Tactic: have := Monoid.pow_exponent_eq_one (⟨g, g_in_s⟩ : S)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
this : Subtype.mk (p := fun (x : G) ↦ x ∈ S) g g_in_s ^ exponent.{u} ↥S = 1
⊢ g ^ exponent.{u} ↥S = 1
have rwa : ∀ (this : Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g ^ exponent.{u} ↥S) sorry = 1), g ^ exponent.{u} ↥S = 1
Tactic: rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
this : Subtype.mk (p := fun (x : G) ↦ x ∈ S) g g_in_s ^ exponent.{u} ↥S = 1
rwa : ∀ (this : Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g ^ exponent.{u} ↥S) ⋯ = 1), g ^ exponent.{u} ↥S = 1
⊢ g ^ exponent.{u} ↥S = 1
have rwa₁ : ∀ (this : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g ^ exponent.{u} ↥S) sorry) : G) = 1), g ^ exponent.{u} ↥S = 1
Tactic: rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1
have refine_1 : 0 < Finset.lcm.{0, u} (β := G) Finset.univ orderOf
Tactic: refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
refine_1 : 0 < Finset.lcm.{0, u} (β := G) Finset.univ orderOf
⊢ ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1
have refine_2 : ∀ (g : G), g ^ Finset.lcm.{0, u} (β := G) Finset.univ orderOf = 1
Tactic: refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.lcm.{0, u} (β := G) Finset.univ orderOf = 1
have refine_2 : orderOf g ∣ exponent G
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, lcm_orderOf_eq_exponent]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
inst_2 : Nontrivial G
⊢ 1 < exponent G
have rw : exponent G ≠ 0 ∧ exponent G ≠ 1
Tactic: rw [Nat.one_lt_iff_ne_zero_and_ne_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
⊢ ∃ (g : G), orderOf g = exponent G
have he : exponent G ≠ 0
Tactic: have he := hG.exponent_ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
⊢ ∃ (g : G), orderOf g = exponent G
have hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
Tactic: have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
⊢ ∃ (g : G), orderOf g = exponent G
have hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
Tactic: have hfin : (Set.range (orderOf : G → ℕ)).Finite := by
    rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
⊢ ∃ (g : G), orderOf g = exponent G
have obtain : ∀ (t : G) (ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)), ∃ (g : G), orderOf g = exponent G
Tactic: obtain ⟨t, ht⟩ := hne.csSup_mem hfin
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
⊢ ∃ (g : G), orderOf g = exponent G
have h : orderOf t = exponent G
Tactic: use t
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
⊢ orderOf t = exponent G
have h : exponent G ∣ orderOf t
Tactic: apply Nat.dvd_antisymm (order_dvd_exponent _)
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
⊢ exponent G ∣ orderOf t
have h : (exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList
Tactic: refine Nat.dvd_of_primeFactorsList_subperm he ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
⊢ (exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList
have h : ∀ x ∈ (exponent G).primeFactorsList,
  List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList
Tactic: rw [List.subperm_ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
⊢ ∀ x ∈ (exponent G).primeFactorsList,
    List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList
have h : ∀ (p : ℕ) (hp : p ∈ (exponent G).primeFactorsList)
  (hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList), False
Tactic: by_contra! ⟨p, hp, hpe⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : p ∈ (exponent G).primeFactorsList
hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList
⊢ False
have hp₁ : Nat.Prime p
Tactic: replace hp := Nat.prime_of_mem_primeFactorsList hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList
hp : Nat.Prime p
⊢ False
have hpe₁ : LT.lt (α := ℕ) (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: simp only [Nat.primeFactorsList_count_eq] at hpe
Cleared hypotheses: hpe
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
hpe :
  LT.lt (α := ℕ) (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpe₁ :
  let k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p;
  k < ((exponent G).factorization : (a : ℕ) → ℕ) p
⊢ False
have hk : let k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p;
k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
Tactic: set k := (orderOf t).factorization p with hk
Cleared hypotheses: hpe
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
⊢ False
have h : ∀ (g : G) (hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)), False
Tactic: obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
this : orderOf t < orderOf (t ^ p ^ k * g)
⊢ False
have this₁ : sSup (Set.range.{0, u + 1} (ι := G) orderOf) < orderOf (t ^ p ^ k * g)
Tactic: rw [ht] at this
Cleared hypotheses: this