-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_append_iff {f : α → β} :
    map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ map f { toArray := l, size_toArray := h } =
      { toArray := L₁, size_toArray := ⋯ } ++ { toArray := L₂, size_toArray := ⋯ } ↔
    ∃ l₁ l₂,
      { toArray := l, size_toArray := h } = l₁ ++ l₂ ∧
        map f l₁ = { toArray := L₁, size_toArray := ⋯ } ∧ map f l₂ = { toArray := L₂, size_toArray := ⋯ }

Tactic:
simp only [map_mk, mk_append_mk, eq_mk, Array.map_eq_append_iff, mk_eq, toArray_append,
  toArray_map]

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ Array.map f l₁ = L₁ ∧ Array.map f l₂ = L₂) ↔
    ∃ l₁ l₂, l = l₁.toArray ++ l₂.toArray ∧ Array.map f l₁.toArray = L₁ ∧ Array.map f l₂.toArray = L₂

Proof state:
case mk
α : Type u_1
β : Type u_2
a✝¹ a✝ : Nat
L₁ : Vector β a✝¹
L₂ : Vector β a✝
f : α → β
l : Array α
h : l.size = a✝¹ + a✝
⊢ map f { toArray := l, size_toArray := h } = L₁ ++ L₂ ↔
    ∃ l₁ l₂, { toArray := l, size_toArray := h } = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Tactic:
rcases L₁ with ⟨L₁, rfl⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
a✝ : Nat
L₂ : Vector β a✝
f : α → β
l : Array α
L₁ : Array β
h : l.size = L₁.size + a✝
⊢ map f { toArray := l, size_toArray := h } = { toArray := L₁, size_toArray := ⋯ } ++ L₂ ↔
    ∃ l₁ l₂,
      { toArray := l, size_toArray := h } = l₁ ++ l₂ ∧ map f l₁ = { toArray := L₁, size_toArray := ⋯ } ∧ map f l₂ = L₂

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ Array.map f l₁ = L₁ ∧ Array.map f l₂ = L₂) ↔
    ∃ l₁ l₂, l = l₁.toArray ++ l₂.toArray ∧ Array.map f l₁.toArray = L₁ ∧ Array.map f l₂.toArray = L₂

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ Array.map f l₁ = L₁ ∧ Array.map f l₂ = L₂) →
    ∃ l₁ l₂, l = l₁.toArray ++ l₂.toArray ∧ Array.map f l₁.toArray = L₁ ∧ Array.map f l₂.toArray = L₂

case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ (∃ l₁ l₂, l = l₁.toArray ++ l₂.toArray ∧ Array.map f l₁.toArray = L₁ ∧ Array.map f l₂.toArray = L₂) →
    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ Array.map f l₁ = L₁ ∧ Array.map f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
h : (l₁ ++ l₂).size = (Array.map f l₁).size + (Array.map f l₂).size
⊢ l₂.size = (Array.map f l₂).size

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
a✝ : Nat
L₂ : Vector β a✝
f : α → β
l : Array α
L₁ : Array β
h : l.size = L₁.size + a✝
⊢ map f { toArray := l, size_toArray := h } = { toArray := L₁, size_toArray := ⋯ } ++ L₂ ↔
    ∃ l₁ l₂,
      { toArray := l, size_toArray := h } = l₁ ++ l₂ ∧ map f l₁ = { toArray := L₁, size_toArray := ⋯ } ∧ map f l₂ = L₂

Tactic:
rcases L₂ with ⟨L₂, rfl⟩

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ map f { toArray := l, size_toArray := h } =
      { toArray := L₁, size_toArray := ⋯ } ++ { toArray := L₂, size_toArray := ⋯ } ↔
    ∃ l₁ l₂,
      { toArray := l, size_toArray := h } = l₁ ++ l₂ ∧
        map f l₁ = { toArray := L₁, size_toArray := ⋯ } ∧ map f l₂ = { toArray := L₂, size_toArray := ⋯ }

Proof state:
α : Type u_1
β : Type u_2
a✝¹ a✝ : Nat
l : Vector α (a✝¹ + a✝)
L₁ : Vector β a✝¹
L₂ : Vector β a✝
f : α → β
⊢ map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Tactic:
rcases l with ⟨l, h⟩

Result:
case mk
α : Type u_1
β : Type u_2
a✝¹ a✝ : Nat
L₁ : Vector β a✝¹
L₂ : Vector β a✝
f : α → β
l : Array α
h : l.size = a✝¹ + a✝
⊢ map f { toArray := l, size_toArray := h } = L₁ ++ L₂ ↔
    ∃ l₁ l₂, { toArray := l, size_toArray := h } = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ (∃ l₁ l₂, l = l₁.toArray ++ l₂.toArray ∧ Array.map f l₁.toArray = L₁ ∧ Array.map f l₂.toArray = L₂) →
    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ Array.map f l₁ = L₁ ∧ Array.map f l₂ = L₂

