awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
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 ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ 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 ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ 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 (↑n : ℤ) ^ (Nat.card G).gcdB n),
    (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ 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 (↑n : ℤ) ^ (Nat.card G).gcdB n),
    (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₄ :
  ∀
    (key :
      g ^ (Nat.card G).gcd n =
        (g ^ Nat.card G) ^ (Nat.card G).gcdA n * HPow.hPow (β := ℤ) g (↑n : ℤ) ^ (Nat.card G).gcdB n),
    (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₅ :
  ∀ (key : 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 ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₆ :
  ∀ (key : HPow.hPow (β := ℕ) g 1 = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ n) ^ (Nat.card G).gcdB n),
    (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₇ :
  ∀ (key : g = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ n) ^ (Nat.card G).gcdB n),
    (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₈ :
  ∀ (key : g = HPow.hPow (α := G) 1 ((Nat.card G).gcdA n) * (g ^ n) ^ (Nat.card G).gcdB n),
    (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₉ :
  ∀ (key : g = 1 * (g ^ n) ^ (Nat.card G).gcdB n), (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₁₀ :
  ∀ (key : g = (g ^ n) ^ (Nat.card G).gcdB n), (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
rwa₁₁ rwa₁₂ rwa₁₃ rwa₁₄ :
  ∀ (key : (g ^ n) ^ (Nat.card G).gcdB n = g), (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ 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

Premises used: zpow_natCast, zpow_add, zpow_mul, one_zpow, pow_card_eq_one', eq_comm, Nat.Coprime.gcd_eq_one, pow_one, one_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
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
rwa₁₁ rwa₁₂ rwa₁₃ 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
⊢ (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

Premises used: zpow_natCast, zpow_add, zpow_mul', zpow_mul, one_zpow, pow_card_eq_one', eq_comm, Nat.Coprime.gcd_eq_one, pow_one, one_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
n : ℕ
G : Type u_6
inst : Group G
h : (Nat.card G).Coprime n
⊢ Eq (α := G) ((powCoprime h : (a : G) → G) 1 : G) (1 : G)

Tactic:
one_pow n

Premises used: one_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
n : ℕ
G : Type u_6
inst : Group G
h : (Nat.card G).Coprime n
g : G
⊢ Eq (α := G) ((powCoprime h : (a : G) → G) g⁻¹ : G) (((powCoprime h : (a : G) → G) g)⁻¹ : G)

Tactic:
inv_pow g n

Premises used: inv_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
n : ℕ
G : Type u_6
inst : Group G
hn : (Nat.card G).Coprime n
⊢ Bijective (β := G) fun (x : G) ↦ x ^ n

Tactic:
(powCoprime hn).bijective

Premises used: Equiv.bijective, powCoprime
-- Module: Mathlib.GroupTheory.OrderOfElement
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)
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
⊢ Finset.image (fun (i : ℕ) ↦ x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x) : Set G).toFinset

Tactic:
ext x
-- Module: Mathlib.GroupTheory.OrderOfElement
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
h₂ 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
⊢ Membership.mem (γ := Finset G) (Finset.image (fun (i : ℕ) ↦ x_1 ^ i) (Finset.range (orderOf x_1))) x ↔
    x ∈ (↑(zpowers x_1) : Set G).toFinset

Tactic:
rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]

Premises used: mem_zpowers_iff_mem_range_orderOf, SetLike.mem_coe, Set.mem_toFinset
-- Module: Mathlib.GroupTheory.OrderOfElement
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 ≤ g • g ^ (Nat.card G - 1) • a

Tactic:
have key := smul_mono_right g (le_pow_smul h (Nat.card G - 1))
-- Module: Mathlib.GroupTheory.OrderOfElement
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

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

Premises used: Nat.card_pos, smul_smul, pow_card_eq_one', Nat.sub_one_add_one_eq_of_pos, one_smul, pow_succ'
-- Module: Mathlib.GroupTheory.OrderOfElement
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 ≤ a
⊢ g • a = a

Tactic:
le_antisymm key h

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.OrderOfElement
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 ≤ a
⊢ g • a = a

Tactic:
exact le_antisymm key h

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.OrderOfElement
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 • g ^ (Nat.card G - 1) • a ≤ g • a

Tactic:
have key := smul_mono_right g (pow_smul_le h (Nat.card G - 1))
-- Module: Mathlib.GroupTheory.OrderOfElement
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
⊢ 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

Premises used: Nat.card_pos, smul_smul, pow_card_eq_one', Nat.sub_one_add_one_eq_of_pos, one_smul, pow_succ'
-- Module: Mathlib.GroupTheory.OrderOfElement
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 : a ≤ g • a
⊢ g • a = a

Tactic:
le_antisymm h key

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.OrderOfElement
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 : a ≤ g • a
⊢ g • a = a

Tactic:
exact le_antisymm h key

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.OrderOfElement
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
zero : HPow.hPow (β := ℕ) a 1 ∈ S
zero₁ zero₂ zero₃ zero₄ : a ∈ S
⊢ a ^ HAdd.hAdd (α := ℕ) 0 1 ∈ S

Tactic:
rwa [zero_add, pow_one]

Premises used: zero_add, pow_one
-- Module: Mathlib.GroupTheory.OrderOfElement
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
succ : a ^ (n + 1) * a ∈ S * S
⊢ a ^ (n + 1 + 1) ∈ S

Tactic:
rw [← hS2, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.GroupTheory.OrderOfElement
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) * a ∈ S * S

Tactic:
Set.mul_mem_mul ih ha

Premises used: Set.mul_mem_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
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) * a ∈ S * S

Tactic:
exact Set.mul_mem_mul ih ha

Premises used: Set.mul_mem_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
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
succ : ∀ (n : ℕ) (ih : a ^ (n + 1) ∈ S), a ^ (n + 1 + 1) ∈ S
⊢ a ^ (n + 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

Premises used: pow_succ, zero_add, pow_one, Nat.zero, Nat.succ
-- Module: Mathlib.GroupTheory.OrderOfElement
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
obtain : ∀ (a : M) (ha : a ∈ S), 1 ∈ S
⊢ 1 ∈ S

Tactic:
obtain ⟨a, ha⟩ := hS1
-- Module: Mathlib.GroupTheory.OrderOfElement
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
rw : a ^ (orderOf a - succ 0 + succ 0) ∈ S
⊢ 1 ∈ S

Tactic:
rw [← pow_orderOf_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (orderOf_pos a))]

Premises used: Nat.succ_le_of_lt, tsub_add_cancel_of_le, pow_orderOf_eq_one, orderOf_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
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
⊢ a ^ (orderOf a - succ 0 + succ 0) ∈ S

Tactic:
pow_mem a ha (orderOf a - 1)

Premises used: Set.Mem, HSub.hSub, orderOf, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
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
⊢ a ^ (orderOf a - succ 0 + succ 0) ∈ S

Tactic:
exact pow_mem a ha (orderOf a - 1)

Premises used: HSub.hSub, orderOf, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
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
rw : Membership.mem (γ := Submonoid G) (submonoidOfIdempotent S hS1 hS2) (a ^ (orderOf a - succ 0))
⊢ Membership.mem (γ := Submonoid G) (submonoidOfIdempotent S hS1 hS2) a⁻¹

Tactic:
rw [← one_mul a⁻¹, ← pow_one a, ← pow_orderOf_eq_one a, ← pow_sub a (orderOf_pos a)]

Premises used: pow_sub, pow_orderOf_eq_one, Inv.inv, pow_one, orderOf_pos, one_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
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 ^ (orderOf a - succ 0))

Tactic:
pow_mem ha (orderOf a - 1)

Premises used: Set.Mem, HSub.hSub, orderOf, pow_mem, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
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 ^ (orderOf a - succ 0))

Tactic:
exact pow_mem ha (orderOf a - 1)

Premises used: HSub.hSub, orderOf, pow_mem, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
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
obtain : ∀ (a : G) (ha : a ∈ S), 1 ∈ S ^ card G
⊢ 1 ∈ S ^ card G

Tactic:
obtain ⟨a, ha⟩ := hS
-- Module: Mathlib.GroupTheory.OrderOfElement
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
rw : a ^ card G ∈ S ^ card G
rw₁ : G
⊢ 1 ∈ S ^ card G

Tactic:
rw [← pow_card_eq_one]

Premises used: pow_card_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
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
⊢ a ^ card G ∈ S ^ card G

Tactic:
Set.pow_mem_pow ha

Premises used: Set.pow_mem_pow, Set.Mem
-- Module: Mathlib.GroupTheory.OrderOfElement
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
apply : card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ card G * S ^ card G) : Type u_6)
⊢ S ^ card G * S ^ card G = S ^ card G

