-- 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.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

Tactic:
rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]

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) ([a] ++ g)

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 y x => r x y = true) ([a] ++ g)

Tactic:
exact chain'_cons'.2 ⟨hga, hg⟩

Result:
no goals

Proof state:
case cons
α : 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
h :
  m ∈
    match r a b with
    | true => splitBy.loop r l b (a :: g) []
    | false => splitBy.loop r l b [] [g.reverse ++ [a]]
⊢ Chain' (fun x y => r x y = true) m

Tactic:
split at h

Result:
case cons.h_1
α : 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) []
⊢ Chain' (fun x y => r x y = true) m

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

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)

Tactic:
exact chain'_cons'.2 ⟨hga, hg⟩

Result:
no goals

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 = g.reverse ++ [a] ∨ m ∈ splitBy.loop r l b [] []
⊢ Chain' (fun x y => r x y = true) m

Tactic:
obtain rfl | hm := h

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 x y => r x y = true) (g.reverse ++ [a])

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

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 : b ∈ (a :: g).head?
⊢ r b b✝ = true

Tactic:
rw [head?_cons, Option.mem_some_iff] at 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 : a = b
⊢ r b b✝ = true

Proof state:
case cons
α : 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
h : m ∈ splitBy.loop r (b :: l) a g []
⊢ Chain' (fun x y => r x y = true) m

Tactic:
simp [splitBy.loop] at h

Result:
case cons
α : 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
h :
  m ∈
    match r a b with
    | true => splitBy.loop r l b (a :: g) []
    | false => splitBy.loop r l b [] [g.reverse ++ [a]]
⊢ Chain' (fun x y => r x y = true) m