awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
iterate : ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
hx₁ : orderOf y ≠ 0
hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
hx₂ : orderOf x ≠ 0
hn₁ : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))

Tactic:
iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]

Premises used: Nat.Coprime, orderOf_pow_orderOf_div
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)

Tactic:
simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Premises used: Nat.coprime_factorizationLCMLeft_factorizationLCMRight, Nat.factorizationLCMLeft_mul_factorizationLCMRight, Nat.factorizationLCMLeft_dvd_left, Nat.factorizationLCMRight_dvd_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf y ≠ 0

Tactic:
simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Premises used: Nat.coprime_factorizationLCMLeft_factorizationLCMRight, Nat.factorizationLCMLeft_mul_factorizationLCMRight, Nat.factorizationLCMLeft_dvd_left, Nat.factorizationLCMRight_dvd_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y

Tactic:
simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Premises used: Nat.coprime_factorizationLCMLeft_factorizationLCMRight, Nat.factorizationLCMLeft_mul_factorizationLCMRight, Nat.factorizationLCMLeft_dvd_left, Nat.factorizationLCMRight_dvd_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

Tactic:
simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Premises used: Nat.coprime_factorizationLCMLeft_factorizationLCMRight, Nat.factorizationLCMLeft_mul_factorizationLCMRight, Nat.factorizationLCMLeft_dvd_left, Nat.factorizationLCMRight_dvd_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x

Tactic:
simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Premises used: Nat.coprime_factorizationLCMLeft_factorizationLCMRight, Nat.factorizationLCMLeft_mul_factorizationLCMRight, Nat.factorizationLCMLeft_dvd_left, Nat.factorizationLCMRight_dvd_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1

Tactic:
simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Premises used: Nat.coprime_factorizationLCMLeft_factorizationLCMRight, Nat.factorizationLCMLeft_mul_factorizationLCMRight, Nat.factorizationLCMLeft_dvd_left, Nat.factorizationLCMRight_dvd_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
pos :
  ∀ (hx : orderOf x = 0),
    ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)
neg :
  ∀ (hx : ¬orderOf x = 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)

Tactic:
by_cases hx : orderOf x = 0

Premises used: orderOf
-- Module: Mathlib.GroupTheory.Exponent
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)
neg :
  ∀ (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)

Tactic:
by_cases hy : orderOf y = 0

Premises used: orderOf
-- Module: Mathlib.GroupTheory.Exponent
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)
neg :
  ∀ (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)

Tactic:
by_cases hy : orderOf y = 0

Premises used: orderOf
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ Membership.mem (γ := Set G) {x, y} x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ orderOf x = (orderOf x).lcm (orderOf y)

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
exact ⟨x, subset_closure (by simp), by simp [hx]⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ Membership.mem (γ := Set G) {x, y} x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ orderOf x = (orderOf x).lcm (orderOf y)

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
exact ⟨x, subset_closure (by simp), by simp [hx]⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ Membership.mem (γ := Set G) {x, y} y

Tactic:
simp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ orderOf y = (orderOf x).lcm (orderOf y)

Tactic:
simp [hy]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
exact ⟨y, subset_closure (by simp), by simp [hy]⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ Membership.mem (γ := Set G) {x, y} x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ Membership.mem (γ := Set G) {x, y} y

Tactic:
simp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ (z : G), Membership.mem (γ := Submonoid G) (closure {x, y}) z ∧ orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
exact ⟨_, mul_mem (pow_mem (subset_closure (by simp)) _) (pow_mem (subset_closure (by simp)) _),
      h.orderOf_mul_pow_eq_lcm hx hy⟩
-- Module: Mathlib.GroupTheory.Exponent
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

Tactic:
⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩

Premises used: dvd_antisymm, Iff.intro
-- Module: Mathlib.GroupTheory.Exponent
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
refine_3 : ∀ (h : ∀ (g : G), g ≠ 1 → orderOf g = p), p ∣ exponent G
⊢ exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p

Tactic:
refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩
-- Module: Mathlib.GroupTheory.Exponent
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 = 1

Tactic:
rw [Ne, ← orderOf_eq_one_iff] at hg

Premises used: Ne, orderOf_eq_one_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : ¬orderOf g = 1
⊢ orderOf g = p

