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

Tactic:
intro x m

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

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

Tactic:
exact h₂ a m

Result:
no goals

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

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

Proof state:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
⊢ p x = false

Tactic:
simpa using h₂ x (by simpa using ⟨a, ma, m⟩)

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 α)
a : List α
mb : a ∈ bs
x : α
m : x ∈ a
h₁ : a = []
⊢ p x = false

Tactic:
simp_all

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 = []
⊢ as ++ (bs ++ (a :: cs) :: ds) = as ++ bs ++ ([] ++ a :: cs) :: ds

Tactic:
simp

Result:
no goals

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

Tactic:
rintro ⟨h, ⟨ys, zs, h₁, 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
⊢ 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.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

Tactic:
rintro a (ma | mb) x m

Result:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
⊢ p x = false

case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 α
mb : a ∈ bs
x : α
m : x ∈ a
⊢ p x = false

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

Tactic:
replace h₁ := h₁.symm

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

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

Tactic:
exact h₁ l ml a m

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 α
mb : a ∈ bs
x : α
m : x ∈ a
⊢ p x = false

Tactic:
specialize h₁ _ mb

Result:
case mp.intro.intro.intro.intro.inl.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 α)
a : List α
mb : a ∈ bs
x : α
m : x ∈ a
h₁ : a = []
⊢ p x = false

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

Tactic:
simp [h₁]

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