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

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l₁ : Array α
⊢ l₁.push a = l₁.push a ∧ f l₁.size a = f ((l₁.push a).size - 1) a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l₂ : Array β
l : Array α
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
β : Type u_2
f : Nat → α → β
l₂ : Array β
l : Array α
b : β
⊢ (∃ l₁ a w, (l₁.mapFinIdx fun i a h => f i a) = l₂ ∧ b = f (l.size - 1) a) ↔
    ∃ a l₁, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l₂ : Array β
l : Array α
b : β
⊢ (∃ l₁ a w, (l₁.mapFinIdx fun i a h => f i a) = l₂ ∧ b = f (l.size - 1) 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
β : Type u_2
f : Nat → α → β
l₂ : Array β
l : Array α
b : β
⊢ (∃ l₁, mapIdx f l₁ = l₂ ∧ ∃ x, l = l₁.push x ∧ b = f (l.size - 1) x) ↔
    ∃ a l₁, l = l₁.push a ∧ mapIdx f l₁ = l₂ ∧ f l₁.size a = b

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁ : Array α
a : α
⊢ l₁.push a = l₁.push a ∧ mapIdx f l₁ = mapIdx f l₁ ∧ f l₁.size a = f ((l₁.push a).size - 1) a

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l₁ : Array α
⊢ ∃ l₁_1, mapIdx f l₁_1 = mapIdx f l₁ ∧ ∃ x, l₁.push a = l₁_1.push x ∧ f l₁.size a = f ((l₁.push a).size - 1) x

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

Result:
no goals

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

Tactic:
constructor

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

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

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

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

Result:
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁ : Array α
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 ((l₁.push a).size - 1) a

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

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

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l₁ : Array α
⊢ ∃ l₁_1, mapIdx f l₁_1 = mapIdx f l₁ ∧ ∃ x, l₁.push a = l₁_1.push x ∧ f l₁.size a = f ((l₁.push a).size - 1) x

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁ : Array α
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 ((l₁.push a).size - 1) a

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

Result:
no goals