awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Exponent
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 : ℕ)

Tactic:
have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
      rw [hpk', Nat.factorization_div hpk]
      simp [k, hp]
-- Module: Mathlib.GroupTheory.Exponent
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 : ℕ)
rw :
  ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
      orderOf (t ^ p ^ k)
⊢ ¬HPow.hPow (β := ℕ) p 1 ∣ orderOf (t ^ p ^ k)

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Exponent
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 : ℕ)
⊢ ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
      orderOf (t ^ p ^ k)

Tactic:
Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp

Premises used: Nat.pow_succ_factorization_not_dvd, Monoid.ExponentExists.orderOf_pos, LT.lt.ne', HPow.hPow
-- Module: Mathlib.GroupTheory.Exponent
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 : ℕ)
⊢ ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
      orderOf (t ^ p ^ k)

Tactic:
exact Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp

Premises used: Nat.pow_succ_factorization_not_dvd, Monoid.ExponentExists.orderOf_pos, LT.lt.ne', HPow.hPow
-- Module: Mathlib.GroupTheory.Exponent
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)

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
-- Module: Mathlib.GroupTheory.Exponent
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)
h : 1 < p ^ (a + 1)
h₁ : HPow.hPow (β := ℕ) p (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) ∣ orderOf t
⊢ orderOf t < orderOf (t ^ p ^ k * g)

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]

Premises used: Nat.div_mul_cancel, pow_succ, Monoid.ExponentExists.orderOf_pos, mul_assoc, pow_add, Commute.orderOf_mul_eq_mul_orderOf_of_coprime, pow_one, lt_mul_iff_one_lt_right, Commute.all
-- Module: Mathlib.GroupTheory.Exponent
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)
⊢ 1 < p ^ (a + 1)

Tactic:
one_lt_pow₀ hp.one_lt a.succ_ne_zero

Premises used: Nat.Prime.one_lt, Nat.succ_ne_zero, one_lt_pow₀
-- Module: Mathlib.GroupTheory.Exponent
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)
⊢ 1 < p ^ (a + 1)

Tactic:
exact one_lt_pow₀ hp.one_lt a.succ_ne_zero

Premises used: Nat.Prime.one_lt, Nat.succ_ne_zero, one_lt_pow₀
-- Module: Mathlib.GroupTheory.Exponent
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)
⊢ HPow.hPow (β := ℕ) p (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) ∣ orderOf t

Tactic:
hpk
-- Module: Mathlib.GroupTheory.Exponent
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)
⊢ HPow.hPow (β := ℕ) p (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) ∣ orderOf t

Tactic:
exact hpk
-- Module: Mathlib.GroupTheory.Exponent
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)
neg : ¬ExponentExists G → exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)

Tactic:
by_cases ExponentExists G

Premises used: Monoid.ExponentExists
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ¬ExponentExists G
⊢ exponent G = 0

Tactic:
rw [← exponent_eq_zero_iff] at he

Premises used: Monoid.exponent_eq_zero_iff
-- Module: Mathlib.GroupTheory.Exponent
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))
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ exponent G = 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]

Premises used: Set.Infinite.Nat.sSup_eq_zero, Iff.mp, Monoid.exponent_eq_zero_iff_range_orderOf_infinite
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h_1 : ¬ExponentExists G
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)

Tactic:
case neg he =>
    rw [← exponent_eq_zero_iff] at he
    rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]

Premises used: Monoid.exponent_eq_zero_iff, Set.Infinite.Nat.sSup_eq_zero
-- Module: Mathlib.GroupTheory.Exponent
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
H' : ∀ w < exponent G, ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ w < a
⊢ exponent G = sSup (Set.range fun (g : G) ↦ orderOf g)

Tactic:
rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]

Premises used: Set.range_nonempty, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
H : ∀ (a : G), orderOf a ≤ exponent G
⊢ ∀ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a → a ≤ exponent G

Tactic:
simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ (a : G), orderOf a ≤ exponent G

Tactic:
orderOf_le_exponent he

Premises used: Monoid.orderOf_le_exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ (a : G), orderOf a ≤ exponent G

Tactic:
exact orderOf_le_exponent he

Premises used: Monoid.orderOf_le_exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
H' :
  ∀ (g : G) (hg : orderOf g = exponent G),
    ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ x < a
