-- Mathlib/Data/List/SplitBy.lean
theorem splitByLoop_eq_append {r : α → α → Bool} {l : List α} {a : α} {g : List α}
    (gs : List (List α)) : splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []

Proof state:
case cons.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 ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []

Tactic:
induction l generalizing a g gs with
| nil => simp [splitBy.loop]
| cons b l IH =>
  simp_rw [splitBy.loop]
  split <;> rw [IH]
  conv_rhs => rw [IH]
  simp

Result:
no goals

Proof state:
case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r [] a g gs = gs.reverse ++ splitBy.loop r [] a g []

Tactic:
simp [splitBy.loop]

Result:
no goals

Proof state:
case cons
α : 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 α)
⊢ splitBy.loop r (b :: l) a g gs = gs.reverse ++ splitBy.loop r (b :: l) a g []

Tactic:
simp_rw [splitBy.loop]

Result:
case cons
α : 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 α)
⊢ (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs)) =
    gs.reverse ++
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]

Proof state:
case cons
α : 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 α)
⊢ (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs)) =
    gs.reverse ++
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
split <;> rw [IH]

Result:
case cons.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]

Proof state:
case cons.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:
conv_rhs => rw [IH]

Result:
case cons.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 ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])