-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem vector₃_induction (P : Vector (Vector (Vector α n) m) k → Prop)
    (of : ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ xs ∈ xss, xs.size = m)
      (h₃ : ∀ xs ∈ xss, ∀ x ∈ xs, x.size = n),
      P (mk (xss.attach.map (fun ⟨xs, m⟩ =>
        mk (xs.attach.map (fun ⟨x, m'⟩ =>
          mk x (h₃ xs m x m'))) (by simpa using h₂ xs m))) (by simpa using h₁)))
    (ass : Vector (Vector (Vector α n) m) k) : P ass

Proof state:
α : Type u_1
n m k : Nat
P : Vector (Vector (Vector α n) m) k → Prop
of :
  ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m)
    (h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (x : Array α), x ∈ xs → x.size = n),
    P
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ =>
                {
                  toArray :=
                    Array.map
                      (fun x =>
                        match x with
                        | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                      xs.attach,
                  size_toArray := ⋯ })
            xss.attach,
        size_toArray := ⋯ }
ass : Vector (Vector (Vector α n) m) k
⊢ ∀ (xs : Array (Array α)),
    xs ∈ (map (fun as => (map toArray as).toArray) ass).toArray → ∀ (x : Array α), x ∈ xs → x.size = n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
P : Vector (Vector (Vector α n) m) k → Prop
of :
  ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m)
    (h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (x : Array α), x ∈ xs → x.size = n),
    P
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ =>
                {
                  toArray :=
                    Array.map
                      (fun x =>
                        match x with
                        | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                      xs.attach,
                  size_toArray := ⋯ })
            xss.attach,
        size_toArray := ⋯ }
ass : Vector (Vector (Vector α n) m) k
⊢ ∀ (xs : Array (Array α)), xs ∈ (map (fun as => (map toArray as).toArray) ass).toArray → xs.size = m

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.199593
n m✝ k : Nat
P : Vector (Vector (Vector α n) m✝) k → Prop
xss : Array (Array (Array α))
h₁ : xss.size = k
h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m✝
h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (x : Array α), x ∈ xs → x.size = n
x✝ : { x // x ∈ xss }
xs : Array (Array α)
m : xs ∈ xss
⊢ (Array.map
        (fun x =>
          match x with
          | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
        xs.attach).size =
    m✝

Tactic:
simpa using h₂ xs m

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
P : Vector (Vector (Vector α n) m) k → Prop
of :
  ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m)
    (h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (x : Array α), x ∈ xs → x.size = n),
    P
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ =>
                {
                  toArray :=
                    Array.map
                      (fun x =>
                        match x with
                        | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                      xs.attach,
                  size_toArray := ⋯ })
            xss.attach,
        size_toArray := ⋯ }
ass : Vector (Vector (Vector α n) m) k
⊢ (map (fun as => (map toArray as).toArray) ass).size = k

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
P : Vector (Vector (Vector α n) m) k → Prop
ass : Vector (Vector (Vector α n) m) k
of :
  P
    {
      toArray :=
        Array.map
          (fun x =>
            match x with
            | ⟨xs, m_1⟩ =>
              {
                toArray :=
                  Array.map
                    (fun x =>
                      match x with
                      | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                    xs.attach,
                size_toArray := ⋯ })
          (map (fun as => (map toArray as).toArray) ass).attach,
      size_toArray := ⋯ }
⊢ P ass

Tactic:
simpa [Array.map_attach, Array.pmap_map] using of

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
P : Vector (Vector (Vector α n) m) k → Prop
of :
  ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m)
    (h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (x : Array α), x ∈ xs → x.size = n),
    P
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ =>
                {
                  toArray :=
                    Array.map
                      (fun x =>
                        match x with
                        | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                      xs.attach,
                  size_toArray := ⋯ })
            xss.attach,
        size_toArray := ⋯ }
ass : Vector (Vector (Vector α n) m) k
⊢ P ass

Tactic:
specialize of (ass.map (fun as => (as.map toArray).toArray)).toArray (by simp) (by simp) (by simp)

Result:
α : Type u_1
n m k : Nat
P : Vector (Vector (Vector α n) m) k → Prop
ass : Vector (Vector (Vector α n) m) k
of :
  P
    {
      toArray :=
        Array.map
          (fun x =>
            match x with
            | ⟨xs, m_1⟩ =>
              {
                toArray :=
                  Array.map
                    (fun x =>
                      match x with
                      | ⟨x, m'⟩ => { toArray := x, size_toArray := ⋯ })
                    xs.attach,
                size_toArray := ⋯ })
          (map (fun as => (map toArray as).toArray) ass).attach,
      size_toArray := ⋯ }
⊢ P ass

Proof state:
α : Type ?u.199593
n m k : Nat
P : Vector (Vector (Vector α n) m) k → Prop
xss : Array (Array (Array α))
h₁ : xss.size = k
h₂ : ∀ (xs : Array (Array α)), xs ∈ xss → xs.size = m
h₃ : ∀ (xs : Array (Array α)), xs ∈ xss → ∀ (x : Array α), x ∈ xs → x.size = n
⊢ (Array.map (fun x => ?m.199732) xss.attach).size = k

Tactic:
simpa using h₁

Result:
no goals