Tactic:
Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g

Premises used: Monoid.order_dvd_exponent, Eq.rec, Nat.Prime.dvd_iff_eq, Iff.mp, Eq.symm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : ¬orderOf g = 1
⊢ orderOf g = p

Tactic:
exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g

Premises used: Nat.Prime.dvd_iff_eq, Iff.mp, Eq.symm
-- Module: Mathlib.GroupTheory.Exponent
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
refine_2 : ∀ (g : G), orderOf g ∣ p
⊢ exponent G ∣ p

Tactic:
rw [exponent_dvd]

Premises used: Monoid.exponent_dvd
-- Module: Mathlib.GroupTheory.Exponent
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
neg : ∀ (hg : ¬g = 1), orderOf g ∣ p
⊢ orderOf g ∣ p

Tactic:
by_cases hg : g = 1
-- Module: Mathlib.GroupTheory.Exponent
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

Tactic:
simp [hg]
-- Module: Mathlib.GroupTheory.Exponent
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
neg neg₁ : p ∣ p
⊢ orderOf g ∣ p

Tactic:
rw [h g hg]
-- Module: Mathlib.GroupTheory.Exponent
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
refine_3 : ∀ (g : G) (hg : g ≠ 1), p ∣ exponent G
⊢ p ∣ exponent G

Tactic:
obtain ⟨g, hg⟩ := exists_ne (1 : G)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Exponent
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
⊢ p ∣ exponent G

Tactic:
simpa [h g hg] using Monoid.order_dvd_exponent g

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite

Tactic:
⟨fun he => ?_, fun he => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Exponent
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
refine_2 : ∀ (he : (Set.range.{0, u + 1} (ι := G) orderOf).Finite), exponent G ≠ 0
⊢ exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite

Tactic:
refine ⟨fun he => ?_, fun he => ?_⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
refine_1 : ∀ (h : ¬(Set.range.{0, u + 1} (ι := G) orderOf).Finite), False
⊢ (Set.range.{0, u + 1} (ι := G) orderOf).Finite

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.Exponent
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
refine_1 : ∀ (t : G) (het : exponent G < orderOf t), False
⊢ False

Tactic:
obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)

Premises used: Set.Infinite.exists_gt, Monoid.exponent, rfl
-- Module: Mathlib.GroupTheory.Exponent
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
t : G
het : exponent G < orderOf t
⊢ False

Tactic:
pow_ne_one_of_lt_orderOf he het (pow_exponent_eq_one t)

Premises used: Monoid.pow_exponent_eq_one, pow_ne_one_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Exponent
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
t : G
het : exponent G < orderOf t
⊢ False

Tactic:
exact pow_ne_one_of_lt_orderOf he het (pow_exponent_eq_one t)

Premises used: Monoid.pow_exponent_eq_one, pow_ne_one_of_lt_orderOf
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
⊢ (Set.range.{0, u + 1} (ι := G) orderOf).Finite

Tactic:
he
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
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
⊢ exponent G ≠ 0

Tactic:
lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht

Premises used: Finset, orderOf, Nat, Set.range
-- Module: Mathlib.GroupTheory.Exponent
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

Tactic:
Finset.prod_pos fun a ha => ?_

Premises used: Finset.prod_pos
-- Module: Mathlib.GroupTheory.Exponent
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
refine : ∀ (a : ℕ) (ha : a ∈ t), 0 < id a
⊢ 0 < t.prod id

Tactic:
refine Finset.prod_pos fun a ha => ?_

Premises used: Finset.prod_pos
-- Module: Mathlib.GroupTheory.Exponent
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
⊢ a ∈ Set.range.{0, u + 1} (ι := G) orderOf

Tactic:
rw [← Finset.mem_coe, ht] at ha

Premises used: Finset.mem_coe
-- Module: Mathlib.GroupTheory.Exponent
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
obtain : ∀ (k : G), 0 < id (orderOf k)
⊢ 0 < id a

Tactic:
obtain ⟨k, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.GroupTheory.Exponent
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
k : G
⊢ 0 < id (orderOf k)

Tactic:
h k

Premises used: dite, orderOf, Function.minimalPeriod
-- Module: Mathlib.GroupTheory.Exponent
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
k : G
⊢ 0 < id (orderOf k)

