-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_push_iff {f : α → β} {l : Vector α (n + 1)} {l₂ : Vector β n} {b : β} :
    map f l = l₂.push b ↔ ∃ l₁ a, l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b

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

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

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

Proof state:
case mk.mk.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l₂ : Array β
h : l.size = l₂.size + 1
l₁ : Vector α l₂.size
a : α
h₁ : { toArray := l, size_toArray := h } = l₁.push a
h₂ : map f l₁ = { toArray := l₂, size_toArray := ⋯ }
⊢ ∃ l₁ a_1, l = l₁.push a_1 ∧ Array.map f l₁ = l₂ ∧ f a_1 = f a

Tactic:
refine ⟨l₁.toArray, a, by simp_all⟩

Result:
no goals

Proof state:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
b : β
l : Array α
l₂ : Array β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a, l = l₁.push a ∧ Array.map f l₁ = l₂ ∧ f a = b) →
    ∃ l₁ a, { toArray := l, size_toArray := h } = l₁.push a ∧ map f l₁ = { toArray := l₂, size_toArray := ⋯ } ∧ f a = b

Tactic:
rintro ⟨l₁, a, rfl, rfl, rfl⟩

Result:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ : Array α
a : α
h : (l₁.push a).size = (Array.map f l₁).size + 1
⊢ ∃ l₁_1 a_1,
    { toArray := l₁.push a, size_toArray := h } = l₁_1.push a_1 ∧
      map f l₁_1 = { toArray := Array.map f l₁, size_toArray := ⋯ } ∧ f a_1 = f a

Proof state:
case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
l : Array α
l₂ : Array β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a,
      { toArray := l, size_toArray := h } = l₁.push a ∧ map f l₁ = { toArray := l₂, size_toArray := ⋯ } ∧ f a = b) →
    ∃ l₁ a, l = l₁.push a ∧ Array.map f l₁ = l₂ ∧ f a = b

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

Result:
case mk.mk.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l₂ : Array β
h : l.size = l₂.size + 1
l₁ : Vector α l₂.size
a : α
h₁ : { toArray := l, size_toArray := h } = l₁.push a
h₂ : map f l₁ = { toArray := l₂, size_toArray := ⋯ }
⊢ ∃ l₁ a_1, l = l₁.push a_1 ∧ Array.map f l₁ = l₂ ∧ f a_1 = f a

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l₂ : Array β
h : l.size = l₂.size + 1
l₁ : Vector α l₂.size
a : α
h₁ : { toArray := l, size_toArray := h } = l₁.push a
h₂ : map f l₁ = { toArray := l₂, size_toArray := ⋯ }
⊢ l = l₁.push a ∧ Array.map f l₁.toArray = l₂ ∧ f a = f a

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ : Array α
a : α
h : (l₁.push a).size = (Array.map f l₁).size + 1
⊢ ∃ l₁_1 a_1,
    { toArray := l₁.push a, size_toArray := h } = l₁_1.push a_1 ∧
      map f l₁_1 = { toArray := Array.map f l₁, size_toArray := ⋯ } ∧ f a_1 = f a

Tactic:
refine ⟨⟨l₁, by simp⟩, a, by simp⟩

Result:
no goals

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

Tactic:
constructor

Result:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
b : β
l : Array α
l₂ : Array β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a, l = l₁.push a ∧ Array.map f l₁ = l₂ ∧ f a = b) →
    ∃ l₁ a, { toArray := l, size_toArray := h } = l₁.push a ∧ map f l₁ = { toArray := l₂, size_toArray := ⋯ } ∧ f a = b

case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
l : Array α
l₂ : Array β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a,
      { toArray := l, size_toArray := h } = l₁.push a ∧ map f l₁ = { toArray := l₂, size_toArray := ⋯ } ∧ f a = b) →
    ∃ l₁ a, l = l₁.push a ∧ Array.map f l₁ = l₂ ∧ f a = b

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

Tactic:
simp only [map_mk, push_mk, mk.injEq, Array.map_eq_push_iff]

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

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Array α
a : α
h : (l₁.push a).size = (Array.map f l₁).size + 1
⊢ { toArray := l₁.push a, size_toArray := h } = { toArray := l₁, size_toArray := ⋯ }.push a ∧
    map f { toArray := l₁, size_toArray := ⋯ } = { toArray := Array.map f l₁, size_toArray := ⋯ } ∧ f a = f a

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α (n + 1)
l₂ : Vector β n
b : β
⊢ map f l = l₂.push b ↔ ∃ l₁ a, l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b

Tactic:
rcases l with ⟨l, h⟩

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