awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Group G_1
x_1 y : G_1
inst_1 : Fintype G_1
x : G_1
n : ℕ
G : Type u_6
inst_2 : Group G
h : (Nat.card G).Coprime n
g : G
key :
  HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
    g ^ ((↑(Nat.card G) : ℤ) * (Nat.card G).gcdA n + (↑n : ℤ) * (Nat.card G).gcdB n)
rwa :
  ∀
    (key :
      HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
        g ^ ((↑(Nat.card G) : ℤ) * (Nat.card G).gcdA n) * g ^ ((↑n : ℤ) * (Nat.card G).gcdB n)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₁ :
  ∀
    (key :
      HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
        HPow.hPow (β := ℤ) g (↑(Nat.card G) : ℤ) ^ (Nat.card G).gcdA n * g ^ ((↑n : ℤ) * (Nat.card G).gcdB n)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₂ :
  ∀
    (key :
      HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
        HPow.hPow (β := ℤ) g (↑(Nat.card G) : ℤ) ^ (Nat.card G).gcdA n *
          HPow.hPow (β := ℤ) (g ^ (Nat.card G).gcdB n) (↑n : ℤ)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₃ :
  ∀
    (key :
      g ^ (Nat.card G).gcd n =
        HPow.hPow (β := ℤ) g (↑(Nat.card G) : ℤ) ^ (Nat.card G).gcdA n *
          HPow.hPow (β := ℤ) (g ^ (Nat.card G).gcdB n) (↑n : ℤ)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₄ :
  ∀
    (key :
      g ^ (Nat.card G).gcd n =
        (g ^ Nat.card G) ^ (Nat.card G).gcdA n * HPow.hPow (β := ℤ) (g ^ (Nat.card G).gcdB n) (↑n : ℤ)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₅ :
  ∀ (key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₆ :
  ∀ (key : HPow.hPow (β := ℕ) g 1 = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₇ :
  ∀ (key : g = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₈ :
  ∀ (key : g = HPow.hPow (α := G) 1 ((Nat.card G).gcdA n) * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₉ :
  ∀ (key : g = 1 * (g ^ (Nat.card G).gcdB n) ^ n), (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
⊢ (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
have rwa₁₀ : ∀ (key : g = (g ^ (Nat.card G).gcdB n) ^ n), (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
Tactic: rwa [zpow_add, zpow_mul, zpow_mul', zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one,
      pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Group G_1
x_1 y : G_1
inst_1 : Fintype G_1
x : G_1
n : ℕ
G : Type u_6
inst_2 : Group G
h : (Nat.card G).Coprime n
g : G
key :
  HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
    g ^ ((↑(Nat.card G) : ℤ) * (Nat.card G).gcdA n + (↑n : ℤ) * (Nat.card G).gcdB n)
rwa :
  ∀
    (key :
      HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
        g ^ ((↑(Nat.card G) : ℤ) * (Nat.card G).gcdA n) * g ^ ((↑n : ℤ) * (Nat.card G).gcdB n)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₁ :
  ∀
    (key :
      HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
        HPow.hPow (β := ℤ) g (↑(Nat.card G) : ℤ) ^ (Nat.card G).gcdA n * g ^ ((↑n : ℤ) * (Nat.card G).gcdB n)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₂ :
  ∀
    (key :
      HPow.hPow (β := ℤ) g (↑((Nat.card G).gcd n) : ℤ) =
        HPow.hPow (β := ℤ) g (↑(Nat.card G) : ℤ) ^ (Nat.card G).gcdA n *
          HPow.hPow (β := ℤ) (g ^ (Nat.card G).gcdB n) (↑n : ℤ)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₃ :
  ∀
    (key :
      g ^ (Nat.card G).gcd n =
        HPow.hPow (β := ℤ) g (↑(Nat.card G) : ℤ) ^ (Nat.card G).gcdA n *
          HPow.hPow (β := ℤ) (g ^ (Nat.card G).gcdB n) (↑n : ℤ)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₄ :
  ∀
    (key :
      g ^ (Nat.card G).gcd n =
        (g ^ Nat.card G) ^ (Nat.card G).gcdA n * HPow.hPow (β := ℤ) (g ^ (Nat.card G).gcdB n) (↑n : ℤ)),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₅ :
  ∀ (key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₆ :
  ∀ (key : HPow.hPow (β := ℕ) g 1 = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₇ :
  ∀ (key : g = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₈ :
  ∀ (key : g = HPow.hPow (α := G) 1 ((Nat.card G).gcdA n) * (g ^ (Nat.card G).gcdB n) ^ n),
    (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₉ :
  ∀ (key : g = 1 * (g ^ (Nat.card G).gcdB n) ^ n), (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
rwa₁₀ :
  ∀ (key : g = (g ^ (Nat.card G).gcdB n) ^ n), (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
⊢ (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
have rwa₁₁ : ∀ (key : (g ^ (Nat.card G).gcdB n) ^ n = g), (fun (g : G) ↦ g ^ n) ((fun (g : G) ↦ g ^ (Nat.card G).gcdB n) g) = g
Tactic: rwa [zpow_add, zpow_mul, zpow_mul', zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one,
      pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
inst_2 : DecidableEq G
this : Fintype ↥(zpowers x) := instFintypeSubtypeMemOfDecidablePred (zpowers x)
⊢ Finset.image (fun (i : ℕ) ↦ x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x) : Set G).toFinset
have h : ∀ (x_1 : G),
  Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x ^ i) (Finset.range (orderOf x))) x_1 ↔
    x_1 ∈ (↑(zpowers x) : Set G).toFinset
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x_1 : G
inst_2 : DecidableEq G
this : Fintype ↥(zpowers x_1) := instFintypeSubtypeMemOfDecidablePred (zpowers x_1)
x : G
⊢ Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
    x ∈ (↑(zpowers x_1) : Set G).toFinset
have h : Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
  x ∈ (↑(zpowers x_1) : Set G)
Tactic: rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x_1 : G
inst_2 : DecidableEq G
this : Fintype ↥(zpowers x_1) := instFintypeSubtypeMemOfDecidablePred (zpowers x_1)
x : G
h :
  Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
    x ∈ (↑(zpowers x_1) : Set G)
⊢ Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
    x ∈ (↑(zpowers x_1) : Set G).toFinset
have h₁ : Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
  Membership.mem (γ := Subgroup G) (zpowers x_1) x
Tactic: rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x_1 : G
inst_2 : DecidableEq G
this : Fintype ↥(zpowers x_1) := instFintypeSubtypeMemOfDecidablePred (zpowers x_1)
x : G
h :
  Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
    x ∈ (↑(zpowers x_1) : Set G)
h₁ :
  Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
    Membership.mem (γ := Subgroup G) (zpowers x_1) x
⊢ Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
    x ∈ (↑(zpowers x_1) : Set G).toFinset
have h₂ : Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
  Membership.mem (γ := Finset G) (Finset.image (fun (x : ℕ) ↦ x_1 ^ x) (Finset.range (orderOf x_1))) x
Tactic: rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_6
inst : Group G
inst_1 : Finite G
α : Type u_7
inst_2 : PartialOrder α
g : G
a : α
inst_3 : MulAction G α
inst_4 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ g • a = a
have key : g • a ≤ g • g ^ (Nat.card G - 1) • a
Tactic: have key := smul_mono_right g (le_pow_smul h (Nat.card G - 1))
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_6
inst : Group G
inst_1 : Finite G
α : Type u_7
inst_2 : PartialOrder α
g : G
a : α
inst_3 : MulAction G α
inst_4 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ g • g ^ (Nat.card G - 1) • a
⊢ g • a = a
have key₁ : g • a ≤ a
Tactic: rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_6
inst : Group G
inst_1 : Finite G
α : Type u_7
inst_2 : PartialOrder α
g : G
a : α
inst_3 : MulAction G α
inst_4 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g • a = a
have key : g • g ^ (Nat.card G - 1) • a ≤ g • a
Tactic: have key := smul_mono_right g (pow_smul_le h (Nat.card G - 1))
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_6
inst : Group G
inst_1 : Finite G
α : Type u_7
inst_2 : PartialOrder α
g : G
a : α
inst_3 : MulAction G α
inst_4 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : g • g ^ (Nat.card G - 1) • a ≤ g • a
⊢ g • a = a
have key₁ : a ≤ g • a
Tactic: rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst : LeftCancelMonoid M
inst_1 : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
ih : a ^ (n + 1) ∈ S
⊢ a ^ (n + 1 + 1) ∈ S
have succ : a ^ (n + 1) * a ∈ S * S
Tactic: rw [← hS2, pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst : LeftCancelMonoid M
inst_1 : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
⊢ a ^ (n + 1) ∈ S
have zero : a ^ HAdd.hAdd (α := ℕ) 0 1 ∈ S
Tactic: induction n with
    | zero => rwa [zero_add, pow_one]
    | succ n ih =>
      rw [← hS2, pow_succ]
      exact Set.mul_mem_mul ih ha
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst : LeftCancelMonoid M
inst_1 : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
zero : a ^ HAdd.hAdd (α := ℕ) 0 1 ∈ S
⊢ a ^ (n + 1) ∈ S
have succ : ∀ (n : ℕ) (ih : a ^ (n + 1) ∈ S), a ^ (n + 1 + 1) ∈ S
Tactic: induction n with
    | zero => rwa [zero_add, pow_one]
    | succ n ih =>
      rw [← hS2, pow_succ]
      exact Set.mul_mem_mul ih ha
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst : LeftCancelMonoid M
inst_1 : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
pow_mem : ∀ (a : M) (ha : a ∈ S) (n : ℕ), a ^ (n + 1) ∈ S
⊢ 1 ∈ S
have obtain : ∀ (a : M) (ha : a ∈ S), 1 ∈ S
Tactic: obtain ⟨a, ha⟩ := hS1
Cleared hypotheses: hS1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst : LeftCancelMonoid M
inst_1 : Finite M
S : Set M
hS2 : S * S = S
pow_mem : ∀ (a : M) (ha : a ∈ S) (n : ℕ), a ^ (n + 1) ∈ S
a : M
ha : a ∈ S
⊢ 1 ∈ S
have rw : a ^ (orderOf a - succ 0 + succ 0) ∈ S
Tactic: rw [← pow_orderOf_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (orderOf_pos a))]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst : Group G
inst_1 : Finite G
S : Set G
hS1 : S.Nonempty
hS2 : S * S = S
a : G
ha : a ∈ S
⊢ Membership.mem (γ := Submonoid G) (submonoidOfIdempotent S hS1 hS2) a⁻¹
have rw : Membership.mem (γ := Submonoid G) (submonoidOfIdempotent S hS1 hS2) (a ^ (orderOf a - succ 0))
Tactic: rw [← one_mul a⁻¹, ← pow_one a, ← pow_orderOf_eq_one a, ← pow_sub a (orderOf_pos a)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst : Group G
inst_1 : Fintype G
S : Set G
hS : S.Nonempty
⊢ 1 ∈ S ^ card G
have obtain : ∀ (a : G) (ha : a ∈ S), 1 ∈ S ^ card G
Tactic: obtain ⟨a, ha⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst : Group G
inst_1 : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ 1 ∈ S ^ card G
have rw : a ^ card G ∈ S ^ card G
Tactic: rw [← pow_card_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst : Group G
inst_1 : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ S ^ card G * S ^ card G = S ^ card G
have apply : card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ card G * S ^ card G) : Type u_6)
Tactic: apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst : Group G
inst_1 : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ card G * S ^ card G) : Type u_6)
have simp_rw : card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ (card G + card G)) : Type u_6)
Tactic: simp_rw [← pow_add,
        Group.card_pow_eq_card_pow_card_univ S (Fintype.card G + Fintype.card G) le_add_self]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst : Group G
inst_1 : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ S ^ card G * S ^ card G = S ^ card G
have apply : card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ card G * S ^ card G) : Type u_6)
Tactic: classical
    apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm
    simp_rw [← pow_add,
        Group.card_pow_eq_card_pow_card_univ S (Fintype.card G + Fintype.card G) le_add_self]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Semiring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
a : G
ha₀ : 0 ≤ a
ha : IsOfFinOrder a
⊢ a = 1
have obtain : ∀ (n : ℕ) (hn : 0 < n) (ha : a ^ n = 1), a = 1
Tactic: obtain ⟨n, hn, ha⟩ := ha.exists_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x = 0
have rw : ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Tactic: rw [orderOf_eq_zero_iff']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False
have hx₁ : |x| ^ n = 1
Tactic: replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
⊢ False
have inl : ∀ (h : |x| < 1), False
Tactic: rcases h.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
inl : ∀ (h : |x| < 1), False
⊢ False
have inr : ∀ (h : 1 < |x|), False
Tactic: rcases h.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
⊢ orderOf x ≤ 2
have inl : ∀ (h : |x| ≠ 1), orderOf x ≤ 2
Tactic: rcases ne_or_eq |x| 1 with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
inl : ∀ (h : |x| ≠ 1), orderOf x ≤ 2
⊢ orderOf x ≤ 2
have inr : ∀ (h : |x| = 1), orderOf x ≤ 2
Tactic: rcases ne_or_eq |x| 1 with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| = 1
⊢ orderOf x ≤ 2
have inr : ∀ (h : Eq.{u_1 + 1} (α := G) |1| 1), orderOf.{u_1} (G := G) 1 ≤ 2
Tactic: rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| = 1
inr : ∀ (h : Eq.{u_1 + 1} (α := G) |1| 1), orderOf.{u_1} (G := G) 1 ≤ 2
⊢ orderOf x ≤ 2
have inr₁ : ∀ (h : Eq.{u_1 + 1} (α := G) |(-1)| 1), orderOf.{u_1} (G := G) (-1) ≤ 2
Tactic: rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst_1 : Finite ι
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x
have have : ∀ (this : Fintype ι), (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst_1 : Finite ι
this : Fintype ι
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x
have simp : (∀ (i : ι), orderOf (x i) ≠ 0) → Ne (α := ℕ) (Finset.lcm Finset.univ fun (i : ι) ↦ orderOf (x i)) 0
Tactic: simp only [← orderOf_ne_zero_iff, Pi.orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : AddGroupWithOne R
inst_1 : Fintype R
⊢ Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0
have rw : HSMul.hSMul (β := R) (card R) 1 = 0
Tactic: rw [← nsmul_one, card_nsmul_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : AddGroupWithOne R
inst_1 : Fintype R
rw : HSMul.hSMul (β := R) (card R) 1 = 0
⊢ Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0
have rw₁ : Eq.{u_6 + 1} (α := R) 0 0
Tactic: rw [← nsmul_one, card_nsmul_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
n : ℕ
⊢ Eq.{u_6 + 1} (α := R) (↑n : R) 0 ↔ addOrderOf.{u_6} (G := R) 1 ∣ n
have rw : HSMul.hSMul (β := R) n 1 = 0 ↔ addOrderOf.{u_6} (G := R) 1 ∣ n
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
n : ℕ
rw : HSMul.hSMul (β := R) n 1 = 0 ↔ addOrderOf.{u_6} (G := R) 1 ∣ n
⊢ Eq.{u_6 + 1} (α := R) (↑n : R) 0 ↔ addOrderOf.{u_6} (G := R) 1 ∣ n
have rw₁ : HSMul.hSMul (β := R) n 1 = 0 ↔ HSMul.hSMul (β := R) n 1 = 0
Tactic: rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
⊢ Eq.{u_6 + 1} (α := R) (↑p : R) 0
have rw : Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0
Tactic: rw [← hn, Nat.cast_card_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
rw : Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0
⊢ Eq.{u_6 + 1} (α := R) (↑p : R) 0
have rw₁ : Eq.{u_6 + 1} (α := R) 0 0
Tactic: rw [← hn, Nat.cast_card_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
⊢ Eq.{u_6 + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
have H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
Tactic: have H : (p : R) = 0 := by rw [← hn, Nat.cast_card_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
⊢ Eq.{u_6 + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
have mp : Eq.{u_6 + 1} (α := R) (↑n : R) 0 → p ∣ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
mp : Eq.{u_6 + 1} (α := R) (↑n : R) 0 → p ∣ n
⊢ Eq.{u_6 + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
have mpr : p ∣ n → Eq.{u_6 + 1} (α := R) (↑n : R) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑n : R) 0
⊢ p ∣ n
have h₁ : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
Tactic: rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
⊢ p ∣ n
have mp : n % p = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
⊢ n % p = 0
have apply : 0 < p
Tactic: apply hR _ (Nat.mod_lt _ _) h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
⊢ 0 < p
have rw : Nonempty R
Tactic: rw [← hn, Fintype.card_pos_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
n : ℕ
⊢ Eq.{u_6 + 1} (α := R) (↑(p * n) : R) 0
have mpr : HMul.hMul (α := R) (↑p : R) (↑n : R) = 0
Tactic: rw [Nat.cast_mul, H, zero_mul]