awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
k : ZMod (minimalPeriod (fun (x : β) ↦ a • x) b)
⊢ (Equiv.symm (orbitZPowersEquiv a b) :
        (a_1 : ZMod (minimalPeriod (fun (x : β) ↦ a • x) b)) → (↑(orbit (↥(zpowers a)) b) : Type u_4))
      k =
    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.cast)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ orbit.{u_3, u_4} (↥(zpowers a)) b) b ⋯)

Tactic:
rfl

Premises used: Subtype.map, ZMod.cast, Quotient.liftOn', MulAction.ofQuotientStabilizer, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
k : ℤ
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 ⋯)
        (k % (↑(minimalPeriod (fun (x : β) ↦ a • x) b) : ℤ)))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ orbit.{u_3, u_4} (↥(zpowers a)) b) 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 ⋯)
⊢ (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 ⋯)

Tactic:
rw [orbitZPowersEquiv_symm_apply, ZMod.coe_intCast]

Premises used: MulAction.orbitZPowersEquiv_symm_apply, ZMod.coe_intCast
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
k : ℤ
⊢ 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 % (↑(minimalPeriod (fun (x : β) ↦ a • x) b) : ℤ)))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ orbit.{u_3, u_4} (↥(zpowers a)) b) 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 ⋯)

Tactic:
Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)

Premises used: MulAction.zpow_smul_mod_minimalPeriod, Subtype.ext
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
k : ℤ
⊢ 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 % (↑(minimalPeriod (fun (x : β) ↦ a • x) b) : ℤ)))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ orbit.{u_3, u_4} (↥(zpowers a)) b) 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 ⋯)

Tactic:
exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)

Premises used: Subtype.ext
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_5
β : Type u_6
inst : AddGroup α
a : α
inst_1 : AddAction α β
b : β
k : ℤ
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 ⋯))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) 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 ⋯)
⊢ (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 ⋯)

Tactic:
rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast]

Premises used: AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_5
β : Type u_6
inst : AddGroup α
a : α
inst_1 : AddAction α β
b : β
k : ℤ
⊢ 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 ⋯))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) 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 ⋯)

Tactic:
Subtype.ext (zsmul_vadd_mod_minimalPeriod a _ k)

Premises used: AddAction.zsmul_vadd_mod_minimalPeriod, Subtype.ext
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_5
β : Type u_6
inst : AddGroup α
a : α
inst_1 : AddAction α β
b : β
k : ℤ
⊢ 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 ⋯))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ AddAction.orbit.{u_5, u_6} (↥(zmultiples a)) b) 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 ⋯)

Tactic:
exact Subtype.ext (zsmul_vadd_mod_minimalPeriod a _ k)

Premises used: Subtype.ext
-- Module: Mathlib.Data.ZMod.QuotientGroup
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))
rw₁ rw₂ : minimalPeriod (fun (x : β) ↦ a • x) b = 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)

Tactic:
rw [← Fintype.ofEquiv_card (orbitZPowersEquiv a b), ZMod.card]

Premises used: Fintype.ofEquiv_card, ZMod.card, MulAction.orbitZPowersEquiv
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)
intro : ∀ (val : Fintype (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4)), minimalPeriod (fun (x : β) ↦ a • x) b ≠ 0
⊢ minimalPeriod (fun (x : β) ↦ a • x) b ≠ 0

Tactic:
cases nonempty_fintype (orbit (zpowers a) b)

Premises used: Membership.mem, Set.Elem, Subtype, MulAction.orbit, nonempty_fintype, Subgroup.zpowers
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)
⊢ 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
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)
intro : Fintype.card.{u_4} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4) ≠ 0
⊢ minimalPeriod (fun (x : β) ↦ a • x) b ≠ 0

Tactic:
rw [minimalPeriod_eq_card]

Premises used: MulAction.minimalPeriod_eq_card
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)
⊢ Fintype.card.{u_4} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4) ≠ 0

Tactic:
Fintype.card_ne_zero

Premises used: Fintype.card_ne_zero
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)
⊢ Fintype.card.{u_4} (↑(orbit.{u_3, u_4} (↥(zpowers a)) b) : Type u_4) ≠ 0

Tactic:
exact Fintype.card_ne_zero