Tactic:
apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm

Premises used: ge_of_eq, Set.eq_of_subset_of_card_le, Eq.symm, Set.subset_mul_left
-- Module: Mathlib.GroupTheory.OrderOfElement
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
simp_rw : card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ (card G + card G)) : Type u_6)
⊢ card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ card G * S ^ 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]

Premises used: pow_add, Fintype.card, HAdd.hAdd, Group.card_pow_eq_card_pow_card_univ, le_add_self
-- Module: Mathlib.GroupTheory.OrderOfElement
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
apply : card.{u_6} (↑(S ^ card G) : Type u_6) = card.{u_6} (↑(S ^ card G * S ^ card G) : Type u_6)
⊢ S ^ card G * S ^ card G = S ^ card G

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]

Premises used: pow_add
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Semiring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
a : G
ha₀ : 0 ≤ a
ha : IsOfFinOrder a
obtain : ∀ (n : ℕ) (hn : 0 < n) (ha : a ^ n = 1), a = 1
⊢ a = 1

Tactic:
obtain ⟨n, hn, ha⟩ := ha.exists_pow_eq_one

Premises used: IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Semiring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
a : G
ha₀ : 0 ≤ a
ha_1 : IsOfFinOrder a
n : ℕ
hn : 0 < n
ha : a ^ n = 1
⊢ a = 1

