awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ False
have h : orderOf t < orderOf (t ^ p ^ k * g)
Tactic: suffices orderOf t < orderOf (t ^ p ^ k * g) by
    rw [ht] at this
    exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)
-- 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 : ℕ)
⊢ orderOf t < orderOf (t ^ p ^ k * g)
have hpk : p ^ k ∣ orderOf t
Tactic: have hpk : p ^ k ∣ orderOf t := Nat.ordProj_dvd _ _
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k
have rw : orderOf t / (orderOf t).gcd (p ^ k) = orderOf t / p ^ k
Tactic: rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
rw : orderOf t / (orderOf t).gcd (p ^ k) = orderOf t / p ^ k
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k
have rw₁ : orderOf t / p ^ k = orderOf t / p ^ k
Tactic: rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
-- 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 : ℕ)
hpk : p ^ k ∣ orderOf t
⊢ orderOf t < orderOf (t ^ p ^ k * g)
have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
Tactic: have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
    rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
⊢ orderOf t < orderOf (t ^ p ^ k * g)
have h : ∀ (a : ℕ) (ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1), orderOf t < orderOf (t ^ p ^ k * g)
Tactic: obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
⊢ (orderOf (t ^ p ^ k)).Coprime (orderOf g)
have rw : p.Coprime (orderOf (t ^ p ^ k))
Tactic: rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
⊢ p.Coprime (orderOf (t ^ p ^ k))
have apply : ¬p ∣ orderOf (t ^ p ^ k)
Tactic: apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
⊢ ¬p ∣ orderOf (t ^ p ^ k)
have nth_rw : ¬HPow.hPow (β := ℕ) p 1 ∣ orderOf (t ^ p ^ k)
Tactic: nth_rw 1 [← pow_one p]
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
⊢ 1 = HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have rw : 1 = HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf t).factorization - (p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: rw [hpk', Nat.factorization_div hpk]
-- 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 : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
⊢ ¬HPow.hPow (β := ℕ) p 1 ∣ orderOf (t ^ p ^ k)
have this : 1 = HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
      rw [hpk', Nat.factorization_div hpk]
      simp [k, hp]
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
this : 1 = HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ ¬HPow.hPow (β := ℕ) p 1 ∣ orderOf (t ^ p ^ k)
have rw : ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
    orderOf (t ^ p ^ k)
Tactic: rw [this]
-- 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 : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
⊢ orderOf t < orderOf (t ^ p ^ k * g)
have hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
Tactic: have hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g) := by
    rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
    apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
    nth_rw 1 [← pow_one p]
    have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
      rw [hpk', Nat.factorization_div hpk]
      simp [k, hp]
    rw [this]
    -- Porting note: convert made to_additive complain
    exact Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp
-- 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
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k * g)
have h : 1 < p ^ (a + 1)
Tactic: rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk',
    hg, ha, hk, pow_add, pow_add, pow_one, ← mul_assoc, ← mul_assoc,
    Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| hG.orderOf_pos t, ← pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
have pos : ExponentExists G → exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
Tactic: by_cases ExponentExists G
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
pos : ExponentExists G → exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
have neg : ¬ExponentExists G → exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
Tactic: by_cases ExponentExists G
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ¬ExponentExists G
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
have he₁ : exponent G = 0
Tactic: rw [← exponent_eq_zero_iff] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
have rw : Eq (α := ℕ) 0 (sSup (Set.range fun (g : G) ↦ orderOf g))
Tactic: rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
rw : Eq (α := ℕ) 0 (sSup (Set.range fun (g : G) ↦ orderOf g))
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
have H : ∀ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a → a ≤ exponent G
Tactic: rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
H : ∀ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a → a ≤ exponent G
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
have H' : ∀ w < exponent G, ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ w < a
Tactic: rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a → a ≤ exponent G
have H : ∀ (a : G), orderOf a ≤ exponent G
Tactic: simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
⊢ ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ x < a
have H' : ∀ (g : G) (hg : orderOf g = exponent G),
  ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ x < a
Tactic: obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
g : G
hg : orderOf g = exponent G
⊢ ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ x < a
have hx₁ : x < orderOf g
Tactic: rw [← hg] at hx
Cleared hypotheses: hx, hg
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ x < a
have H' : ∃ (a : G), x < orderOf a
Tactic: simp_rw [Set.mem_range, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
⊢ exponent G = if ∃ (g : G), orderOf g = 0 then 0 else ⨆ (g : G), orderOf g
have pos : ∀ (h : ∃ (g : G), orderOf g = 0), exponent G = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
pos : ∀ (h : ∃ (g : G), orderOf g = 0), exponent G = 0
⊢ exponent G = if ∃ (g : G), orderOf g = 0 then 0 else ⨆ (g : G), orderOf g
have neg : ∀ (h : ¬∃ (g : G), orderOf g = 0), exponent G = ⨆ (g : G), orderOf g
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CommMonoid G
h : ∃ (g : G), orderOf g = 0
⊢ exponent G = 0
have pos : ∀ (g : G) (hg : orderOf g = 0), exponent G = 0
Tactic: obtain ⟨g, hg⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : CommMonoid G
h : ¬∃ (g : G), orderOf g = 0
⊢ exponent G = ⨆ (g : G), orderOf g
have this : ∀ (x : G), ¬orderOf x = 0
Tactic: have := not_exists.mp h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : CancelCommMonoid G
inst_1 : Fintype G
⊢ exponent G = (Finset.image.{u, 0} (α := G) orderOf Finset.univ).max' ⋯
have rw : exponent G = iSup.{0, u + 1} (ι := G) orderOf
Tactic: rw [← Finset.Nonempty.csSup_eq_max', Finset.coe_image, Finset.coe_univ, Set.image_univ, ← iSup]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Group G
n : ℤ
⊢ (↑(Monoid.exponent G) : ℤ) ∣ n ↔ ∀ (g : G), g ^ n = 1
have simp_rw : Monoid.exponent G ∣ n.natAbs ↔ ∀ (g : G), g ^ n = 1
Tactic: simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Group G
n : ℤ
simp_rw : Monoid.exponent G ∣ n.natAbs ↔ ∀ (g : G), g ^ n = 1
⊢ (↑(Monoid.exponent G) : ℤ) ∣ n ↔ ∀ (g : G), g ^ n = 1
have simp_rw₁ : (∀ (g : G), g ^ n.natAbs = 1) ↔ ∀ (g : G), g ^ n = 1
Tactic: simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Group G
n m : ℤ
⊢ (↑(Monoid.exponent G) : ℤ) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m
have simp_rw : (∀ (g : G), g ^ (n - m) = 1) ↔ ∀ (g : G), g ^ n = g ^ m
Tactic: simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Group G
n m : ℤ
simp_rw : (∀ (g : G), g ^ (n - m) = 1) ↔ ∀ (g : G), g ^ n = g ^ m
⊢ (↑(Monoid.exponent G) : ℤ) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m
have simp_rw₁ : (∀ (g : G), g ^ n * (g ^ m)⁻¹ = 1) ↔ ∀ (g : G), g ^ n = g ^ m
Tactic: simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]
-- 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
⊢ exponent ((i : ι) → M i) = 0
have rw : ∀ (hj : ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : M j), g ^ n = 1), ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
Tactic: rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
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 : ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : M j), g ^ n = 1
⊢ ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
have push : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (_ : 0 < n), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
Tactic: push Not at hj ⊢
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 : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1
⊢ ∀ (n : ℕ) (_ : 0 < n), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
have h : ∀ (n : ℕ) (hn : 0 < n) (this : ∃ (g : M j), g ^ n ≠ 1), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
Tactic: peel hj with n hn _
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
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
have h : ∀ (m : M j) (hm : m ^ n ≠ 1), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
Tactic: obtain ⟨m, hm⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
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
have h : ∀ (h : Pi.mulSingle (M := M) j m ^ n = 1), m ^ n = 1
Tactic: refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
-- 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
⊢ exponent ((i : ι) → M i) = 0
have rw : ∀ (hj : ¬ExponentExists.{u_2} (M j)), ¬ExponentExists ((i : ι) → M i)
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)
⊢ exponent ((i : ι) → M i) = 0
have rw₁ : ∀ (hj : ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : M j), g ^ n = 1), ¬∃ (n : ℕ), 0 < n ∧ ∀ (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
⊢ exponent ((i : ι) → M i) = 0
have rw₄ : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (_ : 0 < n), ∃ (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