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

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

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

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

Tactic:
obtain ⟨l, ml, m⟩ | m := m

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro.inl.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 : α
l : List α
ml : l ∈ as
m : a ∈ l
⊢ (!p a) = true

case mpr.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 ∈ ys
⊢ (!p a) = true

Proof state:
α : 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
⊢ (as ++ (ys ++ a :: zs) :: bs).flatten = as.flatten ++ ys ++ a :: (zs ++ bs.flatten)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List (List α)
p : α → Bool
a : α
⊢ find? p xs.flatten = some 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

Tactic:
rw [find?_eq_some_iff_append]

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

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
l : List α
ml : l ∈ as
a : α
m : a ∈ l
⊢ a ∈ as.flatten ++ bs

Tactic:
simpa using .inl ⟨l, ml, m⟩

Result:
no goals