Tactic:
rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
L₁ L₂ : Array β
l₁ : Array α
size_toArray✝¹ : l₁.size = L₁.size
l₂ : Array α
size_toArray✝ : l₂.size = L₂.size
h :
  ({ toArray := l₁, size_toArray := size_toArray✝¹ }.toArray ++
        { toArray := l₂, size_toArray := size_toArray✝ }.toArray).size =
    L₁.size + L₂.size
h₁ : Array.map f { toArray := l₁, size_toArray := size_toArray✝¹ }.toArray = L₁
h₂ : Array.map f { toArray := l₂, size_toArray := size_toArray✝ }.toArray = L₂
⊢ ∃ l₁_1 l₂_1,
    { toArray := l₁, size_toArray := size_toArray✝¹ }.toArray ++
          { toArray := l₂, size_toArray := size_toArray✝ }.toArray =
        l₁_1 ++ l₂_1 ∧
      Array.map f l₁_1 = L₁ ∧ Array.map f l₂_1 = L₂

Proof state:
α : Type u_1
β : Type u_2
f : α → β
L₁ L₂ : Array β
l₁ : Array α
size_toArray✝¹ : l₁.size = L₁.size
l₂ : Array α
size_toArray✝ : l₂.size = L₂.size
h :
  ({ toArray := l₁, size_toArray := size_toArray✝¹ }.toArray ++
        { toArray := l₂, size_toArray := size_toArray✝ }.toArray).size =
    L₁.size + L₂.size
h₁ : Array.map f { toArray := l₁, size_toArray := size_toArray✝¹ }.toArray = L₁
h₂ : Array.map f { toArray := l₂, size_toArray := size_toArray✝ }.toArray = L₂
⊢ { toArray := l₁, size_toArray := size_toArray✝¹ }.toArray ++
        { toArray := l₂, size_toArray := size_toArray✝ }.toArray =
      l₁ ++ l₂ ∧
    Array.map f l₁ = L₁ ∧ Array.map f l₂ = L₂

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
h : (l₁ ++ l₂).size = (Array.map f l₁).size + (Array.map f l₂).size
⊢ l₁ ++ l₂ = (Vector.cast ⋯ l₁.toVector).toArray ++ (Vector.cast ⋯ l₂.toVector).toArray ∧
    Array.map f (Vector.cast ⋯ l₁.toVector).toArray = Array.map f l₁ ∧
      Array.map f (Vector.cast ⋯ l₂.toVector).toArray = Array.map f l₂

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
L₁ L₂ : Array β
l₁ : Array α
size_toArray✝¹ : l₁.size = L₁.size
l₂ : Array α
size_toArray✝ : l₂.size = L₂.size
h :
  ({ toArray := l₁, size_toArray := size_toArray✝¹ }.toArray ++
        { toArray := l₂, size_toArray := size_toArray✝ }.toArray).size =
    L₁.size + L₂.size
h₁ : Array.map f { toArray := l₁, size_toArray := size_toArray✝¹ }.toArray = L₁
h₂ : Array.map f { toArray := l₂, size_toArray := size_toArray✝ }.toArray = L₂
⊢ ∃ l₁_1 l₂_1,
    { toArray := l₁, size_toArray := size_toArray✝¹ }.toArray ++
          { toArray := l₂, size_toArray := size_toArray✝ }.toArray =
        l₁_1 ++ l₂_1 ∧
      Array.map f l₁_1 = L₁ ∧ Array.map f l₂_1 = L₂

Tactic:
exact ⟨l₁, l₂, by simp_all⟩

Result:
no goals

Proof state:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
h : (l₁ ++ l₂).size = (Array.map f l₁).size + (Array.map f l₂).size
⊢ ∃ l₁_1 l₂_1,
    l₁ ++ l₂ = l₁_1.toArray ++ l₂_1.toArray ∧
      Array.map f l₁_1.toArray = Array.map f l₁ ∧ Array.map f l₂_1.toArray = Array.map f l₂

Tactic:
exact ⟨l₁.toVector.cast (by simp), l₂.toVector.cast (by simp), by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
h : (l₁ ++ l₂).size = (Array.map f l₁).size + (Array.map f l₂).size
⊢ l₁.size = (Array.map f l₁).size

Tactic:
simp

Result:
no goals