-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_push_iff {f : α → β} {l : Array α} {l₂ : Array β} {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
f : α → β
l₂ : Array β
b : β
l : List α
⊢ map f { toList := l } = l₂.push b ↔ ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ map f { toList := l } = { toList := l₂ }.push b ↔
    ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b

Proof state:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ (∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [b]) →
    ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b

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

Result:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
l₁ l₂ : List α
h : List.map f l₂ = [b]
⊢ ∃ l₁_1 a, { toList := l₁ ++ l₂ } = l₁_1.push a ∧ map f l₁_1 = { toList := List.map f l₁ } ∧ f a = b

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ map f { toList := l } = { toList := l₂ }.push b ↔
    ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b

Tactic:
simp only [List.map_toArray, List.push_toArray, mk.injEq, List.map_eq_append_iff]

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ (∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [b]) ↔
    ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b

Proof state:
case mk.mk.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
a : α
⊢ ∃ l₁_1 a_1, { toList := l₁ ++ [a] } = l₁_1.push a_1 ∧ map f l₁_1 = { toList := List.map f l₁ } ∧ f a_1 = f a

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

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
a : α
⊢ { toList := l₁ ++ [a] } = l₁.toArray.push a ∧ map f l₁.toArray = { toList := List.map f l₁ } ∧ f a = f a

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
l₁ l₂ : List α
h : List.map f l₂ = [b]
⊢ ∃ l₁_1 a, { toList := l₁ ++ l₂ } = l₁_1.push a ∧ map f l₁_1 = { toList := List.map f l₁ } ∧ f a = b

Tactic:
simp only [List.map_eq_singleton_iff] at h

Result:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
l₁ l₂ : List α
h : ∃ a, l₂ = [a] ∧ f a = b
⊢ ∃ l₁_1 a, { toList := l₁ ++ l₂ } = l₁_1.push a ∧ map f l₁_1 = { toList := List.map f l₁ } ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l₂ : Array β
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⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l₂ : Array β
b : β
l : List α
⊢ map f { toList := l } = l₂.push b ↔ ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b

Proof state:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
l₁ l₂ : List α
h : ∃ a, l₂ = [a] ∧ f a = b
⊢ ∃ l₁_1 a, { toList := l₁ ++ l₂ } = l₁_1.push a ∧ map f l₁_1 = { toList := List.map f l₁ } ∧ f a = b

Tactic:
obtain ⟨a, rfl, rfl⟩ := h

Result:
case mk.mk.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ : List α
a : α
⊢ ∃ l₁_1 a_1, { toList := l₁ ++ [a] } = l₁_1.push a_1 ∧ map f l₁_1 = { toList := List.map f l₁ } ∧ f a_1 = f a

Proof state:
case mk.mk.mpr.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l : List α
l₂ : List β
l₁ : List α
a : α
h₁ : { toList := l } = { toList := l₁ }.push a
h₂ : map f { toList := l₁ } = { toList := l₂ }
⊢ ∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [f a]

Tactic:
refine ⟨l₁, [a], by simp_all⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
l₂ : List β
l₁ : List α
a : α
h₁ : { toList := l } = { toList := l₁ }.push a
h₂ : map f { toList := l₁ } = { toList := l₂ }
⊢ l = l₁ ++ [a] ∧ List.map f l₁ = l₂ ∧ List.map f [a] = [f a]

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ (∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b) →
    ∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [b]

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

Result:
case mk.mk.mpr.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l : List α
l₂ : List β
l₁ : List α
a : α
h₁ : { toList := l } = { toList := l₁ }.push a
h₂ : map f { toList := l₁ } = { toList := l₂ }
⊢ ∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [f a]

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ (∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [b]) ↔
    ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b

Tactic:
constructor

Result:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ (∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [b]) →
    ∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b

case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
l₂ : List β
⊢ (∃ l₁ a, { toList := l } = l₁.push a ∧ map f l₁ = { toList := l₂ } ∧ f a = b) →
    ∃ l₁ l₂_1, l = l₁ ++ l₂_1 ∧ List.map f l₁ = l₂ ∧ List.map f l₂_1 = [b]