awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
have : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
have₁ : ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0), minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have₂ : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0
have₃ have₄ : ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0), minOrder (ZMod n) = (↑n.minFac : ℕ∞)
refine_1 :
  ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0),
    LE.le (α := ℕ∞) (↑(Nat.card ↥(zmultiples (↑(n / n.minFac) : ZMod n))) : ℕ∞) (↑n.minFac : ℕ∞)
⊢ minOrder (ZMod n) = (↑n.minFac : ℕ∞)
have refine_2 : ∀ (this : Ne (α := ZMod n) (↑(n / n.minFac) : ZMod n) 0) (s : AddSubgroup (ZMod n)) (hs : s ≠ ⊥),
  (↑s : Set (ZMod n)).Finite → LE.le (α := ℕ∞) (↑n.minFac : ℕ∞) (↑(Nat.card ↥s) : ℕ∞)
Tactic: classical
  have : (↑(n / n.minFac) : ZMod n) ≠ 0 := by
    rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]
    exact
      not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
        (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)
  refine ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
    le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_
  · rw [Nat.card_zmultiples, ZMod.addOrderOf_coe _ hn,
      gcd_eq_right (div_dvd_of_dvd n.minFac_dvd), Nat.div_div_self n.minFac_dvd hn]
  · haveI : Nontrivial s := s.bot_or_nontrivial.resolve_left hs
    exact WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <|
      (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
p : ℕ
hp : Nat.Prime p
⊢ minOrder (ZMod p) = (↑p : ℕ∞)
have rw : Eq (α := ℕ∞) (↑p.minFac : ℕ∞) (↑p : ℕ∞)
Tactic: rw [ZMod.minOrder hp.ne_zero hp.ne_one, hp.minFac_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Order.Min (goal)
Goal:
p : ℕ
hp : Nat.Prime p
rw : Eq (α := ℕ∞) (↑p.minFac : ℕ∞) (↑p : ℕ∞)
⊢ minOrder (ZMod p) = (↑p : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑p : ℕ∞) (↑p : ℕ∞)
Tactic: rw [ZMod.minOrder hp.ne_zero hp.ne_one, hp.minFac_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
x : G
⊢ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ↔ x ^ n = 1
have rw : IsFixedPt.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1 ↔ x ^ n = 1
Tactic: rw [IsPeriodicPt, IsFixedPt, mul_left_iterate_apply_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
x : G
rw : IsFixedPt.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1 ↔ x ^ n = 1
⊢ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ↔ x ^ n = 1
have rw₁ : Eq.{u_1 + 1} (α := G) ((fun (x_1 : G) ↦ x * x_1)^[n] 1) 1 ↔ x ^ n = 1
Tactic: rw [IsPeriodicPt, IsFixedPt, mul_left_iterate_apply_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
x : G
rw : IsFixedPt.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1 ↔ x ^ n = 1
rw₁ : Eq.{u_1 + 1} (α := G) ((fun (x_1 : G) ↦ x * x_1)^[n] 1) 1 ↔ x ^ n = 1
⊢ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ↔ x ^ n = 1
have rw₂ : x ^ n = 1 ↔ x ^ n = 1
Tactic: rw [IsPeriodicPt, IsFixedPt, mul_left_iterate_apply_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
⊢ IsOfFinOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1
have rw : (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1
Tactic: rw [isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : DivisionMonoid G
x : G
⊢ (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1
have refine : (∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1) → ∀ (n : ℤ) (hn : n ≠ 0) (hn' : x ^ n = 1), x ^ n.natAbs = 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, ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n.natAbs = 1
have inl : ∀ (h : n = (↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rcases (Int.natAbs_eq_iff (a := n)).mp rfl with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n.natAbs = 1
have inr : ∀ (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rcases (Int.natAbs_eq_iff (a := n)).mp rfl with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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 : ℤ)
⊢ x ^ n.natAbs = 1
have inl : ∀ (hn' : HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ) = 1) (h : n = (↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rwa [h, zpow_natCast] at hn'
Cleared hypotheses: hn', h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n.natAbs = 1
have inl₁ : ∀ (hn' : x ^ n.natAbs = 1) (h : n = (↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rwa [h, zpow_natCast] at hn'
Cleared hypotheses: hn', h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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 : ℤ)
⊢ x ^ n.natAbs = 1
have inr : ∀ (hn' : HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ)) = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'
Cleared hypotheses: hn', h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n.natAbs = 1
have inr₁ : ∀ (hn' : (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ))⁻¹ = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'
Cleared hypotheses: hn', h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n.natAbs = 1
have inr₂ : ∀ (hn' : HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ) = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'
Cleared hypotheses: hn', h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n.natAbs = 1
have inr₃ : ∀ (hn' : x ^ n.natAbs = 1) (h : n = -(↑n.natAbs : ℤ)), x ^ n.natAbs = 1
Tactic: rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'
Cleared hypotheses: hn', h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
⊢ ¬IsOfFinOrder x
have simp_rw : ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1
Tactic: simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ False
have hnx₁ : x ^ n = HPow.hPow (β := ℕ) x 0
Tactic: rw [← pow_zero x] at hnx
Cleared hypotheses: hnx
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ False
have hn_pos₁ : LT.lt (α := ℕ) 0 0
Tactic: rw [h hnx] at hn_pos
Cleared hypotheses: hn_pos, hnx
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
⊢ IsOfFinOrder a → IsOfFinOrder (a ^ n)
have simp_rw : (∃ (n : ℕ), 0 < n ∧ a ^ n = 1) → ∃ (n_1 : ℕ), 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
Tactic: simp_rw [isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
h : IsOfFinOrder (a ^ n)
hn : n ≠ 0
⊢ IsOfFinOrder a
have rw : ∀ (h : ∃ (n_1 : ℕ), 0 < n_1 ∧ (a ^ n) ^ n_1 = 1) (hn : n ≠ 0), ∃ (n : ℕ), 0 < n ∧ a ^ n = 1
Tactic: rw [isOfFinOrder_iff_pow_eq_one] at *
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ ∃ (n : ℕ), 0 < n ∧ a ^ n = 1
have rcases : ∀ (m : ℕ) (hm : 0 < m) (ha : (a ^ n) ^ m = 1), ∃ (n : ℕ), 0 < n ∧ a ^ n = 1
Tactic: rcases h with ⟨m, hm, ha⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0
have inl : IsOfFinOrder (HPow.hPow (β := ℕ) a 0) ↔ IsOfFinOrder a ∨ Eq (α := ℕ) 0 0
Tactic: rcases Decidable.eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
a : G
n : ℕ
inl : IsOfFinOrder (HPow.hPow (β := ℕ) a 0) ↔ IsOfFinOrder a ∨ Eq (α := ℕ) 0 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0
have inr : ∀ (hn : n ≠ 0), IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0
Tactic: rcases Decidable.eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
a : G
inst_1 : IsMulTorsionFree G
ha : a ≠ 1
⊢ ¬IsOfFinOrder a
have rw : ¬∃ (n : ℕ), 0 < n ∧ a ^ n = 1
Tactic: rw [isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : IsMulTorsionFree G
a : G
ha : IsOfFinOrder a
⊢ a = 1
have contrapose! : ∀ (ha : a ≠ 1), ¬IsOfFinOrder a
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Submonoid G
x : ↥H
⊢ IsOfFinOrder (↑x : G) ↔ IsOfFinOrder x
have rw : (∃ (n : ℕ), 0 < n ∧ (↑x : G) ^ n = 1) ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: rw [isOfFinOrder_iff_pow_eq_one, isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
H : Submonoid G
x : ↥H
⊢ (∃ (n : ℕ), 0 < n ∧ (↑x : G) ^ n = 1) ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
have norm_cast : (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : IsConj x y
⊢ IsOfFinOrder x → IsOfFinOrder y
have simp_rw : (∃ (n : ℕ), 0 < n ∧ x ^ n = 1) → ∃ (n : ℕ), 0 < n ∧ y ^ n = 1
Tactic: simp_rw [isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ y ^ n = 1
have rw : IsConj (x ^ n) (y ^ n)
Tactic: rw [← isConj_one_right, ← eq']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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 : ℕ), 0 < n ∧ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1
have obtain : ∀ (n : ℕ) (npos : 0 < n) (hn : x ^ 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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1
have rw : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) (1 : H)
Tactic: rw [← f.map_pow, hn, f.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1
have rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) 1 : H) (1 : H)
Tactic: rw [← f.map_pow, hn, f.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1
have rw₂ : Eq.{u_2 + 1} (α := H) 1 1
Tactic: rw [← f.map_pow, hn, f.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
η : Type u_6
Gs : η → Type u_7
inst : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
⊢ ∀ (i : η), IsOfFinOrder (x i)
have obtain : ∀ (n : ℕ) (npos : 0 < n) (hn : x ^ n = 1) (i : η), IsOfFinOrder (x i)
Tactic: obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ Group ↥(powers x)
have hpos : 0 < sorry.choose (p := fun (n : ℕ) ↦ 0 < n ∧ x ^ n = 1)
Tactic: obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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)
⊢ Group ↥(powers x)
have hx₁ : x ^ sorry.choose (p := fun (n : ℕ) ↦ 0 < n ∧ x ^ n = 1) = 1
Tactic: obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ x ^ orderOf x = 1
have convert_2 : x ^ orderOf x = (fun (x_1 : G) ↦ x * x_1)^[minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1] 1
Tactic: convert! Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ x ^ orderOf x = (fun (x_1 : G) ↦ x * x_1)^[minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1] 1
have 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
Tactic: rw [orderOf, mul_left_iterate_apply_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ orderOf x = (fun (x_1 : G) ↦ x * x_1)^[minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1] 1
have convert_2₁ : x ^ minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = x ^ minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1
Tactic: rw [orderOf, mul_left_iterate_apply_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ orderOf x = 0
have rwa : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 0
Tactic: rwa [orderOf, minimalPeriod, dif_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
h : ¬IsOfFinOrder x
rwa : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 0
⊢ orderOf x = 0
have 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
Tactic: rwa [orderOf, minimalPeriod, dif_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ orderOf x = 0
have rwa₂ : Eq (α := ℕ) 0 0
Tactic: rwa [orderOf, minimalPeriod, dif_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ orderOf x = 0
have hnc : 1 ∉ periodicPts fun (x_1 : G) ↦ x * x_1
Tactic: rwa [orderOf, minimalPeriod, dif_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
have simp_rw : ¬IsOfFinOrder x ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Tactic: simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
simp_rw : ¬IsOfFinOrder x ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
have simp_rw₁ : (¬∃ (n : ℕ), 0 < n ∧ x ^ n = 1) ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Tactic: simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
have simp_rw₂ : (∀ (x_1 : ℕ), ¬(0 < x_1 ∧ x ^ x_1 = 1)) ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Tactic: simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
M₀ : Type u_6
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
⊢ orderOf.{u_6} (G := M₀) 0 = 0
have rw : ¬∃ (n : ℕ), 0 < n ∧ HPow.hPow (α := M₀) 0 n = 1
Tactic: rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1
have 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
Tactic: simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ (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
have 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
Tactic: split_ifs with h1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ 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
have 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
Tactic: rw [find_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ 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
have 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
Tactic: classical
    rw [find_eq_iff]
    simp only [h, true_and, not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
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
have 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)
Tactic: rw [iff_false_left h.ne]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ 0 < orderOf x ↔ IsOfFinOrder x
have rw : 0 < orderOf x ↔ ¬orderOf x = 0
Tactic: rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
rw : 0 < orderOf x ↔ ¬orderOf x = 0
⊢ 0 < orderOf x ↔ IsOfFinOrder x
have rw₁ : orderOf x ≠ 0 ↔ ¬orderOf x = 0
Tactic: rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
β : Type u_5
inst : Monoid G
x : G
inst_1 : Monoid β
y : β
hx : IsOfFinOrder x
h : orderOf y ∣ orderOf x
⊢ IsOfFinOrder y
have rw : ∀ (hx : 0 < orderOf x) (h : orderOf y ∣ orderOf x), 0 < orderOf y
Tactic: rw [← orderOf_pos_iff] at hx ⊢
Cleared hypotheses: hx, h