-- Module: Mathlib.Data.List.PeriodicityLemma
Goal:
α : Type u_1
_x : (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
h :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage (β := ℕ × ℕ)
              (fun
                  (x :
                    (w : List α) ×'
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                PSigma.casesOn (β := fun {w : List α} ↦
                  (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)
                  (motive :=
                  fun
                    (_x :
                      (w : List α) ×'
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  ℕ × ℕ) x
                  fun (w : List α)
                    (p :
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  PSigma.casesOn (β := fun {p : ℕ} ↦
                    (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                    fun
                      (p :
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    ℕ × ℕ) p
                    fun (p : ℕ)
                      (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    PSigma.casesOn (β := fun {q : ℕ} ↦
                      (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                      fun (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      ℕ × ℕ) q
                      fun (q : ℕ) (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      PSigma.casesOn (β := fun (per_p : w.HasPeriod p) ↦
                        (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                        fun (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ)
                        per_p fun (per_p : w.HasPeriod p) (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                        PSigma.casesOn (β := fun (per_q : w.HasPeriod q) ↦ p + q - p.gcd q ≤ w.length) (motive :=
                          fun (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ) per_q
                          fun (per_q : w.HasPeriod q) (len : p + q - p.gcd q ≤ w.length) ↦ (q, p))
              Prod.instWellFoundedRelation :
            WellFoundedRelation
              ((w : List α) ×'
                (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)).1
        y _x →
      HasPeriod.{u_1} (α := α) y.1 (Nat.gcd y.2.1 y.2.2.1)
w : List α
p_1 : (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
h_1 :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage (β := ℕ × ℕ)
              (fun
                  (x :
                    (w : List α) ×'
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                PSigma.casesOn (β := fun {w : List α} ↦
                  (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)
                  (motive :=
                  fun
                    (_x :
                      (w : List α) ×'
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  ℕ × ℕ) x
                  fun (w : List α)
                    (p :
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  PSigma.casesOn (β := fun {p : ℕ} ↦
                    (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                    fun
                      (p :
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    ℕ × ℕ) p
                    fun (p : ℕ)
                      (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    PSigma.casesOn (β := fun {q : ℕ} ↦
                      (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                      fun (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      ℕ × ℕ) q
                      fun (q : ℕ) (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      PSigma.casesOn (β := fun (per_p : w.HasPeriod p) ↦
                        (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                        fun (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ)
                        per_p fun (per_p : w.HasPeriod p) (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                        PSigma.casesOn (β := fun (per_q : w.HasPeriod q) ↦ p + q - p.gcd q ≤ w.length) (motive :=
                          fun (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ) per_q
                          fun (per_q : w.HasPeriod q) (len : p + q - p.gcd q ≤ w.length) ↦ (q, p))
              Prod.instWellFoundedRelation :
            WellFoundedRelation
              ((w : List α) ×'
                (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)).1
        y
        (PSigma.mk (β := fun {w : List α} ↦
          (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) w p_1) →
      HasPeriod.{u_1} (α := α) y.1 (Nat.gcd y.2.1 y.2.2.1)
p : ℕ
q_1 : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
h_2 :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage (β := ℕ × ℕ)
              (fun
                  (x :
                    (w : List α) ×'
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                PSigma.casesOn (β := fun {w : List α} ↦
                  (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)
                  (motive :=
                  fun
                    (_x :
                      (w : List α) ×'
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  ℕ × ℕ) x
                  fun (w : List α)
                    (p :
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  PSigma.casesOn (β := fun {p : ℕ} ↦
                    (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                    fun
                      (p :
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    ℕ × ℕ) p
                    fun (p : ℕ)
                      (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    PSigma.casesOn (β := fun {q : ℕ} ↦
                      (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                      fun (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      ℕ × ℕ) q
                      fun (q : ℕ) (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      PSigma.casesOn (β := fun (per_p : w.HasPeriod p) ↦
                        (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                        fun (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ)
                        per_p fun (per_p : w.HasPeriod p) (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                        PSigma.casesOn (β := fun (per_q : w.HasPeriod q) ↦ p + q - p.gcd q ≤ w.length) (motive :=
                          fun (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ) per_q
                          fun (per_q : w.HasPeriod q) (len : p + q - p.gcd q ≤ w.length) ↦ (q, p))
              Prod.instWellFoundedRelation :
            WellFoundedRelation
              ((w : List α) ×'
                (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)).1
        y
        (PSigma.mk (β := fun {w : List α} ↦
          (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) w
          (PSigma.mk (β := fun {p : ℕ} ↦
            (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) p q_1)) →
      HasPeriod.{u_1} (α := α) y.1 (Nat.gcd y.2.1 y.2.2.1)
q : ℕ
per_p_1 : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
h_3 :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage (β := ℕ × ℕ)
              (fun
                  (x :
                    (w : List α) ×'
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                PSigma.casesOn (β := fun {w : List α} ↦
                  (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)
                  (motive :=
                  fun
                    (_x :
                      (w : List α) ×'
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  ℕ × ℕ) x
                  fun (w : List α)
                    (p :
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  PSigma.casesOn (β := fun {p : ℕ} ↦
                    (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                    fun
                      (p :
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    ℕ × ℕ) p
                    fun (p : ℕ)
                      (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    PSigma.casesOn (β := fun {q : ℕ} ↦
                      (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                      fun (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      ℕ × ℕ) q
                      fun (q : ℕ) (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      PSigma.casesOn (β := fun (per_p : w.HasPeriod p) ↦
                        (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                        fun (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ)
                        per_p fun (per_p : w.HasPeriod p) (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                        PSigma.casesOn (β := fun (per_q : w.HasPeriod q) ↦ p + q - p.gcd q ≤ w.length) (motive :=
                          fun (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ) per_q
                          fun (per_q : w.HasPeriod q) (len : p + q - p.gcd q ≤ w.length) ↦ (q, p))
              Prod.instWellFoundedRelation :
            WellFoundedRelation
              ((w : List α) ×'
                (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)).1
        y
        (PSigma.mk (β := fun {w : List α} ↦
          (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) w
          (PSigma.mk (β := fun {p : ℕ} ↦
            (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) p
            (PSigma.mk (β := fun {q : ℕ} ↦ (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) q
              per_p_1))) →
      HasPeriod.{u_1} (α := α) y.1 (Nat.gcd y.2.1 y.2.2.1)
per_p : w.HasPeriod p
per_q_1 : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
h_4 :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage (β := ℕ × ℕ)
              (fun
                  (x :
                    (w : List α) ×'
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                PSigma.casesOn (β := fun {w : List α} ↦
                  (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)
                  (motive :=
                  fun
                    (_x :
                      (w : List α) ×'
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  ℕ × ℕ) x
                  fun (w : List α)
                    (p :
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  PSigma.casesOn (β := fun {p : ℕ} ↦
                    (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                    fun
                      (p :
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    ℕ × ℕ) p
                    fun (p : ℕ)
                      (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    PSigma.casesOn (β := fun {q : ℕ} ↦
                      (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                      fun (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      ℕ × ℕ) q
                      fun (q : ℕ) (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      PSigma.casesOn (β := fun (per_p : w.HasPeriod p) ↦
                        (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                        fun (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ)
                        per_p fun (per_p : w.HasPeriod p) (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                        PSigma.casesOn (β := fun (per_q : w.HasPeriod q) ↦ p + q - p.gcd q ≤ w.length) (motive :=
                          fun (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ) per_q
                          fun (per_q : w.HasPeriod q) (len : p + q - p.gcd q ≤ w.length) ↦ (q, p))
              Prod.instWellFoundedRelation :
            WellFoundedRelation
              ((w : List α) ×'
                (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)).1
        y
        (PSigma.mk (β := fun {w : List α} ↦
          (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) w
          (PSigma.mk (β := fun {p : ℕ} ↦
            (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) p
            (PSigma.mk (β := fun {q : ℕ} ↦ (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) q
              (PSigma.mk (β := fun (per_p : w.HasPeriod p) ↦ (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) per_p
                per_q_1)))) →
      HasPeriod.{u_1} (α := α) y.1 (Nat.gcd y.2.1 y.2.2.1)
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
h_5 :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage (β := ℕ × ℕ)
              (fun
                  (x :
                    (w : List α) ×'
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                PSigma.casesOn (β := fun {w : List α} ↦
                  (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)
                  (motive :=
                  fun
                    (_x :
                      (w : List α) ×'
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  ℕ × ℕ) x
                  fun (w : List α)
                    (p :
                      (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                  PSigma.casesOn (β := fun {p : ℕ} ↦
                    (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                    fun
                      (p :
                        (p : ℕ) ×'
                          (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    ℕ × ℕ) p
                    fun (p : ℕ)
                      (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                    PSigma.casesOn (β := fun {q : ℕ} ↦
                      (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                      fun (q : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      ℕ × ℕ) q
                      fun (q : ℕ) (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                      PSigma.casesOn (β := fun (per_p : w.HasPeriod p) ↦
                        (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) (motive :=
                        fun (per_p : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ)
                        per_p fun (per_p : w.HasPeriod p) (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦
                        PSigma.casesOn (β := fun (per_q : w.HasPeriod q) ↦ p + q - p.gcd q ≤ w.length) (motive :=
                          fun (per_q : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) ↦ ℕ × ℕ) per_q
                          fun (per_q : w.HasPeriod q) (len : p + q - p.gcd q ≤ w.length) ↦ (q, p))
              Prod.instWellFoundedRelation :
            WellFoundedRelation
              ((w : List α) ×'
                (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length)).1
        y
        (PSigma.mk (β := fun {w : List α} ↦
          (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) w
          (PSigma.mk (β := fun {p : ℕ} ↦
            (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) p
            (PSigma.mk (β := fun {q : ℕ} ↦ (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) q
              (PSigma.mk (β := fun (per_p : w.HasPeriod p) ↦ (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length) per_p
                (PSigma.mk (β := fun (per_q : w.HasPeriod q) ↦ p + q - p.gcd q ≤ w.length) per_q len))))) →
      HasPeriod.{u_1} (α := α) y.1 (Nat.gcd y.2.1 y.2.2.1)
p_pos : p > 0
q_pos : q > 0
h_6 hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ Prod.Lex (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (fun (a₁ a₂ : ℕ) ↦ a₁ < a₂) (q, p - q) (q, p)

Tactic:
grind