-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a : α} :
    xs.flatten.find? p = some a ↔
      p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧
        (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x)

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
as : List (List α)
ys zs : List α
bs : List (List α)
h₁ : ∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true
h₂ : ∀ (x : α), x ∈ ys → (!p x) = true
⊢ p a = true ∧
    ∃ as_1 bs_1, (as ++ (ys ++ a :: zs) :: bs).flatten = as_1 ++ a :: bs_1 ∧ ∀ (a : α), a ∈ as_1 → (!p a) = true

Tactic:
refine ⟨h, as.flatten ++ ys, zs ++ bs.flatten, by simp, ?_⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
as : List (List α)
ys zs : List α
bs : List (List α)
h₁ : ∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true
h₂ : ∀ (x : α), x ∈ ys → (!p x) = true
⊢ ∀ (a : α), a ∈ as.flatten ++ ys → (!p a) = true

Proof state:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as bs : List (List α)
h₂ : ∀ (a : α), a ∈ as.flatten → (!p a) = true
h₁ : bs.flatten = a :: zs
⊢ ∃ as_1 ys zs bs_1,
    as ++ bs = as_1 ++ (ys ++ a :: zs) :: bs_1 ∧
      (∀ (a : List α), a ∈ as_1 → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
rw [flatten_eq_cons_iff] at h₁

Result:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as bs : List (List α)
h₂ : ∀ (a : α), a ∈ as.flatten → (!p a) = true
h₁ : ∃ as bs_1 cs, bs = as ++ (a :: bs_1) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ zs = bs_1 ++ cs.flatten
⊢ ∃ as_1 ys zs bs_1,
    as ++ bs = as_1 ++ (ys ++ a :: zs) :: bs_1 ∧
      (∀ (a : List α), a ∈ as_1 → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Proof state:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
as : List (List α)
h₂ : ∀ (a : α), a ∈ as.flatten → (!p a) = true
bs : List (List α)
cs : List α
ds : List (List α)
h₁ : ∀ (l : List α), l ∈ bs → l = []
⊢ ∃ as_1 ys zs bs_1,
    as ++ (bs ++ (a :: cs) :: ds) = as_1 ++ (ys ++ a :: zs) :: bs_1 ∧
      (∀ (a : List α), a ∈ as_1 → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
refine ⟨as ++ bs, [], cs, ds, by simp, ?_⟩

Result:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
as : List (List α)
h₂ : ∀ (a : α), a ∈ as.flatten → (!p a) = true
bs : List (List α)
cs : List α
ds : List (List α)
h₁ : ∀ (l : List α), l ∈ bs → l = []
⊢ (∀ (a : List α), a ∈ as ++ bs → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ [] → (!p x) = true

Proof state:
case mp.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : a :: zs = c :: cs ++ ds.flatten
h₂ : ∀ (a : α), a ∈ as.flatten ++ bs → (!p a) = true
x : α
m : x ∈ bs
⊢ p x = false

Tactic:
simpa using h₂ x (by simpa using .inr m)

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
xs : List (List α)
p : α → Bool
a : α
h : p a = true
ys zs : List α
h₁ : xs.flatten = ys ++ a :: zs
h₂ : ∀ (a : α), a ∈ ys → (!p a) = true
⊢ p a = true ∧
    ∃ as ys zs bs,
      xs = as ++ (ys ++ a :: zs) :: bs ∧
        (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
refine ⟨h, ?_⟩

Result:
case mp.intro.intro.intro.intro
α : Type u_1
xs : List (List α)
p : α → Bool
a : α
h : p a = true
ys zs : List α
h₁ : xs.flatten = ys ++ a :: zs
h₂ : ∀ (a : α), a ∈ ys → (!p a) = true
⊢ ∃ as ys zs bs,
    xs = as ++ (ys ++ a :: zs) :: bs ∧
      (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Proof state:
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : a :: zs = c :: cs ++ ds.flatten
h₂ : ∀ (a : α), a ∈ as.flatten ++ bs → (!p a) = true
x : α
m : x ∈ bs
⊢ x ∈ as.flatten ++ bs

Tactic:
simpa using .inr m

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a✝ : α
h : p a✝ = true
as : List (List α)
h₂ : ∀ (a : α), a ∈ as.flatten → (!p a) = true
bs : List (List α)
cs : List α
ds : List (List α)
h₁ : ∀ (l : List α), l ∈ bs → l = []
a : List α
ma : a ∈ as
x : α
m : x ∈ a
⊢ x ∈ as.flatten

Tactic:
simpa using ⟨a, ma, m⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
xs : List (List α)
p : α → Bool
a : α
h : p a = true
ys zs : List α
h₁ : xs.flatten = ys ++ a :: zs
h₂ : ∀ (a : α), a ∈ ys → (!p a) = true
⊢ ∃ as ys zs bs,
    xs = as ++ (ys ++ a :: zs) :: bs ∧
      (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
rw [flatten_eq_append_iff] at h₁

Result:
case mp.intro.intro.intro.intro
α : Type u_1
xs : List (List α)
p : α → Bool
a : α
h : p a = true
ys zs : List α
h₁ :
  (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ a :: zs = bs.flatten) ∨
    ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ a :: zs = c :: cs ++ ds.flatten
h₂ : ∀ (a : α), a ∈ ys → (!p a) = true
⊢ ∃ as ys zs bs,
    xs = as ++ (ys ++ a :: zs) :: bs ∧
      (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Proof state:
case mp.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : a :: zs = c :: cs ++ ds.flatten
h₂ : ∀ (a : α), a ∈ as.flatten ++ bs → (!p a) = true
⊢ (∃ x x_1, as ++ (bs ++ c :: cs) :: ds = as ++ (bs ++ a :: x) :: x_1) ∧
    (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ bs → p x = false

Tactic:
refine ⟨?_, ?_, ?_⟩

Result:
case mp.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : a :: zs = c :: cs ++ ds.flatten
h₂ : ∀ (a : α), a ∈ as.flatten ++ bs → (!p a) = true
⊢ ∃ x x_1, as ++ (bs ++ c :: cs) :: ds = as ++ (bs ++ a :: x) :: x_1

case mp.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : a :: zs = c :: cs ++ ds.flatten
h₂ : ∀ (a : α), a ∈ as.flatten ++ bs → (!p a) = true
⊢ ∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false

case mp.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
a : α
h : p a = true
zs : List α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h₁ : a :: zs = c :: cs ++ ds.flatten
h₂ : ∀ (a : α), a ∈ as.flatten ++ bs → (!p a) = true
⊢ ∀ (x : α), x ∈ bs → p x = false