-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_append_iff {l : List α} :
    mapIdx f l = l₁ ++ l₂ ↔
      ∃ (l₁' : List α) (l₂' : List α), l = l₁' ++ l₂' ∧
        mapIdx f l₁' = l₁ ∧
        mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁', mapIdx f l₁' = l₁ ∧ ∃ x, l = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = l₂) ↔
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

Tactic:
constructor

Result:
case mp
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁', mapIdx f l₁' = l₁ ∧ ∃ x, l = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = l₂) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

case mpr
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂) →
    ∃ l₁', mapIdx f l₁' = l₁ ∧ ∃ x, l = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = l₂

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁' l₂' w, (l₁'.mapFinIdx fun i a h => f i a) = l₁ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a) = l₂) ↔
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

Tactic:
simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]

Result:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁', mapIdx f l₁' = l₁ ∧ ∃ x, l = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = l₂) ↔
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₂✝ : List α✝
l₁ l₂ : List α
h : mapIdx (fun i => f (i + l₁.length)) l₂ = l₂✝
⊢ l₁ ++ l₂ = l₁ ++ l₂ ∧ mapIdx f l₁ = mapIdx f l₁ ∧ mapIdx (fun i => f (i + l₁.length)) l₂ = l₂✝

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α
⊢ l₁ ++ l₂ = l₁ ++ l₂ ∧ mapIdx (fun i => f (i + l₁.length)) l₂ = mapIdx (fun i => f (i + l₁.length)) l₂

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ mapIdx f l = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

Tactic:
rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_append_iff]

Result:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁' l₂' w, (l₁'.mapFinIdx fun i a h => f i a) = l₁ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a) = l₂) ↔
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

Proof state:
case mp
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁', mapIdx f l₁' = l₁ ∧ ∃ x, l = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = l₂) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

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

Result:
case mp.intro.intro.intro.intro
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₂✝ : List α✝
l₁ l₂ : List α
h : mapIdx (fun i => f (i + l₁.length)) l₂ = l₂✝
⊢ ∃ l₁' l₂', l₁ ++ l₂ = l₁' ++ l₂' ∧ mapIdx f l₁' = mapIdx f l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂✝

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α
⊢ ∃ l₁',
    mapIdx f l₁' = mapIdx f l₁ ∧
      ∃ x, l₁ ++ l₂ = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = mapIdx (fun i => f (i + l₁.length)) l₂

Tactic:
refine ⟨l₁, rfl, l₂, by simp_all⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α✝
l : List α
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂) →
    ∃ l₁', mapIdx f l₁' = l₁ ∧ ∃ x, l = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = l₂

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

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₁ l₂ : List α
⊢ ∃ l₁',
    mapIdx f l₁' = mapIdx f l₁ ∧
      ∃ x, l₁ ++ l₂ = l₁' ++ x ∧ mapIdx (fun i => f (i + l₁'.length)) x = mapIdx (fun i => f (i + l₁.length)) l₂

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l₂✝ : List α✝
l₁ l₂ : List α
h : mapIdx (fun i => f (i + l₁.length)) l₂ = l₂✝
⊢ ∃ l₁' l₂', l₁ ++ l₂ = l₁' ++ l₂' ∧ mapIdx f l₁' = mapIdx f l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂✝

Tactic:
refine ⟨l₁, l₂, by simp_all⟩

Result:
no goals