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

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

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

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

Proof state:
α : Type ?u.94605
β : Type ?u.94629
l₂ : Array β
l : Array α
b : β
f : (i : Nat) → α → i < l.size → β
l₁ : Array α
a : α
w : l = l₁.push a
⊢ l.size - 1 < l.size

Tactic:
simp [w]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁ : Array α
a : α
f : (i : Nat) → α → i < (l₁.push a).size → β
⊢ ∃ l₁' l₂' w,
    ((l₁'.mapFinIdx fun i a_1 h => f i a_1 ⋯) = l₁.mapFinIdx fun i a_1 h => f i a_1 ⋯) ∧
      (l₂'.mapFinIdx fun i a_1 h => f (i + l₁'.size) a_1 ⋯) = #[f ((l₁.push a).size - 1) a ⋯]

Tactic:
exact ⟨l₁, #[a], by simp⟩

Result:
no goals

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

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

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

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

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.94605
β : Type ?u.94629
l₂ : Array β
l : Array α
b : β
f : (i : Nat) → α → i < l.size → β
l₁ : Array α
a✝ : α
w : l = l₁.push a✝
i : Nat
a : α
h : i < l₁.size
⊢ i < l.size

Tactic:
simp [w]

Result:
α : Type ?u.94605
β : Type ?u.94629
l₂ : Array β
l : Array α
b : β
f : (i : Nat) → α → i < l.size → β
l₁ : Array α
a✝ : α
w : l = l₁.push a✝
i : Nat
a : α
h : i < l₁.size
⊢ i < l₁.size + 1

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
a : α
f : (i : Nat) → α → i < (l₁ ++ #[a]).size → β
⊢ ∃ w,
    ((l₁.mapFinIdx fun i a_1 h => f i a_1 ⋯) = l₁.mapFinIdx fun i a_1 h => f i a_1 ⋯) ∧
      f l₁.size a ⋯ = f ((l₁ ++ #[a]).size - 1) a ⋯

Tactic:
simp

Result:
no goals

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

Tactic:
constructor

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

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

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

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

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

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

Tactic:
rw [push_eq_append, mapFinIdx_eq_append_iff]

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

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

Tactic:
simp only [mapFinIdx_eq_singleton_iff, Nat.zero_add] at h₂

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

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

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

Result:
no goals

Proof state:
α : Type ?u.94605
β : Type ?u.94629
l₂ : Array β
l : Array α
b : β
f : (i : Nat) → α → i < l.size → β
l₁ : Array α
a✝ : α
w : l = l₁.push a✝
i : Nat
a : α
h : i < l₁.size
⊢ i < l₁.size + 1

Tactic:
omega

Result:
no goals