-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_push_iff {l : Vector α (n + 1)} {b : β} {f : (i : Nat) → α → (h : i < n + 1) → β} {l₂ : Vector β n} :
    l.mapFinIdx f = l₂.push b ↔
      ∃ (l₁ : Vector α n) (a : α), l = l₁.push a ∧
        l₁.mapFinIdx (fun i a h => f i a (by omega)) = l₂ ∧ b = f n a (by omega)

Proof state:
α : Type ?u.53687
n : Nat
β : Type ?u.53779
l : Vector α (n + 1)
b : β
f : (i : Nat) → α → i < n + 1 → β
l₂ : Vector β n
l₁ : Vector α n
a✝ : α
i : Nat
a : α
h : i < n
⊢ i < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.mp
α : Type u_1
β : Type u_2
b : β
l : Array α
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a w, (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂ ∧ b = f (l.size - 1) a ⋯) →
    ∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ b = f l₂.size a ⋯

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

Result:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
a : α
h : (l₁.push a).size = l₂.size + 1
h₁ : (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂
⊢ ∃ l₁_1 a_1,
    l₁.push a = l₁_1.push a_1 ∧
      (l₁_1.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ f ((l₁.push a).size - 1) a ⋯ = f l₂.size a_1 ⋯

Proof state:
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
a : α
h✝ : (l₁.push a).size = l₂.size + 1
h₁ : (l₁.mapFinIdx fun i a_1 h => f i a_1 ⋯) = l₂
h : l₁.size = l₂.size
⊢ l₁.push a = { toArray := l₁, size_toArray := h }.push a ∧
    ({ toArray := l₁, size_toArray := h }.mapFinIdx fun i a h_1 => f i a ⋯) = l₂ ∧
      f ((l₁.push a).size - 1) a ⋯ = f l₂.size a ⋯

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk.mpr.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
h✝ : l₁.size = l₂.size
a : α
h : ({ toArray := l₁, size_toArray := h✝ }.push a).size = l₂.size + 1
h₁ : ({ toArray := l₁, size_toArray := h✝ }.mapFinIdx fun i a h => f i a ⋯) = l₂
⊢ ∃ l₁_1 a_1 w,
    (l₁_1.mapFinIdx fun i a_2 h_1 => f i a_2 ⋯) = l₂ ∧
      f l₂.size a ⋯ = f (({ toArray := l₁, size_toArray := h✝ }.push a).size - 1) a_1 ⋯

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

Result:
no goals

Proof state:
α : Type ?u.53687
n : Nat
β : Type ?u.53779
l : Vector α (n + 1)
b : β
f : (i : Nat) → α → i < n + 1 → β
l₂ : Vector β n
l₁ : Vector α n
a : α
⊢ n < n + 1

Tactic:
omega

Result:
no goals

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

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

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

Proof state:
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
h✝ : l₁.size = l₂.size
a : α
h : ({ toArray := l₁, size_toArray := h✝ }.push a).size = l₂.size + 1
h₁ : ({ toArray := l₁, size_toArray := h✝ }.mapFinIdx fun i a h => f i a ⋯) = l₂
⊢ ∃ w,
    (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂ ∧
      f l₂.size a ⋯ = f (({ toArray := l₁, size_toArray := h✝ }.push a).size - 1) a ⋯

Tactic:
simp_all

Result:
no goals

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

Tactic:
rcases l with ⟨l, h⟩

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

Proof state:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
a : α
h : (l₁.push a).size = l₂.size + 1
h₁ : (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂
⊢ ∃ l₁_1 a_1,
    l₁.push a = l₁_1.push a_1 ∧
      (l₁_1.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ f ((l₁.push a).size - 1) a ⋯ = f l₂.size a_1 ⋯

Tactic:
simp only [Array.size_push, Nat.add_right_cancel_iff] at h

Result:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
a : α
h✝ : (l₁.push a).size = l₂.size + 1
h₁ : (l₁.mapFinIdx fun i a_1 h => f i a_1 ⋯) = l₂
h : l₁.size = l₂.size
⊢ ∃ l₁_1 a_1,
    l₁.push a = l₁_1.push a_1 ∧
      (l₁_1.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ f ((l₁.push a).size - 1) a ⋯ = f l₂.size a_1 ⋯

Proof state:
case mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
a : α
h✝ : (l₁.push a).size = l₂.size + 1
h₁ : (l₁.mapFinIdx fun i a_1 h => f i a_1 ⋯) = l₂
h : l₁.size = l₂.size
⊢ ∃ l₁_1 a_1,
    l₁.push a = l₁_1.push a_1 ∧
      (l₁_1.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ f ((l₁.push a).size - 1) a ⋯ = f l₂.size a_1 ⋯

Tactic:
exact ⟨⟨l₁, h⟩, a, by simp_all⟩

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
b : β
l : Array α
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a w, (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂ ∧ b = f (l.size - 1) a ⋯) ↔
    ∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ b = f l₂.size a ⋯

Tactic:
constructor

Result:
case mk.mk.mp
α : Type u_1
β : Type u_2
b : β
l : Array α
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a w, (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂ ∧ b = f (l.size - 1) a ⋯) →
    ∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ b = f l₂.size a ⋯

case mk.mk.mpr
α : Type u_1
β : Type u_2
b : β
l : Array α
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ b = f l₂.size a ⋯) →
    ∃ l₁ a w, (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂ ∧ b = f (l.size - 1) a ⋯

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

Tactic:
simp only [mapFinIdx_mk, push_mk, eq_mk, Array.mapFinIdx_eq_push_iff, mk_eq, toArray_push,
  toArray_mapFinIdx]

Result:
case mk.mk
α : Type u_1
β : Type u_2
b : β
l : Array α
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a w, (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂ ∧ b = f (l.size - 1) a ⋯) ↔
    ∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ b = f l₂.size a ⋯