-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_eq_concat_iff (l : List (Option α)) (l' : List α) (a : α) :
    l.reduceOption = l'.concat a ↔
      ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Proof state:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
obtain ⟨l₁, _, h, hl₁, hl₂⟩ := h

Result:
case mp.intro.intro.intro.intro
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
hl₂ : w✝.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Proof state:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
use l₁ ++ replicate m none, replicate n none

Result:
case h
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ (replicate n none).reduceOption = []

Proof state:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
intro h

Result:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : l.reduceOption = l' ++ [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Proof state:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ l.reduceOption = l' ++ [a]

Tactic:
rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]

Result:
no goals

Proof state:
case h
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ (replicate n none).reduceOption = []

Tactic:
simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
  hl₂, and_self]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
hl₂ : w✝.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
rw [reduceOption_eq_singleton_iff] at hl₂

Result:
case mp.intro.intro.intro.intro
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
hl₂ : ∃ m n, w✝ = replicate m none ++ some a :: replicate n none
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Proof state:
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
constructor

Result:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] → ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
hl₂ : ∃ m n, w✝ = replicate m none ++ some a :: replicate n none
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
obtain ⟨m, n, hl₂⟩ := hl₂

Result:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Proof state:
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l'.concat a ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
rw [concat_eq_append]

Result:
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Proof state:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ (∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) → l.reduceOption = l' ++ [a]

Tactic:
intro ⟨_, _, h, hl₁, hl₂⟩

Result:
case mpr
α : Type u_1
l : List (Option α)
l' : List α
a : α
w✝¹ w✝ : List (Option α)
h : l = w✝¹ ++ some a :: w✝
hl₁ : w✝¹.reduceOption = l'
hl₂ : w✝.reduceOption = []
⊢ l.reduceOption = l' ++ [a]

Proof state:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : l.reduceOption = l' ++ [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
rw [reduceOption_eq_append_iff] at h

Result:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []