awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
rw :
  (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul (β := Additive ℤˣ) z ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ z
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul.{u_1, 0, 0} (α := R) (β := Additive ℤˣ) (↑z : R)
        ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ z
have rw₁ : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u) : ℤˣ) z =
  u ^ z
Tactic: rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
rw :
  (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul (β := Additive ℤˣ) z ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ z
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u) : ℤˣ) z =
    u ^ z
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul.{u_1, 0, 0} (α := R) (β := Additive ℤˣ) (↑z : R)
        ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ z
have rw₂ : u ^ z = u ^ z
Tactic: rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
a : ℤ
⊢ AddSubgroup.index (AddSubgroup.zmultiples a) = a.natAbs
have rw : Nat.card (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (AddSubgroup.zmultiples a)) = a.natAbs
Tactic: rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
a : ℤ
rw : Nat.card (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (AddSubgroup.zmultiples a)) = a.natAbs
⊢ AddSubgroup.index (AddSubgroup.zmultiples a) = a.natAbs
have rw₁ : Nat.card (ZMod a.natAbs) = a.natAbs
Tactic: rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
a : ℤ
rw : Nat.card (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (AddSubgroup.zmultiples a)) = a.natAbs
rw₁ : Nat.card (ZMod a.natAbs) = a.natAbs
⊢ AddSubgroup.index (AddSubgroup.zmultiples a) = a.natAbs
have rw₂ : a.natAbs = a.natAbs
Tactic: rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
n : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
⊢ LE.le (α := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
    (comap.{0, u_3} (N := ↥(zmultiples a))
      ((zmultiplesHom ↥(zmultiples a) : (a_1 : ↥(zmultiples a)) → ℤ →+ ↥(zmultiples a))
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯))
      (stabilizer (↥(zmultiples a)) b))
have rw : HSMul.hSMul (β := ↥(zmultiples a)) (minimalPeriod (fun (x : β) ↦ a +ᵥ x) b)
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a sorry) +ᵥ
    b =
  b
Tactic: rw [zmultiples_le, mem_comap, mem_stabilizer_iff, zmultiplesHom_apply, natCast_zsmul]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
n : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
⊢ HSMul.hSMul (β := ↥(zmultiples a)) (minimalPeriod (fun (x : β) ↦ a +ᵥ x) b)
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯) +ᵥ
      b =
    b
have simp_rw : (fun (x : β) ↦
        HVAdd.hVAdd (α := ↥(zmultiples a))
          (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a sorry)
          x)^[minimalPeriod (fun (x : β) ↦ a +ᵥ x) b]
    b =
  b
Tactic: simp_rw [← vadd_iterate]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
n : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
⊢ Injective (α :=
    HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))) (β :=
    HasQuotient.Quotient ↥(zmultiples a) (B := AddSubgroup ↥(zmultiples a)) (stabilizer (↥(zmultiples a)) b))
    (⇑(QuotientAddGroup.map (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
          (stabilizer (↥(zmultiples a)) b)
          ((zmultiplesHom ↥(zmultiples a) : (a_1 : ↥(zmultiples a)) → ℤ →+ ↥(zmultiples a))
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯))
          ⋯) :
      (a_1 : ℤ ⧸ zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ)) →
        ↥(zmultiples a) ⧸ stabilizer (↥(zmultiples a)) b)
have rw : LE.le (α :=
  AddSubgroup
    (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))))
  (ker
    (QuotientAddGroup.map (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ)) (stabilizer (↥(zmultiples a)) b)
      ((zmultiplesHom ↥(zmultiples a) : (a_1 : ↥(zmultiples a)) → ℤ →+ ↥(zmultiples a))
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a sorry))
      sorry))
  ⊥
Tactic: rw [← ker_eq_bot_iff, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
n : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
⊢ LE.le (α :=
    AddSubgroup
      (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))))
    (ker
      (QuotientAddGroup.map (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
        (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a) : (a_1 : ↥(zmultiples a)) → ℤ →+ ↥(zmultiples a))
          (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯))
        ⋯))
    ⊥