⊢ ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ x < a

Tactic:
obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he

Premises used: Monoid.exists_orderOf_eq_exponent
-- Module: Mathlib.GroupTheory.Exponent
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
⊢ x < orderOf g

Tactic:
rw [← hg] at hx
-- Module: Mathlib.GroupTheory.Exponent
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
hx₁ : x < orderOf g
⊢ orderOf g = exponent G

Tactic:
rw [← hg] at hx
-- Module: Mathlib.GroupTheory.Exponent
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
H' : ∃ (a : G), x < orderOf a
⊢ ∃ (a : ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (g : G) ↦ orderOf g) a ∧ x < a

Tactic:
simp_rw [Set.mem_range, exists_exists_eq_and]

Premises used: Set.mem_range, exists_exists_eq_and
-- Module: Mathlib.GroupTheory.Exponent
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 : G), x < orderOf a

Tactic:
⟨g, hx⟩

Premises used: Exists.intro
-- Module: Mathlib.GroupTheory.Exponent
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 : G), x < orderOf a

Tactic:
exact ⟨g, hx⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
pos : ∀ (h : ∃ (g : G), orderOf g = 0), exponent G = 0
neg : ∀ (h : ¬∃ (g : G), orderOf g = 0), exponent G = ⨆ (g : G), orderOf g
⊢ exponent G = if ∃ (g : G), orderOf g = 0 then 0 else ⨆ (g : G), orderOf g

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ∃ (g : G), orderOf g = 0
pos : ∀ (g : G) (hg : orderOf g = 0), exponent G = 0
⊢ exponent G = 0

Tactic:
obtain ⟨g, hg⟩ := h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0

Tactic:
exponent_eq_zero_of_order_zero hg

Premises used: Monoid.exponent_eq_zero_of_order_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0

Tactic:
exact exponent_eq_zero_of_order_zero hg

Premises used: Monoid.exponent_eq_zero_of_order_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ¬∃ (g : G), orderOf g = 0
⊢ ∀ (x : G), ¬orderOf x = 0

Tactic:
have := not_exists.mp h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ¬∃ (g : G), orderOf g = 0
this : ∀ (x : G), ¬orderOf x = 0
⊢ exponent G = ⨆ (g : G), orderOf g

Tactic:
exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

Premises used: Monoid.exponent_eq_iSup_orderOf, Ne.bot_lt
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
h : ¬∃ (g : G), orderOf g = 0
this : ∀ (x : G), ¬orderOf x = 0
⊢ exponent G = ⨆ (g : G), orderOf g

Tactic:
exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

Premises used: Monoid.exponent_eq_iSup_orderOf, Ne.bot_lt
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CancelCommMonoid G
inst_1 : Fintype G
⊢ 1 ∈ Finset.image.{u, 0} (α := G) orderOf Finset.univ

Tactic:
simp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CancelCommMonoid G
inst_1 : Fintype G
rw : exponent G = iSup.{0, u + 1} (ι := G) orderOf
⊢ exponent G = (Finset.image.{u, 0} (α := G) orderOf Finset.univ).max' ⋯

