-- 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:
α : Type u_1
xs : Array (Array α)
p : α → Bool
a : α
⊢ find? p xs.flatten = some a ↔
    p a = true ∧
      ∃ as ys zs bs,
        xs = as.push (ys.push a ++ zs) ++ bs ∧
          (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
cases xs using array₂_induction

Result:
case of
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
⊢ find? p (List.map List.toArray xss✝).toArray.flatten = some a ↔
    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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simpa using h₂

Result:
no goals

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

Tactic:
exact ⟨as.toList.map Array.toList, ys.toList,
  ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
    by simpa using h₁, by simpa using h₂⟩

Result:
no goals

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
⊢ xss✝ = List.map toList as.toList ++ (ys.toList ++ a :: zs.toList) :: List.map toList bs.toList

Tactic:
simpa using h

Result:
no goals

Proof state:
case of
α : Type u_1
p : α → Bool
a : α
xss✝ : List (List α)
⊢ find? p (List.map List.toArray xss✝).toArray.flatten = some a ↔
    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 [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some_iff]

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

Proof state:
case of.mp
α : 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

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

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

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

Tactic:
constructor

Result:
case of.mp
α : 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

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

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
⊢ ∀ (x : α), x ∈ ys.toList → p x = false

Tactic:
simpa using h₂

Result:
no goals

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

Tactic:
exact ⟨as.toArray.map List.toArray, ys.toArray,
  ⟨zs.toArray, bs.toArray.map List.toArray, by simp⟩, by simpa using h₁, by simpa using h₂⟩

Result:
no goals

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

Tactic:
simpa using h₁

Result:
no goals