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

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

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
l₂ : Vector β n
l : Vector α (n + 1)
b : β
⊢ (∃ l₁ a, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ b = f n a) → ∃ a l₁, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b

case mpr
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
l₂ : Vector β n
l : Vector α (n + 1)
b : β
⊢ (∃ a l₁, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b) → ∃ l₁ a, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ b = f n a

Proof state:
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
l₁ : Vector α n
a : α
⊢ l₁.push a = l₁.push a ∧ mapIdx f l₁ = mapIdx f l₁ ∧ f l₁.size a = f n a

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
l₁ : Vector α n
a : α
⊢ ∃ a_1 l₁_1, l₁.push a = l₁_1.push a_1 ∧ mapIdx f l₁_1 = mapIdx f l₁ ∧ f l₁_1.size a_1 = f n a

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

Result:
no goals

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

Tactic:
rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_push_iff]

Result:
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
l₂ : Vector β n
l : Vector α (n + 1)
b : β
⊢ (∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a) = l₂ ∧ b = f n a) ↔
    ∃ a l₁, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
a : α
l₁ : Vector α n
⊢ mapIdx f l₁ = mapIdx f l₁ ∧ f l₁.size a = f n a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
l₂ : Vector β n
l : Vector α (n + 1)
b : β
⊢ (∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a) = l₂ ∧ b = f n a) ↔
    ∃ a l₁, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b

Tactic:
simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]

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

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

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

Result:
case mp.intro.intro.intro.intro
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
l₁ : Vector α n
a : α
⊢ ∃ a_1 l₁_1, l₁.push a = l₁_1.push a_1 ∧ mapIdx f l₁_1 = mapIdx f l₁ ∧ f l₁_1.size a_1 = f n a

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

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

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
a : α
l₁ : Vector α n
⊢ ∃ l₁_1 a_1, l₁.push a = l₁_1.push a_1 ∧ mapIdx f l₁_1 = mapIdx f l₁ ∧ f l₁.size a = f n a_1

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
n : Nat
β : Type u_2
f : Nat → α → β
a : α
l₁ : Vector α n
⊢ ∃ l₁_1 a_1, l₁.push a = l₁_1.push a_1 ∧ mapIdx f l₁_1 = mapIdx f l₁ ∧ f l₁.size a = f n a_1

Tactic:
exact ⟨l₁, a, rfl, by simp⟩

Result:
no goals