Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
_x : (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝⁵ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y _x →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
w : List α
p✝ : (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝⁴ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, p✝⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
p : ℕ
q✝ : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝³ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, q✝⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
q : ℕ
per_p✝ : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝² :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, ⟨q, per_p✝⟩⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
per_p : w.HasPeriod p
per_q✝¹ : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝¹ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, ⟨q, ⟨per_p, per_q✝¹⟩⟩⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
per_q✝ : w.HasPeriod q
len✝ : p + q - p.gcd q ≤ w.length
a✝ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, ⟨q, ⟨per_p, ⟨per_q✝, len✝⟩⟩⟩⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
p_pos : p > 0
q_pos : q > 0
h✝ hyp : compare p q = Ordering.lt
p_lt_q : p < q
per_q : w.HasPeriod p
len : q + p - q.gcd p ≤ w.length
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (p, q) (q, p)

pp: α : Type u_1
_x : (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝⁵ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y _x →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
w : List α
p✝ : (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝⁴ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, p✝⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
p : ℕ
q✝ : (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝³ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, q✝⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
q : ℕ
per_p✝ : (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝² :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, ⟨q, per_p✝⟩⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
per_p : w.HasPeriod p
per_q✝ : (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length
a✝¹ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, ⟨q, ⟨per_p, per_q✝⟩⟩⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
a✝ :
  ∀
    (y :
      (w : List α) ×' (p : ℕ) ×' (q : ℕ) ×' (_ : w.HasPeriod p) ×' (_ : w.HasPeriod q) ×' p + q - p.gcd q ≤ w.length),
    (invImage
            (fun x ↦
              PSigma.casesOn x fun w p ↦
                PSigma.casesOn p fun p q ↦
                  PSigma.casesOn q fun q per_p ↦
                    PSigma.casesOn per_p fun per_p per_q ↦ PSigma.casesOn per_q fun per_q len ↦ (q, p))
            Prod.instWellFoundedRelation).1
        y ⟨w, ⟨p, ⟨q, ⟨per_p, ⟨per_q, len⟩⟩⟩⟩⟩ →
      y.1.HasPeriod (y.2.1.gcd y.2.2.1)
p_pos : p > 0
q_pos : q > 0
h✝ 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:
all_goals grind

Goal state after: