awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have key : Eq.{u_6 + 1} (α := G) ((fun (x : ℤ) ↦ g ^ x) (↑((Nat.card G).gcd n) : ℤ))
  ((fun (x : ℤ) ↦ g ^ x) ((↑(Nat.card G) : ℤ) * (Nat.card G).gcdA n + (↑n : ℤ) * (Nat.card G).gcdB n))
Tactic: have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)
-- 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)
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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 ^ (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
⊢ (fun (g : G) ↦ g ^ (Nat.card G).gcdB n) ((fun (g : G) ↦ g ^ n) g) = g
have 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
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