Tactic:
(pow_eq_one_iff_of_nonneg ha₀ hn.ne').1 ha

Premises used: LT.lt.ne', Iff.mp, pow_eq_one_iff_of_nonneg
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Semiring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
a : G
ha₀ : 0 ≤ a
ha_1 : IsOfFinOrder a
n : ℕ
hn : 0 < n
ha : a ^ n = 1
⊢ a = 1

Tactic:
exact (pow_eq_one_iff_of_nonneg ha₀ hn.ne').1 ha

Premises used: LT.lt.ne', Iff.mp, pow_eq_one_iff_of_nonneg
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
ha₀ : LE.le.{u_1} (α := G) 1 0
ha : IsOfFinOrder.{u_1} (G := G) 1
⊢ False

Tactic:
one_pos.not_ge ha₀

Premises used: LT.lt.not_ge, one_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
ha₀ : LE.le.{u_1} (α := G) 1 0
ha : IsOfFinOrder.{u_1} (G := G) 1
⊢ False

Tactic:
exact one_pos.not_ge ha₀

Premises used: LT.lt.not_ge, one_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
rw : ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
⊢ orderOf x = 0

Tactic:
rw [orderOf_eq_zero_iff']

Premises used: orderOf_eq_zero_iff'
-- Module: Mathlib.GroupTheory.OrderOfElement
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
⊢ |x| ^ n = 1

Tactic:
simpa only [abs_one, abs_pow] using congr_arg abs hx

Premises used: abs, congr_arg, abs_one, abs_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
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
⊢ |x| ^ n = 1

Tactic:
replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs hx
-- Module: Mathlib.GroupTheory.OrderOfElement
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
inr : ∀ (h : 1 < |x|), False
⊢ False

Tactic:
rcases h.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h_1 : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : |x| < 1
⊢ False

Tactic:
((pow_lt_one₀ (abs_nonneg x) h hn.ne').ne hx).elim

Premises used: False.elim, LT.lt.ne', pow_lt_one₀, abs_nonneg, LT.lt.ne
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h_1 : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : |x| < 1
⊢ False

Tactic:
exact ((pow_lt_one₀ (abs_nonneg x) h hn.ne').ne hx).elim

Premises used: False.elim, LT.lt.ne', pow_lt_one₀, abs_nonneg, LT.lt.ne
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h_1 : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : 1 < |x|
⊢ False

Tactic:
((one_lt_pow₀ h hn.ne').ne' hx).elim

Premises used: False.elim, LT.lt.ne', one_lt_pow₀
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h_1 : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : 1 < |x|
⊢ False

Tactic:
exact ((one_lt_pow₀ h hn.ne').ne' hx).elim

Premises used: False.elim, LT.lt.ne', one_lt_pow₀
-- Module: Mathlib.GroupTheory.OrderOfElement
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
inr : ∀ (h : |x| = 1), orderOf x ≤ 2
⊢ orderOf x ≤ 2

Tactic:
rcases ne_or_eq |x| 1 with h | h

Premises used: ne_or_eq, abs, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x ≤ 2

Tactic:
simp [orderOf_abs_ne_one h]

Premises used: orderOf_abs_ne_one
-- Module: Mathlib.GroupTheory.OrderOfElement
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
inr₁ : ∀ (h : Eq.{u_1 + 1} (α := G) |(-1)| 1), orderOf.{u_1} (G := G) (-1) ≤ 2
⊢ orderOf x ≤ 2

Tactic:
rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)

Premises used: eq_or_eq_neg_of_abs_eq, rfl