Tactic:
rw [← Finset.Nonempty.csSup_eq_max', Finset.coe_image, Finset.coe_univ, Set.image_univ, ← iSup]

Premises used: Set.image_univ, Finset.coe_univ, iSup, Finset.coe_image, Finset.Nonempty.csSup_eq_max'
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CancelCommMonoid G
inst_1 : Fintype G
⊢ exponent G = iSup.{0, u + 1} (ι := G) orderOf

Tactic:
exponent_eq_iSup_orderOf orderOf_pos

Premises used: Monoid.exponent_eq_iSup_orderOf, orderOf_pos
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CancelCommMonoid G
inst_1 : Fintype G
⊢ exponent G = iSup.{0, u + 1} (ι := G) orderOf

Tactic:
exact exponent_eq_iSup_orderOf orderOf_pos

Premises used: Monoid.exponent_eq_iSup_orderOf
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
inst_1 : Fintype G
⊢ Monoid.exponent G ∣ Fintype.card G

Tactic:
Monoid.exponent_dvd.mpr <| fun _ => orderOf_dvd_card

Premises used: Iff.mpr, Monoid.exponent_dvd, orderOf_dvd_card
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
⊢ Monoid.exponent G ∣ Nat.card G

Tactic:
Monoid.exponent_dvd.mpr orderOf_dvd_natCard

Premises used: Iff.mpr, Monoid.exponent_dvd, orderOf_dvd_natCard
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
H : Subgroup G
⊢ Monoid.exponent.{u} ↥H.toSubmonoid = Monoid.exponent.{u} ↥H

Tactic:
Monoid.exponent_eq_of_mulEquiv (MulEquiv.subgroupCongr rfl)

Premises used: MulEquiv.subgroupCongr, Monoid.exponent_eq_of_mulEquiv, rfl
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
⊢ Monoid.exponent.{u} ↥⊤ = Monoid.exponent G

Tactic:
Monoid.exponent_eq_of_mulEquiv topEquiv

Premises used: Monoid.exponent_eq_of_mulEquiv, Subgroup.topEquiv
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
H : Subgroup G
g : G
g_in_H : g ∈ H
⊢ g ^ Monoid.exponent.{u} ↥H = 1

Tactic:
exponent_toSubmonoid H ▸ Submonoid.pow_exponent_eq_one g_in_H

Premises used: Submonoid.pow_exponent_eq_one, Eq.rec, Subgroup.exponent_toSubmonoid
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
n : ℤ
simp_rw : Monoid.exponent G ∣ n.natAbs ↔ ∀ (g : G), g ^ n = 1
simp_rw₁ : (∀ (g : G), g ^ n.natAbs = 1) ↔ ∀ (g : G), g ^ n = 1
⊢ (↑(Monoid.exponent G) : ℤ) ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]

Premises used: Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one, Int.natCast_dvd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Group G
n m : ℤ
simp_rw : (∀ (g : G), g ^ (n - m) = 1) ↔ ∀ (g : G), g ^ n = g ^ m
simp_rw₁ : (∀ (g : G), g ^ n * (g ^ m)⁻¹ = 1) ↔ ∀ (g : G), g ^ n = g ^ m
⊢ (↑(Monoid.exponent G) : ℤ) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m

Tactic:
simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Premises used: mul_inv_eq_one, zpow_sub, Group.exponent_dvd_iff_forall_zpow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
hj : exponent.{u_2} (M j) = 0
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

Tactic:
rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢

Premises used: Monoid.ExponentExists, Monoid.exponent_eq_zero_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
hj : ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : M j), g ^ n = 1
push : ∀ (hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1) (n : ℕ) (_ : 0 < n), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
⊢ ¬∃ (n : ℕ), 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1

Tactic:
push Not at hj ⊢

Premises used: Not
-- Module: Mathlib.GroupTheory.Exponent
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ) (_ : 0 < n), ∃ (g : M j), g ^ n ≠ 1
h : ∀ (n : ℕ) (hn : 0 < n) (this : ∃ (g : M j), g ^ n ≠ 1), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
⊢ ∀ (n : ℕ) (_ : 0 < n), ∃ (g : (i : ι) → M i), g ^ n ≠ 1

Tactic:
peel hj with n hn _
-- Module: Mathlib.GroupTheory.Exponent
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
h : ∀ (m : M j) (hm : m ^ n ≠ 1), ∃ (g : (i : ι) → M i), g ^ n ≠ 1
⊢ ∃ (g : (i : ι) → M i), g ^ n ≠ 1

Tactic:
obtain ⟨m, hm⟩ := this
-- Module: Mathlib.GroupTheory.Exponent
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

Tactic:
⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩

Premises used: Exists.intro, Pi.mulSingle
-- Module: Mathlib.GroupTheory.Exponent
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
h : ∀ (h : Pi.mulSingle (M := M) j m ^ n = 1), m ^ n = 1
⊢ ∃ (g : (i : ι) → M i), g ^ n ≠ 1

Tactic:
refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
-- Module: Mathlib.GroupTheory.Exponent
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
h : Pi.mulSingle (M := M) j m ^ n = 1
⊢ m ^ n = 1

Tactic:
simpa using congr_fun h j

Premises used: congr_fun
-- Module: Mathlib.GroupTheory.Exponent
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
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
⊢ exponent ((i : ι) → M i) = 0

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

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

Tactic:
Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one