awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Factorial
Goal:
n p : ℕ
h : n ≤ p
rw : (↑(∏ i ∈ range n, (p - 1 - i)) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * (↑(∏ i ∈ range n, (i + 1)) : ZMod p)
⊢ (↑((p - 1).descFactorial n) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * (↑n ! : ZMod p)

Tactic:
rw [descFactorial_eq_prod_range, factorial_eq_prod_range_add_one]

Premises used: Nat.descFactorial_eq_prod_range, Nat.factorial_eq_prod_range_add_one
-- Module: Mathlib.Data.ZMod.Factorial
Goal:
n p : ℕ
h : n ≤ p
simp : ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * ∏ i ∈ range n, (↑(i + 1) : ZMod p)
⊢ (↑(∏ i ∈ range n, (p - 1 - i)) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * (↑(∏ i ∈ range n, (i + 1)) : ZMod p)

Tactic:
simp only [cast_prod]

Premises used: Nat.cast_prod
-- Module: Mathlib.Data.ZMod.Factorial
Goal:
n p : ℕ
h : n ≤ p
nth_rw :
  ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) #(range n) * ∏ i ∈ range n, (↑(i + 1) : ZMod p)
⊢ ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * ∏ i ∈ range n, (↑(i + 1) : ZMod p)

Tactic:
nth_rw 2 [← card_range n]

Premises used: Finset.card_range
-- Module: Mathlib.Data.ZMod.Factorial
Goal:
n p : ℕ
h : n ≤ p
rw :
  Eq (α := ZMod p) (∏ i ∈ range n, (↑(p - 1 - i) : ZMod p))
    (∏ a ∈ range n, HMul.hMul (α := ZMod p) (-1) (↑(a + 1) : ZMod p))
⊢ ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) #(range n) * ∏ i ∈ range n, (↑(i + 1) : ZMod p)

Tactic:
rw [pow_card_mul_prod]

Premises used: Finset.pow_card_mul_prod
-- Module: Mathlib.Data.ZMod.Factorial
Goal:
n p : ℕ
h : n ≤ p
⊢ Eq (α := ZMod p) (∏ i ∈ range n, (↑(p - 1 - i) : ZMod p))
    (∏ a ∈ range n, HMul.hMul (α := ZMod p) (-1) (↑(a + 1) : ZMod p))

Tactic:
prod_congr rfl ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.ZMod.Factorial
Goal:
n p : ℕ
h : n ≤ p
refine : ∀ x ∈ range n, (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
⊢ Eq (α := ZMod p) (∏ i ∈ range n, (↑(p - 1 - i) : ZMod p))
    (∏ a ∈ range n, HMul.hMul (α := ZMod p) (-1) (↑(a + 1) : ZMod p))

Tactic:
refine prod_congr rfl ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.ZMod.Factorial
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₅ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₆ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    HMul.hMul (α := ZMod p) (-1) (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₇ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    -HMul.hMul (α := ZMod p) 1 (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₈ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -(↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₉ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = HAdd.hAdd (α := ZMod p) (-(↑x : ZMod p)) (-1)
rw₁₀ rw₁₁ : HAdd.hAdd (α := ZMod p) (-(↑x : ZMod p)) (-1) = HAdd.hAdd (α := ZMod p) (-(↑x : ZMod p)) (-1)
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)

Tactic:
rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]

Premises used: neg_add_rev, CharP.cast_eq_zero, Iff.mpr, Nat.cast_succ, List.mem_range, Nat.cast_sub, tsub_add_eq_tsub_tsub_swap, add_comm, Nat.add_one_le_iff, Nat.le_trans, Iff.mp, mul_add, neg_mul, mul_one, one_mul, zero_sub
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
z : ZMod 2
au : Additive ℤˣ
⊢ z • au = z.val • au

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
n : ℕ
au : Additive ℤˣ
⊢ HSMul.hSMul (α := ZMod 2) (↑n : ZMod 2) au = n • au

Tactic:
(Int.units_pow_eq_pow_mod_two au n).symm

Premises used: Additive, Int.units_pow_eq_pow_mod_two, Eq.symm, ZMod.val
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
rw :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val * z₂.val % 2) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
rw₂ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val * z₂.val) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
rw₃ rw₄ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val ^ z₁.val

Tactic:
rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]

Premises used: ZMod.val_mul, Int.units_pow_eq_pow_mod_two, pow_mul, mul_comm
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
rw :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) ((z₁.val + z₂.val) % 2) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
rw₂ rw₃ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₁.val *
      HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val

Tactic:
rw [← pow_add, ZMod.val_add, ← Int.units_pow_eq_pow_mod_two]

Premises used: ZMod.val_add, pow_add, Int.units_pow_eq_pow_mod_two
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
⊢ Int.instUnitsPow = Monoid.toPow

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
⊢ Int.instUnitsPow = DivInvMonoid.toZPow

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
r : R
⊢ (Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) (u ^ r) =
    HSMul.hSMul (β := Additive ℤˣ) r ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
