mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xb.length < (xa :: xb).length

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xb.length < (xa :: xb).length
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (map length (sz.splitLengths l))[i] = sz[i]

pp: α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length

Tactic:
]

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (map length (sz.splitLengths l))[i] = sz[i]

α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = true
⊢ gs.reverse ++ splitBy.loop r l b (a :: g) [] = gs.reverse ++ splitBy.loop r l b (a :: g) []

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
]

Goal state after:
case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (i : ℕ) (hi : i < (sz.splitLengths l).length), (sz.splitLengths l)[i].length ≤ b

Tactic:
]

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (i : ℕ) (hi : i < (sz.splitLengths l).length), (sz.splitLengths l)[i].length ≤ b
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten =
    g.reverse ++ a :: b :: l

Tactic:
]

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten =
    g.reverse ++ a :: b :: l
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.rel
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xs.length + 1

Tactic:
]

Goal state after:
case intro.intro.inr.rel
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xs.length + 1
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
]

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = true
⊢ ¬[] ∈ splitBy.loop r l b (a :: g) []

pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
· exact IH

Goal state after:
case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])

Tactic:
]

Goal state after:
case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mp
α : Type u_1
p : ℕ
w : List α
⊢ w <+: take p w ++ w → ∀ i < w.length - p, w[i]? = w[i + p]?

Tactic:
]

Goal state after:
case mp
α : Type u_1
p : ℕ
w : List α
⊢ w <+: take p w ++ w → ∀ i < w.length - p, w[i]? = w[i + p]?
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) a

Tactic:
]

Goal state after:
case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) a
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) []

Tactic:
]

Goal state after:
case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) []
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ Acc (Shortlex r) (head :: tail)

Tactic:
]

Goal state after:
case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ Acc (Shortlex r) (head :: tail)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [(a :: g).reverse].reverse
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
reverse_cons,

Goal state after:
case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [].reverse ++ [(a :: g).reverse]
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ l.length ≤ tail.length

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ l.length ≤ tail.length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [] ∨ m = (a :: g).reverse
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
]

Goal state after:
case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [] ∨ m = (a :: g).reverse
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
⊢ w <+: take p w ++ w

Tactic:
]

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
⊢ w <+: take p w ++ w
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
⊢ IsChain (fun b a ↦ r a b = true) (a :: g)

Tactic:
]

Goal state after:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
⊢ IsChain (fun b a ↦ r a b = true) (a :: g)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
drop : take p w ++ List.drop p w <+: take p w ++ w
⊢ w <+: take p w ++ w

Tactic:
]

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
drop : take p w ++ List.drop p w <+: take p w ++ w
⊢ w <+: take p w ++ w
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w <+: take p w ++ w

Tactic:
]

Goal state after:
α : Type u_1
w : List α
p : ℕ
large : w.length ≤ p
⊢ w <+: take p w ++ w
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case pos
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ w[i]? = w[i]?

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case neg.inl
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
small : i < p
eq : i % p = i
⊢ w[i]? = w[i]?

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
⊢ w[i % p]? = w[i]?

Tactic:
]

Goal state after:
case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
⊢ w[i % p]? = w[i]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
]

Goal state after:
case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
⊢ ∀ i < w.length - p, w[i]? = w[i + p]?

Tactic:
]

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
⊢ ∀ i < w.length - p, w[i]? = w[i + p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
less : i < w.length - p
⊢ w[i % p]? = w[i % p]?

Tactic:
]

Goal state after:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) ([a].reverse ++ g.reverse.reverse)

Tactic:
reverse_cons,

Goal state after:
case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) ([].reverse ++ [a] ++ g.reverse.reverse)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ v[j]? = v[j]?

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ j < v.length

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length

Tactic:
]

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ j < v.length

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
⊢ u.length ≤ j + u.length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) ([a] ++ g)

Tactic:
]

Goal state after:
case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) ([a] ++ g)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ (v ++ w)[j + u.length + p - u.length]? = v[j + p]?

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ u.length ≤ j + u.length + p

Tactic:
]

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ (v ++ w)[j + u.length + p - u.length]? = v[j + p]?

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ u.length ≤ j + u.length + p
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse])

Tactic:
]

Goal state after:
case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse])
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ v[j + u.length + p - u.length]? = v[j + p]?

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ j + u.length + p - u.length < v.length

Tactic:
]

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ v[j + u.length + p - u.length]? = v[j + p]?

α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ j + u.length + p - u.length < v.length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false)
    (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs))

Tactic:
]

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false)
    (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs))