[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
    comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
      (stabilizer { x // x ∈ zmultiples a } b)
[PROOFSTEP]
rw [zmultiples_le, mem_comap, mem_stabilizer_iff, zmultiplesHom_apply, coe_nat_zsmul]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ b = b
[PROOFSTEP]
simp_rw [← vadd_iterate]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ (fun x => { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ x)^[minimalPeriod (fun x => a +ᵥ x) b] b = b
[PROOFSTEP]
exact isPeriodicPt_minimalPeriod ((· +ᵥ ·) a) b
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ Injective
    ↑(QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b)))
[PROOFSTEP]
rw [← ker_eq_bot_iff, eq_bot_iff]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ ker
      (QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b))) ≤
    ⊥
[PROOFSTEP]
refine' fun q => induction_on' q fun n hn => _
[GOAL]
n✝ : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)
n : ℤ
hn :
  ↑n ∈
    ker
      (QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b)))
⊢ ↑n ∈ ⊥
[PROOFSTEP]
rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ← zsmul_vadd_eq_iff_minimalPeriod_dvd]
[GOAL]
n✝ : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)
n : ℤ
hn :
  ↑n ∈
    ker
      (QuotientAddGroup.map (zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b))
        (stabilizer { x // x ∈ zmultiples a } b)
        (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
        (_ :
          zmultiples ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) ≤
            comap (↑(zmultiplesHom { x // x ∈ zmultiples a }) { val := a, property := (_ : a ∈ zmultiples a) })
              (stabilizer { x // x ∈ zmultiples a } b)))
⊢ n • a +ᵥ b = b
[PROOFSTEP]
exact (eq_zero_iff _).mp hn
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ↑(orbitZpowersEquiv a b).symm ↑k =
    { val := a, property := (_ : a ∈ zpowers a) } ^ k •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) }
[PROOFSTEP]
rw [orbitZpowersEquiv_symm_apply, ZMod.coe_int_cast]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ { val := a, property := (_ : a ∈ zpowers a) } ^ (k % ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b)) •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) } =
    { val := a, property := (_ : a ∈ zpowers a) } ^ k •
      { val := b, property := (_ : b ∈ orbit { x // x ∈ zpowers a } b) }
[PROOFSTEP]
exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁵ : AddGroup A
inst✝⁴ : Ring R
α✝ : Type u_3
β✝ : Type u_4
inst✝³ : Group α✝
a✝ : α✝
inst✝² : MulAction α✝ β✝
b✝ : β✝
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ ↑(orbitZmultiplesEquiv a b).symm ↑k =
    k • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ
      { val := b, property := (_ : b ∈ AddAction.orbit { x // x ∈ zmultiples a } b) }
[PROOFSTEP]
rw [AddAction.orbit_zmultiples_equiv_symm_apply, ZMod.coe_int_cast]
  -- porting note: times out without `a b` explicit
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁵ : AddGroup A
inst✝⁴ : Ring R
α✝ : Type u_3
β✝ : Type u_4
inst✝³ : Group α✝
a✝ : α✝
inst✝² : MulAction α✝ β✝
b✝ : β✝
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)) • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ
      { val := b, property := (_ : b ∈ AddAction.orbit { x // x ∈ zmultiples a } b) } =
    k • { val := a, property := (_ : a ∈ zmultiples a) } +ᵥ
      { val := b, property := (_ : b ∈ AddAction.orbit { x // x ∈ zmultiples a } b) }
[PROOFSTEP]
exact Subtype.ext (zsmul_vadd_mod_minimalPeriod a b k)
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b = Fintype.card ↑(orbit { x // x ∈ zpowers a } b)
[PROOFSTEP]
rw [← Fintype.ofEquiv_card (orbitZpowersEquiv a b), @ZMod.card _ (_)]
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b ≠ 0
[PROOFSTEP]
cases nonempty_fintype (orbit (zpowers a) b)
[GOAL]
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
val✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b ≠ 0
[PROOFSTEP]
haveI : Nonempty (orbit (zpowers a) b) := (orbit_nonempty b).to_subtype
[GOAL]
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
val✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
this : Nonempty ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b ≠ 0
[PROOFSTEP]
rw [minimalPeriod_eq_card]
[GOAL]
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit { x // x ∈ zpowers a } b)
val✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
this : Nonempty ↑(orbit { x // x ∈ zpowers a } b)
⊢ Fintype.card ↑(orbit { x // x ∈ zpowers a } b) ≠ 0
[PROOFSTEP]
exact Fintype.card_ne_zero
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
⊢ orderOf a = Nat.card { x // x ∈ zpowers a }
[PROOFSTEP]
have := Nat.card_congr (MulAction.orbitZpowersEquiv a (1 : α))
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
this :
  Nat.card ↑(MulAction.orbit { x // x ∈ zpowers a } 1) =
    Nat.card (ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) a) 1))
⊢ orderOf a = Nat.card { x // x ∈ zpowers a }
[PROOFSTEP]
rwa [Nat.card_zmod, orbit_subgroup_one_eq_self, eq_comm] at this 
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
h : IsOfFinOrder a
⊢ Finite { x // x ∈ zpowers a }
[PROOFSTEP]
rw [← orderOf_pos_iff, order_eq_card_zpowers'] at h 
[GOAL]
n : ℕ
A : Type u_1
R : Type u_2
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_3
inst✝ : Group α
a : α
h : 0 < Nat.card { x // x ∈ zpowers a }
⊢ Finite { x // x ∈ zpowers a }
[PROOFSTEP]
exact Nat.finite_of_card_ne_zero h.ne.symm
