awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ IsOfFinAddOrder (G := Additive G) ((Additive.ofMul : (a : G) → Additive G) x : Additive G) ↔ IsOfFinOrder x

Tactic:
Iff.rfl

Premises used: Set.Mem, Additive, Iff.rfl, IsOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_6
inst : AddMonoid α
x : α
⊢ IsOfFinOrder (G := Multiplicative α) ((Multiplicative.ofAdd : (a : α) → Multiplicative α) x : Multiplicative α) ↔
    IsOfFinAddOrder x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, IsOfFinAddOrder, Multiplicative
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ IsOfFinOrder x ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Tactic:
simp [IsOfFinOrder, mem_periodicPts, isPeriodicPt_mul_iff_pow_eq_one]

Premises used: isPeriodicPt_mul_iff_pow_eq_one, IsOfFinOrder, Function.mem_periodicPts
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
rw : (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1
⊢ IsOfFinOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
⊢ (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1

Tactic:
⟨fun ⟨n, hn, hn'⟩ ↦ ⟨n, Int.natCast_ne_zero_iff_pos.mpr hn, zpow_natCast x n ▸ hn'⟩,
    fun ⟨n, hn, hn'⟩ ↦ ⟨n.natAbs, Int.natAbs_pos.mpr hn, ?_⟩⟩

Premises used: zpow_natCast, Iff.mpr, _private.0.isOfFinOrder_iff_zpow_eq_one.match_2, Int.natCast_ne_zero_iff_pos, Int.natAbs_pos, _private.0.isOfFinOrder_iff_zpow_eq_one.match_1, Exists, Eq.rec, Ne, Nat.cast, And, HPow.hPow, And.intro, LT.lt, Iff.intro, Int.natAbs, Exists.intro, OfNat.ofNat, Eq.symm, Eq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
refine : (∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1) → ∀ (n : ℤ) (hn : n ≠ 0) (hn' : x ^ n = 1), x ^ n.natAbs = 1
⊢ (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1

Tactic:
refine ⟨fun ⟨n, hn, hn'⟩ ↦ ⟨n, Int.natCast_ne_zero_iff_pos.mpr hn, zpow_natCast x n ▸ hn'⟩,
    fun ⟨n, hn, hn'⟩ ↦ ⟨n.natAbs, Int.natAbs_pos.mpr hn, ?_⟩⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
h : ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
inl : ∀ (h : n = (↑n.natAbs : ℤ)), x ^ n.natAbs = 1
inr : ∀ (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
⊢ x ^ n.natAbs = 1

Tactic:
rcases (Int.natAbs_eq_iff (a := n)).mp rfl with h | h

Premises used: Int.natAbs_eq_iff, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
h_1 : ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = (↑n.natAbs : ℤ)
inl : ∀ (hn' : HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ) = 1) (h : n = (↑n.natAbs : ℤ)), x ^ n.natAbs = 1
inl₁ inl₂ inl₃ inl₄ : ∀ (hn' : x ^ n.natAbs = 1) (h : n = (↑n.natAbs : ℤ)), x ^ n.natAbs = 1
⊢ x ^ n.natAbs = 1

Tactic:
rwa [h, zpow_natCast] at hn'

Premises used: zpow_natCast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
h_1 : ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -(↑n.natAbs : ℤ)
inr : ∀ (hn' : HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ)) = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
inr₁ : ∀ (hn' : (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ))⁻¹ = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
inr₂ : ∀ (hn' : HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ) = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
inr₃ inr₄ inr₅ inr₆ : ∀ (hn' : x ^ n.natAbs = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
⊢ x ^ n.natAbs = 1

Tactic:
rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'

Premises used: zpow_natCast, inv_eq_one, zpow_neg
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
simp_rw : ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1
⊢ ¬IsOfFinOrder x

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

Premises used: not_exists, not_and, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ x ^ n = HPow.hPow (β := ℕ) x 0

Tactic:
rw [← pow_zero x] at hnx

Premises used: pow_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = HPow.hPow (β := ℕ) x 0
⊢ LT.lt (α := ℕ) 0 0

Tactic:
rw [h hnx] at hn_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = HPow.hPow (β := ℕ) x 0
hn_pos₁ : LT.lt (α := ℕ) 0 0
⊢ x ^ n = HPow.hPow (β := ℕ) x 0

Tactic:
rw [h hnx] at hn_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
n : ℕ
hn_pos : LT.lt (α := ℕ) 0 0
hnx : x ^ n = HPow.hPow (β := ℕ) x 0
⊢ False

Tactic:
irrefl 0 hn_pos

Premises used: irrefl, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
n : ℕ
hn_pos : LT.lt (α := ℕ) 0 0
hnx : x ^ n = HPow.hPow (β := ℕ) x 0
⊢ False

Tactic:
exact irrefl 0 hn_pos

Premises used: irrefl, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
⊢ IsOfFinOrder.{u_1} (G := G) 1

Tactic:
isOfFinOrder_iff_pow_eq_one.mpr ⟨1, Nat.one_pos, one_pow 1⟩

Premises used: Iff.mpr, one_pow, Nat.one_pos, And.intro, Exists.intro, OfNat.ofNat, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
simp_rw : (∃ (n : ℕ), 0 < n ∧ a ^ n = 1) → ∃ (n_1 : ℕ), 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
⊢ IsOfFinOrder a → IsOfFinOrder (a ^ n)

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ (a ^ n) ^ m = 1

Tactic:
simp [pow_right_comm _ n, ha]

Premises used: pow_right_comm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ ∃ (n_1 : ℕ), 0 < n_1 ∧ (a ^ n) ^ n_1 = 1

Tactic:
exact ⟨m, hm, by simp [pow_right_comm _ n, ha]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
h : IsOfFinOrder (a ^ n)
hn : n ≠ 0
rw : ∀ (h : ∃ (n_1 : ℕ), 0 < n_1 ∧ (a ^ n) ^ n_1 = 1) (hn : n ≠ 0), ∃ (n : ℕ), 0 < n ∧ a ^ n = 1
⊢ IsOfFinOrder a

Tactic:
rw [isOfFinOrder_iff_pow_eq_one] at *

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
h : ∃ (n_1 : ℕ), 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
hn : n ≠ 0
rcases : ∀ (m : ℕ) (hm : 0 < m) (ha : (a ^ n) ^ m = 1), ∃ (n : ℕ), 0 < n ∧ a ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ a ^ n = 1

Tactic:
rcases h with ⟨m, hm, ha⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
hn : n ≠ 0
m : ℕ
hm : 0 < m
ha rwa rwa₁ rwa₂ rwa₃ : (a ^ n) ^ m = 1
⊢ a ^ (n * m) = 1

Tactic:
rwa [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
hn : n ≠ 0
m : ℕ
hm : 0 < m
ha : (a ^ n) ^ m = 1
⊢ ∃ (n : ℕ), 0 < n ∧ a ^ n = 1

Tactic:
exact ⟨n * m, mul_pos hn.bot_lt hm, by rwa [pow_mul]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
inl : IsOfFinOrder (HPow.hPow (β := ℕ) a 0) ↔ IsOfFinOrder a ∨ Eq (α := ℕ) 0 0
inr : ∀ (hn : n ≠ 0), IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
rcases Decidable.eq_or_ne n 0 with rfl | hn

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
⊢ IsOfFinOrder (HPow.hPow (β := ℕ) a 0) ↔ IsOfFinOrder a ∨ Eq (α := ℕ) 0 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
hn : n ≠ 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩

Premises used: IsOfFinOrder.pow, Iff.intro, IsOfFinOrder.of_pow, Or.inl, Or.resolve_right
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
hn : n ≠ 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
inst_1 : IsMulTorsionFree G
ha : a ≠ 1
rw : ¬∃ (n : ℕ), 0 < n ∧ a ^ n = 1
⊢ ¬IsOfFinOrder a

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
inst_1 : IsMulTorsionFree G
ha : a ≠ 1
n : ℕ
hn : 0 < n
han : a ^ n = 1
⊢ Eq.{u_1 + 1} (α := G) ((fun (a : G) ↦ a ^ n) a) ((fun (a : G) ↦ a ^ n) 1)

Tactic:
simpa using han
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
inst_1 : IsMulTorsionFree G
ha : a ≠ 1
n : ℕ
hn : 0 < n
han : a ^ n = 1
⊢ False

Tactic:
exact ha <| pow_left_injective hn.ne' <| by simpa using han

Premises used: LT.lt.ne', Nat.pow_left_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : IsMulTorsionFree G
a : G
ha : IsOfFinOrder a
contrapose! : ∀ (ha : a ≠ 1), ¬IsOfFinOrder a
⊢ a = 1

Tactic:
contrapose! ha
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : IsMulTorsionFree G
a : G
ha : a ≠ 1
⊢ ¬IsOfFinOrder a

Tactic:
apply not_isOfFinOrder_of_isMulTorsionFree ha

Premises used: not_isOfFinOrder_of_isMulTorsionFree
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : IsMulTorsionFree G
a : G
⊢ IsOfFinOrder a ↔ a = 1

Tactic:
⟨IsOfFinOrder.eq_one', fun h => h.symm ▸ IsOfFinOrder.one⟩

Premises used: Eq.rec, IsOfFinOrder.eq_one', Iff.intro, Eq.symm, IsOfFinOrder.one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Submonoid G
x : ↥H
rw : (∃ (n : ℕ), 0 < n ∧ (↑x : G) ^ n = 1) ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
⊢ IsOfFinOrder (↑x : G) ↔ IsOfFinOrder x

Tactic:
rw [isOfFinOrder_iff_pow_eq_one, isOfFinOrder_iff_pow_eq_one]

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Submonoid G
x : ↥H
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
⊢ (∃ (n : ℕ), 0 < n ∧ (↑x : G) ^ n = 1) ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : IsConj x y
simp_rw : (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) → ∃ (n : ℕ), 0 < n ∧ y ^ n = 1
⊢ IsOfFinOrder x → IsOfFinOrder y

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
rw : IsConj (x ^ n) (y ^ n)
⊢ y ^ n = 1

Tactic:
rw [← isConj_one_right, ← eq']

Premises used: isConj_one_right
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj (x ^ n) (y ^ n)

Tactic:
h.pow n

Premises used: IsConj.pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj (x ^ n) (y ^ n)

Tactic:
exact h.pow n

Premises used: IsConj.pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ y ^ n = 1

Tactic:
exact ⟨n, n_gt_0, by rw [← isConj_one_right, ← eq']; exact h.pow n⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
inst_1 : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
obtain :
  ∀ (n : ℕ) (npos : 0 < n) (hn : x ^ n = 1), ∃ (n : ℕ), 0 < n ∧ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1

Tactic:
obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one

Premises used: IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
inst_1 : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
rw : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) (1 : H)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) 1 : H) (1 : H)
rw₂ rw₃ : Eq.{u_2 + 1} (α := H) 1 1
⊢ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1

Tactic:
rw [← f.map_pow, hn, f.map_one]

Premises used: MonoidHom.map_one, MonoidHom.map_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
inst_1 : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1

Tactic:
exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
η : Type u_6
Gs : η → Type u_7
inst : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
obtain : ∀ (n : ℕ) (npos : 0 < n) (hn : x ^ n = 1) (i : η), IsOfFinOrder (x i)
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one

Premises used: IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
η : Type u_6
Gs : η → Type u_7
inst : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩

Premises used: Iff.mpr, And.intro, Exists.intro, congr_fun, Eq.symm, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
η : Type u_6
Gs : η → Type u_7
inst : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
exact fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩

Premises used: Iff.mpr, And.intro, Exists.intro, congr_fun, Eq.symm, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid G
a b x y : G
n m : ℕ
hx : IsOfFinOrder x
⊢ 0 < ⋯.choose (p := fun (n : ℕ) ↦ 0 < n ∧ x ^ n = 1)

Tactic:
obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec

Premises used: Exists.choose_spec, IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid G
a b x y : G
n m : ℕ
hx : IsOfFinOrder x
hpos : 0 < ⋯.choose (p := fun (n : ℕ) ↦ 0 < n ∧ x ^ n = 1)
⊢ x ^ ⋯.choose (p := fun (n : ℕ) ↦ 0 < n ∧ x ^ n = 1) = 1

Tactic:
obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec

Premises used: Exists.choose_spec, IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid G
a b x y : G
n m : ℕ
hx_1 : IsOfFinOrder x
hpos : 0 < ⋯.choose (p := fun (n : ℕ) ↦ 0 < n ∧ x ^ n = 1)
hx : x ^ ⋯.choose (p := fun (n : ℕ) ↦ 0 < n ∧ x ^ n = 1) = 1
⊢ Group ↥(powers x)

Tactic:
exact Submonoid.groupPowers hpos hx

Premises used: Submonoid.groupPowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Subsingleton G
x : G
⊢ orderOf x = 1

Tactic:
simp [orderOf, nontriviality]

Premises used: orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ addOrderOf (G := Additive G) ((Additive.ofMul : (a : G) → Additive G) x : Additive G) = orderOf x

Tactic:
rfl

Premises used: Additive, orderOf, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_6
inst : AddMonoid α
a : α
⊢ orderOf (G := Multiplicative α) ((Multiplicative.ofAdd : (a : α) → Multiplicative α) a : Multiplicative α) =
    addOrderOf a

Tactic:
rfl

Premises used: addOrderOf, Multiplicative, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : IsOfFinOrder x
⊢ 0 < orderOf x

Tactic:
minimalPeriod_pos_of_mem_periodicPts h

Premises used: Function.minimalPeriod_pos_of_mem_periodicPts, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ x ^ orderOf x = 1

Tactic:
Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)

Premises used: Function.isPeriodicPt_minimalPeriod, HMul.hMul, OfNat.ofNat, Eq.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
convert_2 : x ^ orderOf x = (fun (x_1 : G) ↦ x * x_1)^[minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1] 1
⊢ x ^ orderOf x = 1

Tactic:
convert! Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)

Premises used: Function.isPeriodicPt_minimalPeriod, HMul.hMul, OfNat.ofNat, Eq.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
convert_2 :
  x ^ minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 =
    (fun (x_1 : G) ↦ x * x_1)^[minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1] 1
convert_2₁ convert_2₂ : x ^ minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = x ^ minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1
⊢ x ^ orderOf x = (fun (x_1 : G) ↦ x * x_1)^[minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1] 1

Tactic:
rw [orderOf, mul_left_iterate_apply_one]

Premises used: orderOf, mul_left_iterate_apply_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
h : ¬IsOfFinOrder x
rwa : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 0
rwa₁ :
  Eq (α := ℕ)
    (if h : Membership.mem (γ := Set G) (periodicPts fun (x_1 : G) ↦ x * x_1) 1 then
      Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) h
    else 0)
    0
rwa₂ : Eq (α := ℕ) 0 0
hnc : 1 ∉ periodicPts fun (x_1 : G) ↦ x * x_1
rwa₃ : Eq (α := ℕ) 0 0
hnc₁ hnc₂ hnc₃ : 1 ∉ periodicPts fun (x_1 : G) ↦ x * x_1
⊢ orderOf x = 0

Tactic:
rwa [orderOf, minimalPeriod, dif_neg]

Premises used: dif_neg, orderOf, Function.minimalPeriod
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ orderOf x = 0 ↔ ¬IsOfFinOrder x

Tactic:
⟨fun h H ↦ H.orderOf_pos.ne' h, orderOf_eq_zero⟩

Premises used: IsOfFinOrder.orderOf_pos, LT.lt.ne', Iff.intro, orderOf_eq_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
simp_rw : ¬IsOfFinOrder x ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
simp_rw₁ : (¬∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
simp_rw₂ : (∀ (x_1 : ℕ), ¬(0 < x_1 ∧ x ^ x_1 = 1)) ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

Premises used: not_exists, orderOf_eq_zero_iff, not_and, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ orderOf x ≠ 0 ↔ IsOfFinOrder x

Tactic:
orderOf_eq_zero_iff.not_left

Premises used: orderOf_eq_zero_iff, Iff.not_left
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
M₀ : Type u_6
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
rw : ¬∃ (n : ℕ), 0 < n ∧ HPow.hPow (α := M₀) 0 n = 1
⊢ orderOf.{u_6} (G := M₀) 0 = 0

Tactic:
rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one]

Premises used: orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
M₀ : Type u_6
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
⊢ ¬∃ (n : ℕ), 0 < n ∧ HPow.hPow (α := M₀) 0 n = 1

Tactic:
simp +contextual [ne_of_gt]

Premises used: Nat.ne_of_gt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
simp_rw :
  (if h : Membership.mem (γ := Set G) (periodicPts fun (x_1 : G) ↦ x * x_1) 1 then
        Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) h
      else 0) =
      n ↔
    IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1

Tactic:
simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]

Premises used: Ne, orderOf, isPeriodicPt_mul_iff_pow_eq_one, Function.minimalPeriod
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
pos :
  ∀ (h1 : Membership.mem (γ := Set G) (periodicPts fun (x_1 : G) ↦ x * x_1) 1),
    Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) h1 = n ↔
      IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1
neg :
  ∀ (h1 : 1 ∉ periodicPts fun (x_1 : G) ↦ x * x_1),
    0 = n ↔ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1
⊢ (if h : Membership.mem (γ := Set G) (periodicPts fun (x_1 : G) ↦ x * x_1) 1 then
        Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) h
      else 0) =
      n ↔
    IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1

Tactic:
split_ifs with h1
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : Membership.mem (γ := Set G) (periodicPts fun (x_1 : G) ↦ x * x_1) 1
pos :
  ((n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) ∧
      ∀ n_1 < n, ¬(n_1 > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1
⊢ Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) h1 = n ↔
    IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1

Tactic:
rw [find_eq_iff]

Premises used: Nat.find_eq_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : Membership.mem (γ := Set G) (periodicPts fun (x_1 : G) ↦ x * x_1) 1
⊢ ((n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) ∧
      ∀ n_1 < n, ¬(n_1 > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1

Tactic:
simp only [h, true_and, not_and]

Premises used: not_and, true_and
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : Membership.mem (γ := Set G) (periodicPts fun (x_1 : G) ↦ x * x_1) 1
pos pos₁ pos₂ :
  ((n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) ∧
      ∀ n_1 < n, ¬(n_1 > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1
⊢ Nat.find (p := fun (n : ℕ) ↦ n > 0 ∧ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1) h1 = n ↔
    IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1

Tactic:
classical
    rw [find_eq_iff]
    simp only [h, true_and, not_and]

Premises used: not_and, Nat.find_eq_iff, true_and
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun (x_1 : G) ↦ x * x_1
neg : ¬(IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1)
⊢ 0 = n ↔ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) m 1

Tactic:
rw [iff_false_left h.ne]

Premises used: iff_false_left, LT.lt.ne
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun (x_1 : G) ↦ x * x_1
h' : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1
⊢ False

Tactic:
h1 ⟨n, h, h'⟩

Premises used: And.intro, Exists.intro