u : Additive ℤˣ
r : R
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ) (r • u) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) u : ℤˣ) r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
rw :
  (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul (β := Additive ℤˣ) n ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ n
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u) : ℤˣ) n =
    u ^ n
rw₂ rw₃ : u ^ n = u ^ n
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul.{u_1, 0, 0} (α := R) (β := Additive ℤˣ) (↑n : R)
        ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ n

Tactic:
rw [Nat.cast_smul_eq_nsmul, toMul_nsmul, toMul_ofMul]

Premises used: toMul_ofMul, toMul_nsmul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
s : ℤˣ
n : ℕ
inst_2 : n.AtLeastTwo
⊢ HPow.hPow.{0, u_1, 0} (β := R) s (OfNat.ofNat n) = HPow.hPow (β := ℕ) s (OfNat.ofNat n)

Tactic:
uzpow_natCast _ _

Premises used: uzpow_natCast
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
x : R
⊢ HPow.hPow (α := ℤˣ) 1 x = 1

Tactic:
Additive.ofMul.injective <| smul_zero _

Premises used: smul_zero, Additive.ofMul, Equiv.injective
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
s₁ s₂ : ℤˣ
x : R
⊢ (s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x

Tactic:
Additive.ofMul.injective <| smul_add x (Additive.ofMul s₁) (Additive.ofMul s₂)

Premises used: Additive.ofMul, Equiv.injective, DFunLike.coe, smul_add
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
s : ℤˣ
⊢ HPow.hPow.{0, u_1, 0} (β := R) s 0 = 1

Tactic:
Additive.ofMul.injective <| zero_smul R (Additive.ofMul s)

Premises used: Additive.ofMul, zero_smul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
s : ℤˣ
⊢ HPow.hPow.{0, u_1, 0} (β := R) s 1 = s

Tactic:
Additive.ofMul.injective <| one_smul R (Additive.ofMul s)

Premises used: Additive.ofMul, one_smul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
s : ℤˣ
x y : R
⊢ s ^ (x * y) = (s ^ x) ^ y

Tactic:
Additive.ofMul.injective <| mul_comm x y ▸ mul_smul y x (Additive.ofMul s)

Premises used: Eq.rec, Additive.ofMul, mul_comm, Equiv.injective, Eq.symm, DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
s : ℤˣ
x y : R
⊢ s ^ (x + y) = s ^ x * s ^ y

Tactic:
Additive.ofMul.injective <| add_smul x y (Additive.ofMul s)

Premises used: Additive.ofMul, add_smul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Module R (Additive ℤˣ)
s : ℤˣ
x y : R
⊢ s ^ (x - y) = s ^ x / s ^ y

Tactic:
Additive.ofMul.injective <| sub_smul x y (Additive.ofMul s)

Premises used: sub_smul, Additive.ofMul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.ZMod.IntUnitsPower
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Module R (Additive ℤˣ)
s : ℤˣ
x : R
⊢ s ^ (-x) = (s ^ x)⁻¹

Tactic:
Additive.ofMul.injective <| neg_smul x (Additive.ofMul s)

Premises used: neg_smul, Additive.ofMul, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.ZMod.IntUnitsPower
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
rw₂ rw₃ : 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

Tactic:
rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]

Premises used: toMul_ofMul, toMul_zsmul, Int.cast_smul_eq_zsmul
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
a : ℤ
rw : Nat.card (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (AddSubgroup.zmultiples a)) = a.natAbs
rw₁ : Nat.card (ZMod a.natAbs) = a.natAbs
rw₂ rw₃ : a.natAbs = a.natAbs
⊢ AddSubgroup.index (AddSubgroup.zmultiples a) = a.natAbs

Tactic:
rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]

Premises used: AddSubgroup.index, Int.quotientZMultiplesEquivZMod, Nat.card_congr, Nat.card_zmod, AddEquiv.toEquiv
-- 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 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
rw :
  HSMul.hSMul (β := ↥(zmultiples a)) (minimalPeriod (fun (x : β) ↦ a +ᵥ x) b)
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯) +ᵥ
      b =
    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))

Tactic:
rw [zmultiples_le, mem_comap, mem_stabilizer_iff, zmultiplesHom_apply, natCast_zsmul]

Premises used: AddSubgroup.zmultiples_le, AddAction.mem_stabilizer_iff, AddSubgroup.mem_comap, zmultiplesHom_apply, natCast_zsmul
-- 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 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
simp_rw :
  (fun (x : β) ↦
          HVAdd.hVAdd (α := ↥(zmultiples a))
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯)
            x)^[minimalPeriod (fun (x : β) ↦ a +ᵥ x) b]
      b =
    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

Tactic:
simp_rw [← vadd_iterate]

Premises used: vadd_iterate
-- 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 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
⊢ (fun (x : β) ↦
          HVAdd.hVAdd (α := ↥(zmultiples a))
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯)
            x)^[minimalPeriod (fun (x : β) ↦ a +ᵥ x) b]
      b =
    b