Premises used: Fintype.card_ne_zero
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
inst : Group α
a : α
⊢ 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 : α))
-- Module: Mathlib.Data.ZMod.QuotientGroup
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
rwa₁ rwa₂ rwa₃ 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
⊢ Nat.card.{u_3} ↥(zpowers a) = orderOf a

Tactic:
rwa [Nat.card_zmod, orbit_subgroup_one_eq_self] at this

Premises used: Nat.card_zmod, orbit_subgroup_one_eq_self
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
inst : Group α
a : α
⊢ (↑(zpowers a) : Set α).Finite ↔ IsOfFinOrder a

Tactic:
simp only [← orderOf_pos_iff, ← Nat.card_zpowers, Nat.card_pos_iff, ← SetLike.coe_sort_coe,
    nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, OneMemClass.coe_nonempty, true_and]

Premises used: SetLike.coe_sort_coe, OneMemClass.coe_nonempty, Set.nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, Nat.card_zpowers, orderOf_pos_iff, true_and
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
inst : Group α
a : α
⊢ (↑(zpowers a) : Set α).Infinite ↔ ¬IsOfFinOrder a

Tactic:
finite_zpowers.not

Premises used: finite_zpowers, Iff.not, Set.Infinite
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (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) =
    HPow.hPow (β := ℤ) g k.cast • Quotient.out q

Tactic:
rfl

Premises used: ZMod.cast, Quotient.liftOn', MulAction.ofQuotientStabilizer, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Data.ZMod.QuotientGroup
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
rw₃ rw₄ : g ^ k • Quotient.out q = g ^ k • 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)))

Tactic:
rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
    zpow_smul_mod_minimalPeriod]

Premises used: MulAction.zpow_smul_mod_minimalPeriod, Subgroup.quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)))
have :
  ∀ (this : Fintype (G ⧸ H)),
    H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out
⊢ 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 _
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)))
this : Fintype (G ⧸ H)
have :
  ∀
    (this :
      (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) →
        Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)),
    H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out
⊢ H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out

Tactic:
have (q : Quotient (MulAction.orbitRel (zpowers g) (G ⧸ H))) :
      Fintype (MulAction.orbit (zpowers g) q.out) := Fintype.ofFinite _
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)))
this_1 : Fintype (G ⧸ H)
this :
  (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)
simp :
  Fintype.card.{u_3} (G ⧸ H) =
    ∑ x : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), Fintype.card.{u_3} (↑(orbit (↥(zpowers g)) x.out) : Type u_3)
⊢ H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out

Tactic:
simp only [MulAction.minimalPeriod_eq_card, index_eq_card, Nat.card_eq_fintype_card]

Premises used: Subgroup.index_eq_card, MulAction.minimalPeriod_eq_card, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)))
this_1 : Fintype (G ⧸ H)
this :
  (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)
rw :
  Fintype.card.{u_3} (G ⧸ H) =
    Fintype.card.{u_3}
      ((x : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) × (↑(orbit (↥(zpowers g)) x.out) : Type u_3))
⊢ Fintype.card.{u_3} (G ⧸ H) =
    ∑ x : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), Fintype.card.{u_3} (↑(orbit (↥(zpowers g)) x.out) : Type u_3)

Tactic:
rw [← Fintype.card_sigma]

Premises used: Fintype.card_sigma
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)))
this_1 : Fintype (G ⧸ H)
this :
  (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)
⊢ Fintype.card.{u_3} (G ⧸ H) =
    Fintype.card.{u_3}
      ((x : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) × (↑(orbit (↥(zpowers g)) x.out) : Type u_3))

Tactic:
Fintype.card_congr (MulAction.selfEquivSigmaOrbits (zpowers g) (G ⧸ H))

Premises used: Fintype.card_congr, Membership.mem, Subtype, HasQuotient.Quotient, Subgroup.zpowers, MulAction.selfEquivSigmaOrbits
-- Module: Mathlib.Data.ZMod.QuotientGroup
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)))
this_1 : Fintype (G ⧸ H)
this :
  (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)
⊢ Fintype.card.{u_3} (G ⧸ H) =
    Fintype.card.{u_3}
      ((x : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) × (↑(orbit (↥(zpowers g)) x.out) : Type u_3))

Tactic:
exact Fintype.card_congr (MulAction.selfEquivSigmaOrbits (zpowers g) (G ⧸ H))

