-- 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
α : Type u_1
xs : List (List α)
p : α → Bool
a : α
⊢ (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) →
    p a = true ∧ ∃ as bs, xs.flatten = as ++ a :: bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
rintro ⟨h, ⟨as, ys, zs, bs, rfl, h₁, h₂⟩⟩

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
⊢ 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

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₁ : ∃ 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

Tactic:
obtain ⟨bs, cs, ds, rfl, h₁, rfl⟩ := h₁

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 = []
⊢ ∃ 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

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
a : α
m : a ∈ as.flatten ++ ys
⊢ (!p a) = true

Tactic:
simp at m

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 : α
m : (∃ l, l ∈ as ∧ a ∈ l) ∨ a ∈ ys
⊢ (!p a) = true

Proof state:
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
l : List α
ml : l ∈ as
a : α
m : a ∈ l
⊢ p a = false

Tactic:
simpa using h₂ a (by simpa using .inl ⟨l, ml, m⟩)

Result:
no goals

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
⊢ ∃ as_1 ys,
    (∃ x x_1, as ++ (bs ++ c :: cs) :: ds = as_1 ++ (ys ++ a :: x) :: x_1) ∧
      (∀ (a : List α), a ∈ as_1 → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false

Tactic:
refine ⟨as, bs, ?_⟩

Result:
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

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₁ :
  (∃ 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

Tactic:
obtain (⟨as, bs, rfl, rfl, h₁⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h₁⟩) := 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 :: zs = bs.flatten
h₂ : ∀ (a : α), a ∈ as.flatten → (!p a) = true
⊢ ∃ 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

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
⊢ ∃ as_1 ys zs bs_1,
    as ++ (bs ++ c :: 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

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 = []
⊢ (∀ (a : List α), a ∈ as ++ bs → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ [] → (!p x) = true

Tactic:
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 ∨ a ∈ bs → ∀ (x : α), x ∈ a → p x = false

Proof state:
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

Tactic:
intro l ml a m

Result:
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
l : List α
ml : l ∈ as
a : α
m : a ∈ l
⊢ p a = false

Proof state:
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

Tactic:
simp_all

Result:
no goals