Tactic:
isPeriodicPt_minimalPeriod (a +ᵥ ·) b

Premises used: Function.isPeriodicPt_minimalPeriod, HVAdd.hVAdd, Function.IsPeriodicPt, Function.IsFixedPt
-- 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 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
⊢ (fun (x : β) ↦
          HVAdd.hVAdd (α := ↥(zmultiples a))
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯)
            x)^[minimalPeriod (fun (x : β) ↦ a +ᵥ x) b]
      b =
    b

Tactic:
exact isPeriodicPt_minimalPeriod (a +ᵥ ·) b

Premises used: Function.isPeriodicPt_minimalPeriod, HVAdd.hVAdd
-- 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 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
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 ⋯))
        ⋯))
    ⊥
⊢ 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)

Tactic:
rw [← ker_eq_bot_iff, eq_bot_iff]

Premises used: AddMonoidHom.ker_eq_bot_iff, eq_bot_iff
-- 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 : 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 ⋯))
        ⋯))
    ⊥

Tactic:
fun q => induction_on q fun n hn => ?_

Premises used: QuotientAddGroup.induction_on
-- 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 : AddGroup α
a : α
inst_3 : AddAction α β
b : β
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 ⋯))
            ⋯))
        (↑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) : ℤ))
⊢ 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 ⋯))
        ⋯))
    ⊥

Tactic:
refine fun q => induction_on q fun n hn => ?_
-- Module: Mathlib.Data.ZMod.QuotientGroup
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) : ℤ))
rw : n • a +ᵥ b = b
⊢ Membership.mem (γ :=
    AddSubgroup
      (HasQuotient.Quotient ℤ (B := AddSubgroup ℤ) (zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))))
    ⊥ (↑n : ℤ ⧸ zmultiples (↑(minimalPeriod (fun (x : β) ↦ a +ᵥ x) b) : ℤ))

Tactic:
rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ←
              zsmul_vadd_eq_iff_minimalPeriod_dvd]

Premises used: AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd, Int.mem_zmultiples_iff, AddSubgroup.mem_bot, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Data.ZMod.QuotientGroup
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) : ℤ))
⊢ n • a +ᵥ b = b

Tactic:
(eq_zero_iff _).mp hn

Premises used: Set.Mem, setOf, Iff.mp, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Data.ZMod.QuotientGroup
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) : ℤ))
⊢ n • a +ᵥ b = b

Tactic:
exact (eq_zero_iff _).mp hn

Premises used: Iff.mp, QuotientAddGroup.eq_zero_iff
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
β : Type u_4
inst : AddGroup α
a : α
inst_1 : AddAction α β
b : β
n : ZMod (minimalPeriod (fun (x : β) ↦ a +ᵥ x) b)
⊢ (AddEquiv.symm (zmultiplesQuotientStabilizerEquiv a b) :
        (a_1 : ZMod (minimalPeriod (fun (x : β) ↦ a +ᵥ x) b)) → ↥(zmultiples a) ⧸ stabilizer (↥(zmultiples a)) b)
      n =
    HSMul.hSMul (α := ℤ) (β :=
      HasQuotient.Quotient ↥(zmultiples a) (B := AddSubgroup ↥(zmultiples a)) (stabilizer (↥(zmultiples a)) b)) n.cast
      (↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := AddSubgroup α) (zmultiples a) x) a ⋯) :
        ↥(zmultiples a) ⧸ stabilizer (↥(zmultiples a)) b)

Tactic:
rfl

Premises used: ZMod.cast, Quotient.liftOn', AddCon.liftOn, QuotientAddGroup.Quotient.addGroup._aux_9, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Data.ZMod.QuotientGroup
Goal:
α : Type u_3
β : Type u_4
inst : Group α
a : α
inst_1 : MulAction α β
b : β
n : ZMod (minimalPeriod (fun (x : β) ↦ a • x) b)
⊢ (MulEquiv.symm (zpowersQuotientStabilizerEquiv a b) :
        (a_1 : Multiplicative (ZMod (minimalPeriod (fun (x : β) ↦ a • x) b))) →
          ↥(zpowers a) ⧸ stabilizer (↥(zpowers a)) b)
      n =
    HPow.hPow (α := HasQuotient.Quotient ↥(zpowers a) (B := Subgroup ↥(zpowers a)) (stabilizer (↥(zpowers a)) b)) (β :=
      ℤ)
      (↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subgroup α) (zpowers a) x) a ⋯) :
        ↥(zpowers a) ⧸ stabilizer (↥(zpowers a)) b)
      n.cast

Tactic:
rfl

Premises used: ZMod.cast, Quotient.liftOn', Set.Mem, AddCon.liftOn, Additive, MulOpposite, setOf, MulAction.orbit, Quot.map, Quotient.map', MulOpposite.unop, rfl