have refine : ∀ (q : HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))) (n : ℤ)
  (hn :
    Membership.mem (γ :=
      AddSubgroup
        (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))))
      (ker
        (QuotientAddGroup.map (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
          (stabilizer (↥(zmultiples a)) b)
          ((zmultiplesHom ↥(zmultiples a) : (a_1 : ↥(zmultiples a)) → ℤ →+ ↥(zmultiples a))
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a sorry))
          sorry))
      (↑n : ℤ ⧸ zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))),
  Membership.mem (γ :=
    AddSubgroup
      (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))))
    ⊥ (↑n : ℤ ⧸ zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
Tactic: refine fun q => induction_on q fun n hn => ?_
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
n_1 : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
q : HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
n : ℤ
hn :
  Membership.mem (γ :=
    AddSubgroup
      (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))))
    (ker
      (QuotientAddGroup.map (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
        (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a) : (a_1 : ↥(zmultiples a)) → ℤ →+ ↥(zmultiples a))
          (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯))
        ⋯))
    (↑n : ℤ ⧸ zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
⊢ Membership.mem (γ :=
    AddSubgroup
      (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))))
    ⊥ (↑n : ℤ ⧸ zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
have rw : n • a +ᵥ b = b
Tactic: rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ←
              zsmul_vadd_eq_iff_minimalPeriod_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
k : ℤ
⊢ (Equiv.symm (orbitZPowersEquiv a b) :
        (a_1 : ZMod (minimalPeriod (fun (x : β) ↦ a • x) b)) → (↑(orbit (↥(zpowers a)) b) : Type u_4))
      (↑k : ZMod (minimalPeriod (fun (x : β) ↦ a • x) b)) =
    HSMul.hSMul (β := (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4))
      (HPow.hPow (α := ↥(zpowers a))
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subgroup α) (zpowers a) x) a ⋯) k)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ orbit.{u_3, u_4} (↥(zpowers a)) b) b ⋯)
have rw : HSMul.hSMul (β := (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4))
    (HPow.hPow (α := ↥(zpowers a)) (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subgroup α) (zpowers a) x) a sorry)
      (k % (↑(minimalPeriod (fun (x : β) ↦ a • x) b) : ℤ)))
    (Subtype.mk (p := fun (x : β) ↦ x ∈ orbit.{u_3, u_4} (↥(zpowers a)) b) b sorry) =
  HSMul.hSMul (β := (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4))
    (HPow.hPow (α := ↥(zpowers a)) (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subgroup α) (zpowers a) x) a sorry)
      k)
    (Subtype.mk (p := fun (x : β) ↦ x ∈ orbit.{u_3, u_4} (↥(zpowers a)) b) b sorry)
Tactic: rw [orbitZPowersEquiv_symm_apply, ZMod.coe_intCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
α : Type u_5
β : Type u_6
inst : AddGroup α
a : α
inst_1 : AddAction α β
b : β
k : ℤ
⊢ (Equiv.symm (orbitZMultiplesEquiv a b) :
        (a_1 : ZMod (minimalPeriod (fun (x : β) ↦ a +ᵥ x) b)) → (↑(AddAction.orbit (↥(zmultiples a)) b) : Type u_6))
      (↑k : ZMod (minimalPeriod (fun (x : β) ↦ a +ᵥ x) b)) =
    HVAdd.hVAdd (β := (↑(AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) : Type u_6))
      (HSMul.hSMul (β := ↥(zmultiples a)) k
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) b ⋯)
have rw : HVAdd.hVAdd (β := (↑(AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) : Type u_6))
    (HSMul.hSMul (β := ↥(zmultiples a)) (k % (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a sorry))
    (Subtype.mk (p := fun (x : β) ↦ x ∈ AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) b sorry) =
  HVAdd.hVAdd (β := (↑(AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) : Type u_6))
    (HSMul.hSMul (β := ↥(zmultiples a)) k
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a sorry))
    (Subtype.mk (p := fun (x : β) ↦ x ∈ AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) b sorry)
