-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_iff_flatten_eq {L L' : Vector (Vector α n) m} :
    L = L' ↔ L.flatten = L'.flatten

Proof state:
case of.of.mp.h
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h :
  Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach
i : Nat
⊢ L[i]? = L'[i]?

Tactic:
replace h := congrArg (fun x => x[i]?.map (fun x => x.toArray)) h

Result:
case of.of.mp.h
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
i : Nat
h :
  (fun x => Option.map (fun x => x.toArray) x[i]?)
      (Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach) =
    (fun x => Option.map (fun x => x.toArray) x[i]?)
      (Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach)
⊢ L[i]? = L'[i]?

Proof state:
case of.of.mp
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h :
  Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach
⊢ L = L'

Tactic:
apply Array.ext_getElem?

Result:
case of.of.mp.h
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h :
  Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach
⊢ ∀ (i : Nat), L[i]? = L'[i]?

Proof state:
case of.of
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
⊢ {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
            L.attach,
        size_toArray := ⋯ } =
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
            L'.attach,
        size_toArray := ⋯ } ↔
    {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              L.attach,
          size_toArray := ⋯ }.flatten =
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
              L'.attach,
          size_toArray := ⋯ }.flatten

Tactic:
simp only [eq_mk, flatten_mk, Array.map_map, Function.comp_apply, Array.map_subtype,
  Array.unattach_attach, Array.map_id_fun', id_eq]

Result:
case of.of
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
⊢ Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
      Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach ↔
    L.flatten = L'.flatten

Proof state:
case h₁
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h : L.flatten = L'.flatten
⊢ (Array.map Array.size L).size = (Array.map Array.size L').size

Tactic:
simp_all

Result:
no goals

Proof state:
case h₂
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h✝ : L.flatten = L'.flatten
i : Nat
h : i < (Array.map Array.size L).size
h' : i < (Array.map Array.size L').size
⊢ (Array.map Array.size L)[i] = (Array.map Array.size L')[i]

Tactic:
simp only [Array.getElem_map]

Result:
case h₂
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h✝ : L.flatten = L'.flatten
i : Nat
h : i < (Array.map Array.size L).size
h' : i < (Array.map Array.size L').size
⊢ L[i].size = L'[i].size

Proof state:
case of.of.mp.h
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h :
  Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach
⊢ ∀ (i : Nat), L[i]? = L'[i]?

Tactic:
intro i

Result:
case of.of.mp.h
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h :
  Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach
i : Nat
⊢ L[i]? = L'[i]?

Proof state:
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h :
  Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach
this : L = L'
⊢ L.flatten = L'.flatten

Tactic:
simp_all

Result:
no goals

Proof state:
case of.of.mp
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
⊢ Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
      Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach →
    L.flatten = L'.flatten

Tactic:
intro h

Result:
case of.of.mp
α : Type u_1
n m : Nat
L : Array (Array α)
h₁ : L.size = m
h₂ : ∀ (xs : Array α), xs ∈ L → xs.size = n
L' : Array (Array α)
h₁' : L'.size = m
h₂' : ∀ (xs : Array α), xs ∈ L' → xs.size = n
h :
  Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach
⊢ L.flatten = L'.flatten