-- 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:
α : 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] ∈ L'

Tactic:
simp

Result:
no goals

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 : L.flatten = L'.flatten
⊢ Array.map Array.size L = Array.map Array.size L'

Tactic:
ext i h h'

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
⊢ (Array.map Array.size L).size = (Array.map Array.size L').size

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]

Proof state:
case of.of.mpr
α : 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
w : Array.map Array.size L = Array.map Array.size L'
this : L = L'
⊢ Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach

Tactic:
subst this

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

Proof state:
case of.of.mpr
α : 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
w : Array.map Array.size L = Array.map Array.size L'
⊢ Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach

Tactic:
have := Array.eq_iff_flatten_eq.mpr ⟨h, w⟩

Result:
case of.of.mpr
α : 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
w : Array.map Array.size L = Array.map Array.size L'
this : L = L'
⊢ Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach

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
⊢ L[i].size = L'[i].size

Tactic:
rw [h₂ _ (by simp), h₂' _ (by simp)]

Result:
no goals

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

Tactic:
simpa [Option.map_pmap] using h

Result:
no goals

Proof state:
case of.of.mpr
α : 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
⊢ L.flatten = L'.flatten →
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
      Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach

Tactic:
intro h

Result:
case of.of.mpr
α : 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 (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach

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

Tactic:
rfl

Result:
no goals

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✝ : L.flatten = L'.flatten
i : Nat
h : i < (Array.map Array.size L).size
h' : i < (Array.map Array.size L').size
⊢ L[i] ∈ L

Tactic:
simp

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

Tactic:
suffices L = L' by simp_all

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 = L'

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

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

case of.of.mpr
α : 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
⊢ L.flatten = L'.flatten →
    Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L.attach =
      Array.map (fun x => { toArray := x.val, size_toArray := ⋯ }) L'.attach