Tactic:
exact h k
-- Module: Mathlib.GroupTheory.Exponent
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

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
-- Module: Mathlib.GroupTheory.Exponent
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
⊢ t.prod id = 0

Tactic:
rw [h, zero_dvd_iff] at this

Premises used: zero_dvd_iff
-- Module: Mathlib.GroupTheory.Exponent
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
this₁ : t.prod id = 0
⊢ exponent G = 0

Tactic:
rw [h, zero_dvd_iff] at this

Premises used: zero_dvd_iff
-- Module: Mathlib.GroupTheory.Exponent
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 : t.prod id = 0
h : exponent G = 0
⊢ False

Tactic:
htpos.ne' this

Premises used: LT.lt.ne'
-- Module: Mathlib.GroupTheory.Exponent
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 : t.prod id = 0
h : exponent G = 0
⊢ False

Tactic:
exact htpos.ne' this

Premises used: LT.lt.ne'
-- Module: Mathlib.GroupTheory.Exponent
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
refine_2 : exponent G ∣ t.prod id
⊢ exponent G ≠ 0

Tactic:
suffices exponent G ∣ t.prod id by
      intro h
      rw [h, zero_dvd_iff] at this
      exact htpos.ne' this
-- Module: Mathlib.GroupTheory.Exponent
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
refine_2 : ∀ (g : G), orderOf g ∣ t.prod id
⊢ exponent G ∣ t.prod id

Tactic:
rw [exponent_dvd]

Premises used: Monoid.exponent_dvd
-- Module: Mathlib.GroupTheory.Exponent
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
apply : orderOf g ∈ t
⊢ orderOf g ∣ t.prod id

Tactic:
apply Finset.dvd_prod_of_mem id (?_ : orderOf g ∈ _)

Premises used: Finset.dvd_prod_of_mem, id
-- Module: Mathlib.GroupTheory.Exponent
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
rw : orderOf g ∈ Set.range.{0, u + 1} (ι := G) orderOf
⊢ orderOf g ∈ t

Tactic:
rw [← Finset.mem_coe, ht]

Premises used: Finset.mem_coe
-- Module: Mathlib.GroupTheory.Exponent
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 ∈ Set.range.{0, u + 1} (ι := G) orderOf

Tactic:
Set.mem_range_self g

Premises used: Set.mem_range_self
-- Module: Mathlib.GroupTheory.Exponent
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 ∈ Set.range.{0, u + 1} (ι := G) orderOf

Tactic:
exact Set.mem_range_self g

Premises used: Set.mem_range_self
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ (Set.range.{0, u + 1} (ι := G) orderOf).Finite

Tactic:
have := exponent_ne_zero_iff_range_orderOf_finite h
-- Module: Mathlib.GroupTheory.Exponent
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
rwa₂ rwa₃ rwa₄ 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

Tactic:
rwa [Ne, not_iff_comm, Iff.comm] at this

Premises used: Ne, Iff.comm, not_iff_comm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : Fintype G
⊢ Finset.lcm.{0, u} (β := G) Finset.univ orderOf = exponent G

Tactic:
Nat.dvd_antisymm
    (lcm_orderOf_dvd_exponent G)
    (exponent_dvd.mpr fun g => Finset.dvd_lcm (Finset.mem_univ g))

Premises used: Iff.mpr, Finset.mem_univ, Monoid.exponent_dvd, Monoid.lcm_orderOf_dvd_exponent, Finset.dvd_lcm, Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.Exponent
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)
rw₂ rw₃ : Eq.{u_1 + 1} (α := H) 1 1
⊢ Eq.{u_1 + 1} (α := H) ((e : (a : G) → H) (g ^ exponent H) : H) ((e : (a : G) → H) 1 : H)

Tactic:
rw [map_pow, pow_exponent_eq_one, map_one]

Premises used: map_pow, map_one, Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
H : Submonoid G
⊢ exponent.{u} ↥H ∣ exponent G

Tactic:
Monoid.exponent_dvd_of_monoidHom H.subtype H.subtype_injective

Premises used: Submonoid.subtype_injective, Monoid.exponent_dvd_of_monoidHom, Submonoid.subtype