-- Mathlib/Data/List/SplitBy.lean
theorem chain'_getLast_head_splitByLoop {r : α → α → Bool} (l : List α) {a : α}
    {g : List α} {gs : List (List α)} (hgs' : [] ∉ gs)
    (hgs : gs.Chain' fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false)
    (hga : ∀ m ∈ gs.head?, ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) :
    (splitBy.loop r l a g gs).Chain' fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false

Proof state:
case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : Chain' (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
⊢ Chain' (fun a b => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse])

Tactic:
apply List.chain'_reverse.1

Result:
case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : Chain' (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
⊢ Chain' (fun b a => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse]).reverse

Proof state:
case cons.h_2.hgs'
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ (a :: g).reverse :: gs

Tactic:
simpa using hgs'

Result:
no goals

Proof state:
case cons.h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = false
⊢ Chain' (fun a b => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l b [] ((a :: g).reverse :: gs))

Tactic:
apply IH

Result:
case cons.h_2.hgs'
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ (a :: g).reverse :: gs

case cons.h_2.hgs
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = false
⊢ Chain' (fun b a => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) ((a :: g).reverse :: gs)

case cons.h_2.hga
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = false
⊢ ∀ (m : List α), m ∈ ((a :: g).reverse :: gs).head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [b]).head hb) = false

Proof state:
case cons.h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = true
⊢ Chain' (fun a b => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l b (a :: g) gs)

Tactic:
apply IH hgs' hgs

Result:
case cons.h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = true
⊢ ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) (((a :: g).reverse ++ [b]).head hb) = false

Proof state:
case cons.h_1.intro.intro
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      Chain' (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) →
          Chain' (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 : Chain' (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
x✝ : Bool
heq✝ : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w✝ : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w✝) = false
⊢ r (m.getLast ha) (((a :: g).reverse ++ [b]).head ⋯) = false

Tactic:
rwa [reverse_cons, head_append_of_ne_nil]

Result:
no goals