-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_eq_singleton_iff (l : List (Option α)) (a : α) :
    l.reduceOption = [a] ↔ ∃ m n, l = replicate m none ++ some a :: replicate n none

Proof state:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

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

Result:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none

Proof state:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
apply eq_replicate_of_mem at hl₁

Result:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Proof state:
case mp
α : Type u_1
l : List (Option α)
a : α
h : ∃ l₁ a_1 l₂, l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

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

Result:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : filterMap id l₂ = []
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Proof state:
case mp
α : Type u_1
l : List (Option α)
a : α
h : filterMap id l = [a]
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
rw [filterMap_eq_cons_iff] at h

Result:
case mp
α : Type u_1
l : List (Option α)
a : α
h : ∃ l₁ a_1 l₂, l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Proof state:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
apply eq_replicate_of_mem at hl₂

Result:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Proof state:
case mpr
α : Type u_1
l : List (Option α)
a : α
w✝¹ w✝ : ℕ
h : l = replicate w✝¹ none ++ some a :: replicate w✝ none
⊢ filterMap id l = [a]

Tactic:
simp only [h, filterMap_append, filterMap_cons_some, filterMap_replicate_of_none, id_eq,
  nil_append, Option.some.injEq]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : filterMap id l₂ = []
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
rw [filterMap_eq_nil_iff] at hl₂

Result:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Proof state:
case mp.intro.intro.intro.intro.intro.intro.refl
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ m n, replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none

Tactic:
use l₁.length, l₂.length

Result:
no goals

Proof state:
case mpr
α : Type u_1
l : List (Option α)
a : α
⊢ (∃ m n, l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]

Tactic:
intro ⟨_, _, h⟩

Result:
case mpr
α : Type u_1
l : List (Option α)
a : α
w✝¹ w✝ : ℕ
h : l = replicate w✝¹ none ++ some a :: replicate w✝ none
⊢ filterMap id l = [a]

Proof state:
α : Type u_1
l : List (Option α)
a : α
⊢ filterMap id l = [a] ↔ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
constructor

Result:
case mp
α : Type u_1
l : List (Option α)
a : α
⊢ filterMap id l = [a] → ∃ m n, l = replicate m none ++ some a :: replicate n none

case mpr
α : Type u_1
l : List (Option α)
a : α
⊢ (∃ m n, l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]

Proof state:
case mp
α : Type u_1
l : List (Option α)
a : α
⊢ filterMap id l = [a] → ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
intro h

Result:
case mp
α : Type u_1
l : List (Option α)
a : α
h : filterMap id l = [a]
⊢ ∃ m n, l = replicate m none ++ some a :: replicate n none

Proof state:
α : Type u_1
l : List (Option α)
a : α
⊢ l.reduceOption = [a] ↔ ∃ m n, l = replicate m none ++ some a :: replicate n none

Tactic:
dsimp [reduceOption]

Result:
α : Type u_1
l : List (Option α)
a : α
⊢ filterMap id l = [a] ↔ ∃ m n, l = replicate m none ++ some a :: replicate n none