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

Proof state:
case of.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
w : p a = true
as : Array (Array α)
ys zs : Array α
bs : Array (Array α)
h₁ : ∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false
h₂ : ∀ (x : α), x ∈ ys → p x = false
h :
  (fun x => List.map toList x) (List.map List.toArray xss✝).toArray.toList =
    (fun x => List.map toList x) (as.push (ys.push a ++ zs) ++ bs).toList
⊢ ∃ as ys,
    (∃ x x_1, xss✝ = as ++ (ys ++ a :: x) :: x_1) ∧
      (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false

Tactic:
simp [Function.comp_def] at h

Result:
case of.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
w : p a = true
as : Array (Array α)
ys zs : Array α
bs : Array (Array α)
h₁ : ∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false
h₂ : ∀ (x : α), x ∈ ys → p x = false
h : xss✝ = List.map toList as.toList ++ (ys.toList ++ a :: zs.toList) :: List.map toList bs.toList
⊢ ∃ as ys,
    (∃ x x_1, xss✝ = as ++ (ys ++ a :: x) :: x_1) ∧
      (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false

Proof state:
case of
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
⊢ (p a = true ∧
      ∃ as ys zs bs,
        xss✝ = 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 ys zs bs,
        (List.map List.toArray xss✝).toArray = as.push (ys.push a ++ zs) ++ bs ∧
          (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]

Result:
case of
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
⊢ p a = true →
    ((∃ as ys,
        (∃ x x_1, xss✝ = as ++ (ys ++ a :: x) :: x_1) ∧
          (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false) ↔
      ∃ as ys,
        (∃ x x_1, (List.map List.toArray xss✝).toArray = as.push (ys.push a ++ x) ++ x_1) ∧
          (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false)

Proof state:
case of.mpr
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
w : p a = true
⊢ (∃ as ys,
      (∃ x x_1, (List.map List.toArray xss✝).toArray = as.push (ys.push a ++ x) ++ x_1) ∧
        (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false) →
    ∃ as ys,
      (∃ x x_1, xss✝ = as ++ (ys ++ a :: x) :: x_1) ∧
        (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false

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

Result:
case of.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
w : p a = true
as : Array (Array α)
ys zs : Array α
bs : Array (Array α)
h : (List.map List.toArray xss✝).toArray = as.push (ys.push a ++ zs) ++ bs
h₁ : ∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false
h₂ : ∀ (x : α), x ∈ ys → p x = false
⊢ ∃ as ys,
    (∃ x x_1, xss✝ = as ++ (ys ++ a :: x) :: x_1) ∧
      (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false

Proof state:
case of
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
⊢ p a = true →
    ((∃ as ys,
        (∃ x x_1, xss✝ = as ++ (ys ++ a :: x) :: x_1) ∧
          (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false) ↔
      ∃ as ys,
        (∃ x x_1, (List.map List.toArray xss✝).toArray = as.push (ys.push a ++ x) ++ x_1) ∧
          (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false)

Tactic:
intro w

Result:
case of
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
w : p a = true
⊢ (∃ as ys,
      (∃ x x_1, xss✝ = as ++ (ys ++ a :: x) :: x_1) ∧
        (∀ (a : List α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false) ↔
    ∃ as ys,
      (∃ x x_1, (List.map List.toArray xss✝).toArray = as.push (ys.push a ++ x) ++ x_1) ∧
        (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false) ∧ ∀ (x : α), x ∈ ys → p x = false

Proof state:
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
w : p a = true
as : Array (Array α)
ys zs : Array α
bs : Array (Array α)
h₁ : ∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → p x = false
h₂ : ∀ (x : α), x ∈ ys → p x = false
h : xss✝ = List.map toList as.toList ++ (ys.toList ++ a :: zs.toList) :: List.map toList bs.toList
⊢ ∀ (a : List α), a ∈ List.map toList as.toList → ∀ (x : α), x ∈ a → p x = false

Tactic:
simpa using h₁

Result:
no goals