-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem to_append_iff : Red L (L₁ ++ L₂) ↔ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂ :=
  Iff.intro
    (by
      generalize eq : L₁ ++ L₂ = L₁₂
      intro h
      induction' h with L' L₁₂ hLL' h ih generalizing L₁ L₂
      · exact ⟨_, _, eq.symm, by rfl, by rfl⟩
      · obtain @⟨s, e, a, b⟩ := h
        rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)
        · have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) = L₁ ++ s' ++ (a, b) :: (a, not b) :: e :=
            by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩
        · have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ = s ++ (a, b) :: (a, not b) :: (e' ++ L₂) :=
            by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩)
    fun ⟨_, _, Eq, h₃, h₄⟩ => Eq.symm ▸ append_append h₃ h₄

Proof state:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ Red L L₁₂ → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
intro h

Result:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
h : Red L L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Proof state:
case tail.not.inr.intro.intro.intro.intro.intro.intro
α : Type u
L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
h₁ : Red w₁ (s ++ (a, b) :: (a, !b) :: e')
h₂ : Red w₂ L₂
⊢ ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩

Result:
no goals

Proof state:
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₂ L₂

Tactic:
rfl

Result:
no goals

Proof state:
case refl
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
exact ⟨_, _, eq.symm, by rfl, by rfl⟩

Result:
no goals

Proof state:
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₁ L₁

Tactic:
rfl

Result:
no goals

Proof state:
case tail.not
α : Type u
L L₁₂ L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)

Result:
case tail.not.inl.intro.intro
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

case tail.not.inr.intro.intro
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Proof state:
case tail.not.inl.intro.intro
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩

Result:
case tail.not.inl.intro.intro.intro.intro.intro.intro
α : Type u
L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
h₁ : Red w₁ L₁
h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)
⊢ ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Proof state:
case tail.not.inl.intro.intro
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) = L₁ ++ s' ++ (a, b) :: (a, not b) :: e :=
  by simp

Result:
case tail.not.inl.intro.intro
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Proof state:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
h : Red L L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
induction' h with L' L₁₂ hLL' h ih generalizing L₁ L₂

Result:
case refl
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

case tail
α : Type u
L L₁₂✝ L' L₁₂ : List (α × Bool)
hLL' : ReflTransGen Step L L'
h : Step L' L₁₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = L' → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Proof state:
case tail
α : Type u
L L₁₂✝ L' L₁₂ : List (α × Bool)
hLL' : ReflTransGen Step L L'
h : Step L' L₁₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = L' → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
obtain @⟨s, e, a, b⟩ := h

Result:
case tail.not
α : Type u
L L₁₂ L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Proof state:
α : Type u
L L₁ L₂ : List (α × Bool)
⊢ Red L (L₁ ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
generalize eq : L₁ ++ L₂ = L₁₂

Result:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
⊢ Red L L₁₂ → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