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

Proof state:
α : Type u_1
β : Type u_2
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l'.mapFinIdx fun i a h => f (i + 1) a ⋯

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
l₂ : List β
b : β
f : (i : Nat) → α → i < [].length → β
⊢ [].mapFinIdx f = b :: l₂ ↔ ∃ a l₁ w, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h => f (i + 1) a_1 ⋯) = l₂

Tactic:
simp

Result:
no goals

Proof state:
case cons.mp.intro
α : Type u_1
β : Type u_2
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ ∃ a l₁ h,
    f 0 a ⋯ = f 0 x ⋯ ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l'.mapFinIdx fun i a h => f (i + 1) a ⋯

Tactic:
refine ⟨x, l', ⟨rfl, rfl⟩, by simp⟩

Result:
no goals

Proof state:
case cons.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ f 0 x ⋯ = f 0 x ⋯ ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l'.mapFinIdx fun i a h => f (i + 1) a ⋯

Tactic:
exact ⟨rfl, by simp⟩

Result:
no goals

Proof state:
case cons.mp
α : Type u_1
β : Type u_2
l₂ : List β
b : β
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ f 0 x ⋯ = b ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l₂ →
    ∃ a l₁ h, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l₂

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case cons.mp.intro
α : Type u_1
β : Type u_2
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ ∃ a l₁ h,
    f 0 a ⋯ = f 0 x ⋯ ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l'.mapFinIdx fun i a h => f (i + 1) a ⋯

Proof state:
α : Type ?u.38817
β : Type ?u.38841
l₂ : List β
l : List α
b : β
f : (i : Nat) → α → i < l.length → β
a✝ : α
l₁ : List α
w : l = a✝ :: l₁
i : Nat
a : α
h : i < l₁.length
⊢ i < l₁.length

Tactic:
omega

Result:
no goals

Proof state:
case cons.mpr
α : Type u_1
β : Type u_2
l₂ : List β
b : β
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ (∃ a l₁ h, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l₂) →
    f 0 x ⋯ = b ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l₂

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

Result:
case cons.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ f 0 x ⋯ = f 0 x ⋯ ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l'.mapFinIdx fun i a h => f (i + 1) a ⋯

Proof state:
case cons
α : Type u_1
β : Type u_2
l₂ : List β
b : β
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ (x :: l').mapFinIdx f = b :: l₂ ↔ ∃ a l₁ w, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h => f (i + 1) a_1 ⋯) = l₂

Tactic:
simp only [mapFinIdx_cons, cons.injEq, length_cons, Fin.zero_eta, Fin.cast_succ_eq,
  exists_and_left]

Result:
case cons
α : Type u_1
β : Type u_2
l₂ : List β
b : β
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ f 0 x ⋯ = b ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l₂ ↔
    ∃ a l₁ h, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l₂

Proof state:
α : Type u_1
β : Type u_2
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ f 0 x ⋯ = f 0 x ⋯ ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l'.mapFinIdx fun i a h => f (i + 1) a ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.38817
β : Type ?u.38841
l₂ : List β
l : List α
b : β
f : (i : Nat) → α → i < l.length → β
a : α
l₁ : List α
w : l = a :: l₁
⊢ 0 < l.length

Tactic:
simp [w]

Result:
no goals

Proof state:
α : Type ?u.38817
β : Type ?u.38841
l₂ : List β
l : List α
b : β
f : (i : Nat) → α → i < l.length → β
a✝ : α
l₁ : List α
w : l = a✝ :: l₁
i : Nat
a : α
h : i < l₁.length
⊢ i + 1 < l.length

Tactic:
simp [w]

Result:
α : Type ?u.38817
β : Type ?u.38841
l₂ : List β
l : List α
b : β
f : (i : Nat) → α → i < l.length → β
a✝ : α
l₁ : List α
w : l = a✝ :: l₁
i : Nat
a : α
h : i < l₁.length
⊢ i < l₁.length

Proof state:
case cons
α : Type u_1
β : Type u_2
l₂ : List β
b : β
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ f 0 x ⋯ = b ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l₂ ↔
    ∃ a l₁ h, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l₂

Tactic:
constructor

Result:
case cons.mp
α : Type u_1
β : Type u_2
l₂ : List β
b : β
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ f 0 x ⋯ = b ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l₂ →
    ∃ a l₁ h, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l₂

case cons.mpr
α : Type u_1
β : Type u_2
l₂ : List β
b : β
x : α
l' : List α
f : (i : Nat) → α → i < (x :: l').length → β
⊢ (∃ a l₁ h, f 0 a ⋯ = b ∧ (l₁.mapFinIdx fun i a_1 h_1 => f (i + 1) a_1 ⋯) = l₂) →
    f 0 x ⋯ = b ∧ (l'.mapFinIdx fun i a h => f (i + 1) a ⋯) = l₂