-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem getElem_zero_flatten.proof {L : Vector (Vector α m) n} (h : 0 < n * m) :
    (L.findSome? fun l => l[0]?).isSome

Proof state:
case of
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
⊢ (findSome? (fun l => l[0]?)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }).isSome =
    true

Tactic:
have hn : 0 < n := Nat.pos_of_mul_pos_right h

Result:
case of
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
⊢ (findSome? (fun l => l[0]?)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }).isSome =
    true

Proof state:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
h : 0 < n * m
⊢ (findSome? (fun l => l[0]?) L).isSome = true

Tactic:
cases L using vector₂_induction with
| of xss h₁ h₂ =>
  have hn : 0 < n := Nat.pos_of_mul_pos_right h
  have hm : 0 < m := Nat.pos_of_mul_pos_left h
  simp only [hm, getElem?_eq_getElem, findSome?_mk, Array.findSome?_isSome_iff, Array.mem_map,
    Array.mem_attach, mk_eq, true_and, Subtype.exists, exists_prop, exists_eq_right,
    Option.isSome_some, and_true]
  exact ⟨⟨xss[0], h₂ _ (by simp)⟩, by simp⟩

Result:
no goals

Proof state:
case of
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
hm : 0 < m
⊢ ∃ x, x.toArray ∈ xss

Tactic:
exact ⟨⟨xss[0], h₂ _ (by simp)⟩, by simp⟩

Result:
no goals

Proof state:
case of
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
hm : 0 < m
⊢ (findSome? (fun l => l[0]?)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }).isSome =
    true

Tactic:
simp only [hm, getElem?_eq_getElem, findSome?_mk, Array.findSome?_isSome_iff, Array.mem_map,
  Array.mem_attach, mk_eq, true_and, Subtype.exists, exists_prop, exists_eq_right,
  Option.isSome_some, and_true]

Result:
case of
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
hm : 0 < m
⊢ ∃ x, x.toArray ∈ xss

Proof state:
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
hm : 0 < m
⊢ { toArray := xss[0], size_toArray := ⋯ }.toArray ∈ xss

Tactic:
simp

Result:
no goals

Proof state:
case of
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
⊢ (findSome? (fun l => l[0]?)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }).isSome =
    true

Tactic:
have hm : 0 < m := Nat.pos_of_mul_pos_left h

Result:
case of
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
hm : 0 < m
⊢ (findSome? (fun l => l[0]?)
        {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss.attach,
          size_toArray := ⋯ }).isSome =
    true

Proof state:
α : Type u_1
m n : Nat
h : 0 < n * m
xss : Array (Array α)
h₁ : xss.size = n
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = m
hn : 0 < n
hm : 0 < m
⊢ xss[0] ∈ xss

Tactic:
simp

Result:
no goals