Premises used: Fintype.card_congr, Membership.mem, Subtype, HasQuotient.Quotient, Subgroup.zpowers, MulAction.selfEquivSigmaOrbits
-- Module: Mathlib.Data.ZMod.QuotientRing
Goal:
n : ℕ
⊢ Eq (α := ℤ →+* ZMod n)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(quotientSpanNatEquivZMod n) : ℤ ⧸ Ideal.span {(↑n : ℤ)} →+* ZMod n)
      (Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)})))
    (castRingHom (ZMod n))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.Data.ZMod.QuotientRing
Goal:
n : ℕ
a :
  ∀ (x : ℤ),
    Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
      ((@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
              (↑(quotientSpanNatEquivZMod n).symm : ZMod n →+* ℤ ⧸ Ideal.span {(↑n : ℤ)}) (castRingHom (ZMod n)) :
            (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)})
          x :
        HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}) : (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)}) x :
        HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
⊢ Eq (α := ℤ →+* HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
    (@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
      (↑(quotientSpanNatEquivZMod n).symm : ZMod n →+* ℤ ⧸ Ideal.span {(↑n : ℤ)}) (castRingHom (ZMod n)))
    (Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}))

Tactic:
ext
-- Module: Mathlib.Data.ZMod.QuotientRing
Goal:
n : ℕ
x : ℤ
⊢ Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
    ((@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
            (↑(quotientSpanNatEquivZMod n).symm : ZMod n →+* ℤ ⧸ Ideal.span {(↑n : ℤ)}) (castRingHom (ZMod n)) :
          (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)})
        x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}) : (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)}) x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))

Tactic:
simp
-- Module: Mathlib.Data.ZMod.QuotientRing
Goal:
n : ℤ
⊢ Eq (α := ℤ →+* ZMod n.natAbs)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑n.quotientSpanEquivZMod : ℤ ⧸ Ideal.span {n} →+* ZMod n.natAbs) (Ideal.Quotient.mk (Ideal.span {n})))
    (castRingHom (ZMod n.natAbs))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.Data.ZMod.QuotientRing
Goal:
n : ℤ
a :
  ∀ (x : ℤ),
    Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
      ((@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
              (↑n.quotientSpanEquivZMod.symm : ZMod n.natAbs →+* ℤ ⧸ Ideal.span {n}) (castRingHom (ZMod n.natAbs)) :
            (a : ℤ) → ℤ ⧸ Ideal.span {n})
          x :
        HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
      ((Ideal.Quotient.mk (Ideal.span {n}) : (a : ℤ) → ℤ ⧸ Ideal.span {n}) x :
        HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
⊢ Eq (α := ℤ →+* HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
    (@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
      (↑n.quotientSpanEquivZMod.symm : ZMod n.natAbs →+* ℤ ⧸ Ideal.span {n}) (castRingHom (ZMod n.natAbs)))
    (Ideal.Quotient.mk (Ideal.span {n}))

Tactic:
ext
-- Module: Mathlib.Data.ZMod.QuotientRing
Goal:
n x : ℤ
⊢ Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
    ((@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
            (↑n.quotientSpanEquivZMod.symm : ZMod n.natAbs →+* ℤ ⧸ Ideal.span {n}) (castRingHom (ZMod n.natAbs)) :
          (a : ℤ) → ℤ ⧸ Ideal.span {n})
        x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
    ((Ideal.Quotient.mk (Ideal.span {n}) : (a : ℤ) → ℤ ⧸ Ideal.span {n}) x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))

Tactic:
simp
-- Module: Mathlib.Data.ZMod.QuotientRing
Goal:
n_1 : ℕ
A : Type u_1
R : Type u_2
inst : AddGroup A
inst_1 : Ring R
n : ℤ
inst_2 : NeZero n
⊢ Finite (HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))

Tactic:
Finite.of_equiv _ n.quotientSpanEquivZMod.symm.toEquiv

Premises used: Finite.of_equiv, RingEquiv.toEquiv, Int.quotientSpanEquivZMod, RingEquiv.symm
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : n ∣ m
⊢ unitsMap hm = Units.map (↑(castHom hm (ZMod n)) : ZMod m →* ZMod n)

Tactic:
rfl

Premises used: ZMod.unitsMap, rfl