-- Mathlib/Data/List/SplitBy.lean
theorem chain'_of_mem_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α}
    (hga : ∀ b ∈ g.head?, r b a) (hg : g.Chain' fun y x ↦ r x y)
    (h : m ∈ splitBy.loop r l a g []) : m.Chain' fun x y ↦ r x y

Proof state:
case cons.h_2.inr
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b = false
hm : m ∈ splitBy.loop r l b [] []
⊢ Chain' (fun x y => r x y = true) m

Tactic:
apply IH _ chain'_nil hm

Result:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b = false
hm : m ∈ splitBy.loop r l b [] []
⊢ ∀ (b_1 : α), b_1 ∈ [].head? → r b_1 b = true

Proof state:
case cons.h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (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) →
      Chain' (fun y x => r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → Chain' (fun x y => r x y = true) (g.reverse ++ [a])
⊢ Chain' (fun x y => r x y = true) (g.reverse ++ [a])

Tactic:
apply List.chain'_reverse.1

Result:
case cons.h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (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) →
      Chain' (fun y x => r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → Chain' (fun x y => r x y = true) (g.reverse ++ [a])
⊢ Chain' (fun y x => r x y = true) (g.reverse ++ [a]).reverse

Proof state:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
⊢ Chain' (fun x y => r x y = true) (a :: g).reverse

Tactic:
apply List.chain'_reverse.1

Result:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
⊢ Chain' (fun y x => r x y = true) (a :: g).reverse.reverse

Proof state:
case nil.inl
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
hm : m ∈ []
⊢ Chain' (fun x y => r x y = true) m

Tactic:
exact (not_mem_nil m hm).elim

Result:
no goals

Proof state:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
⊢ Chain' (fun y x => r x y = true) (a :: g).reverse.reverse

Tactic:
rw [reverse_reverse]

Result:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
⊢ Chain' (fun y x => r x y = true) (a :: g)

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

Tactic:
rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h

Result:
case cons.h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (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 [] []
⊢ Chain' (fun x y => r x y = true) m

Proof state:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b = false
hm : m ∈ splitBy.loop r l b [] []
⊢ ∀ (b_1 : α), b_1 ∈ [].head? → r b_1 b = true

Tactic:
rintro _ ⟨⟩

Result:
no goals

Proof state:
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
⊢ ∀ (b_1 : α), b_1 ∈ (a :: g).head? → r b_1 b = true

Tactic:
intro b hb

Result:
α : Type u_1
m : List α
r : α → α → Bool
b✝ : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b✝ = true
h : m ∈ splitBy.loop r l b✝ (a :: g) []
b : α
hb : b ∈ (a :: g).head?
⊢ r b b✝ = true

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

Tactic:
obtain hm | rfl := h

Result:
case nil.inl
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
hm : m ∈ []
⊢ Chain' (fun x y => r x y = true) m

case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
⊢ Chain' (fun x y => r x y = true) (a :: g).reverse

Proof state:
α : Type u_1
m : List α
r : α → α → Bool
b✝ : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      Chain' (fun y x => r x y = true) g → m ∈ splitBy.loop r l a g [] → Chain' (fun x y => r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
x✝ : Bool
heq✝ : r a b✝ = true
h : m ∈ splitBy.loop r l b✝ (a :: g) []
b : α
hb : a = b
⊢ r b b✝ = true

Tactic:
rwa [← hb]

Result:
no goals

Proof state:
case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
h : m ∈ splitBy.loop r [] a g []
⊢ Chain' (fun x y => r x y = true) m

Tactic:
rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h

Result:
case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : Chain' (fun y x => r x y = true) g
h : m ∈ [] ∨ m = (a :: g).reverse
⊢ Chain' (fun x y => r x y = true) m