Tactic: rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
inst_2 : Fintype (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
⊢ minimalPeriod (fun (x : β) ↦ a • x) b = Fintype.card.{u_4} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
have rw : minimalPeriod (fun (x : β) ↦ a • x) b = Fintype.card (ZMod (minimalPeriod (fun (x : β) ↦ a • x) b))
Tactic: rw [← Fintype.ofEquiv_card (orbitZPowersEquiv a b), ZMod.card]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
inst_2 : Fintype (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
rw : minimalPeriod (fun (x : β) ↦ a • x) b = Fintype.card (ZMod (minimalPeriod (fun (x : β) ↦ a • x) b))
⊢ minimalPeriod (fun (x : β) ↦ a • x) b = Fintype.card.{u_4} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
have rw₁ : minimalPeriod (fun (x : β) ↦ a • x) b = minimalPeriod (fun (x : β) ↦ a • x) b
Tactic: rw [← Fintype.ofEquiv_card (orbitZPowersEquiv a b), ZMod.card]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
n : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : Group α
a : α
inst_3 : MulAction α β
b : β
inst_4 : Finite.{u_4 + 1} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
⊢ minimalPeriod (fun (x : β) ↦ a • x) b ≠ 0
have intro : ∀ (val : Fintype (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)), minimalPeriod (fun (x : β) ↦ a • x) b ≠ 0
Tactic: cases nonempty_fintype (orbit (zpowers a) b)
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (hypothesis)
Goal:
n : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : Group α
a : α
inst_3 : MulAction α β
b : β
inst_4 : Finite.{u_4 + 1} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
val : Fintype (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
⊢ minimalPeriod (fun (x : β) ↦ a • x) b ≠ 0
have this : Nonempty.{u_4 + 1} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
Tactic: haveI : Nonempty (orbit (zpowers a) b) := (nonempty_orbit b).to_subtype
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
n : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
α : Type u_3
β : Type u_4
inst_2 : Group α
a : α
inst_3 : MulAction α β
b : β
inst_4 : Finite.{u_4 + 1} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
val : Fintype (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
this : Nonempty.{u_4 + 1} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)
⊢ minimalPeriod (fun (x : β) ↦ a • x) b ≠ 0
have intro : Fintype.card.{u_4} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4) ≠ 0
Tactic: rw [minimalPeriod_eq_card]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (hypothesis)
Goal:
α : Type u_3
inst : Group α
a : α
⊢ Nat.card.{u_3} ↥(zpowers a) = orderOf a
have this : Nat.card.{u_3} (↑(MulAction.orbit (↥(zpowers a)) 1) : Type u_3) =
  Nat.card (ZMod (Function.minimalPeriod (fun (x : α) ↦ a • x) 1))
Tactic: have := Nat.card_congr (MulAction.orbitZPowersEquiv a (1 : α))
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
α : Type u_3
inst : Group α
a : α
this :
  Nat.card.{u_3} (↑(MulAction.orbit (↥(zpowers a)) 1) : Type u_3) =
    Nat.card (ZMod (Function.minimalPeriod (fun (x : α) ↦ a • x) 1))
⊢ Nat.card.{u_3} ↥(zpowers a) = orderOf a
have rwa : ∀
  (this :
    Nat.card.{u_3} (↑(MulAction.orbit (↥(zpowers a)) 1) : Type u_3) = Function.minimalPeriod (fun (x : α) ↦ a • x) 1),
  Nat.card.{u_3} ↥(zpowers a) = orderOf a
Tactic: rwa [Nat.card_zmod, orbit_subgroup_one_eq_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
α : Type u_3
inst : Group α
a : α
this :
  Nat.card.{u_3} (↑(MulAction.orbit (↥(zpowers a)) 1) : Type u_3) =
    Nat.card (ZMod (Function.minimalPeriod (fun (x : α) ↦ a • x) 1))
rwa :
  ∀
    (this :
      Nat.card.{u_3} (↑(MulAction.orbit (↥(zpowers a)) 1) : Type u_3) = Function.minimalPeriod (fun (x : α) ↦ a • x) 1),
    Nat.card.{u_3} ↥(zpowers a) = orderOf a
⊢ Nat.card.{u_3} ↥(zpowers a) = orderOf a
have rwa₁ : ∀ (this : Nat.card.{u_3} (↑(↑(zpowers a) : Set α) : Type u_3) = Function.minimalPeriod (fun (x : α) ↦ a • x) 1),
  Nat.card.{u_3} ↥(zpowers a) = orderOf a
Tactic: rwa [Nat.card_zmod, orbit_subgroup_one_eq_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ Eq (α :=
    (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    ((H.quotientEquivSigmaZMod g :
          (a : G ⧸ H) →
            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
        (g ^ k • Quotient.out q) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
have rw : g ^ k • Quotient.out q =
  ((H.quotientEquivSigmaZMod g).symm :
      (a :
          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
        G ⧸ H)
    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
      ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
      (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))))
Tactic: rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
    zpow_smul_mod_minimalPeriod]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
rw :
  g ^ k • Quotient.out q =
    ((H.quotientEquivSigmaZMod g).symm :
        (a :
            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
          G ⧸ H)
      (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))))
⊢ Eq (α :=
    (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    ((H.quotientEquivSigmaZMod g :
          (a : G ⧸ H) →
            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
        (g ^ k • Quotient.out q) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
have rw₁ : g ^ k • Quotient.out q =
  HPow.hPow (β := ℤ) g
      (ZMod.cast (n := minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))) •
    Quotient.out q
Tactic: rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
    zpow_smul_mod_minimalPeriod]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
rw :
  g ^ k • Quotient.out q =
    ((H.quotientEquivSigmaZMod g).symm :
        (a :
            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
          G ⧸ H)
      (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))))
rw₁ :
  g ^ k • Quotient.out q =
    HPow.hPow (β := ℤ) g
        (ZMod.cast (n := minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
          (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))) •
      Quotient.out q
⊢ Eq (α :=
    (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    ((H.quotientEquivSigmaZMod g :
          (a : G ⧸ H) →
            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
        (g ^ k • Quotient.out q) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
have rw₂ : g ^ k • Quotient.out q = g ^ (k % (↑(minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)) : ℤ)) • Quotient.out q
Tactic: rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
    zpow_smul_mod_minimalPeriod]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
rw :
  g ^ k • Quotient.out q =
    ((H.quotientEquivSigmaZMod g).symm :
        (a :
            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) →
          G ⧸ H)
      (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))))
rw₁ :
  g ^ k • Quotient.out q =
    HPow.hPow (β := ℤ) g
        (ZMod.cast (n := minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
          (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))) •
      Quotient.out q
rw₂ :
  g ^ k • Quotient.out q = g ^ (k % (↑(minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)) : ℤ)) • Quotient.out q
⊢ Eq (α :=
    (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    ((H.quotientEquivSigmaZMod g :
          (a : G ⧸ H) →
            (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
        (g ^ k • Quotient.out q) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q
        (↑k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) :
      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) × ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
have rw₃ : g ^ k • Quotient.out q = g ^ k • Quotient.out q
Tactic: rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
    zpow_smul_mod_minimalPeriod]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
inst_1 : Finite.{u_3 + 1} (G ⧸ H)
inst_2 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
⊢ H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out
have have : ∀ (this : Fintype (G ⧸ H)),
  H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out
Tactic: have : Fintype (G ⧸ H) := Fintype.ofFinite _