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

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ mapIdx f { toList := l } = { toList := l₁ } ++ { toList := l₂ } ↔
    ∃ l₁' l₂',
      { toList := l } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }

Tactic:
simp only [List.mapIdx_toArray, List.append_toArray, mk.injEq, List.mapIdx_eq_append_iff,
  toArray_eq_append_iff]

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ List.mapIdx f l₁' = l₁ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂) ↔
    ∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }

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

Tactic:
simp only [List.mapIdx_toArray, mk.injEq, size_toArray] at h₁ h₂

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

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

Tactic:
obtain rfl := h₁

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

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁ l₂ : List α
⊢ l₁ ++ l₂ = l₁.toArray.toList ++ l₂.toArray.toList ∧
    mapIdx f l₁.toArray = { toList := List.mapIdx f l₁ } ∧
      mapIdx (fun i => f (i + l₁.toArray.size)) l₂.toArray = { toList := List.mapIdx (fun i => f (i + l₁.length)) l₂ }

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ List.mapIdx f l₁' = l₁ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂) →
    ∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }

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

Result:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁ l₂ : List α
⊢ ∃ l₁' l₂',
    l₁ ++ l₂ = l₁'.toList ++ l₂'.toList ∧
      mapIdx f l₁' = { toList := List.mapIdx f l₁ } ∧
        mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := List.mapIdx (fun i => f (i + l₁.length)) l₂ }

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ List.mapIdx f l₁' = l₁ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂) ↔
    ∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ List.mapIdx f l₁' = l₁ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂) →
    ∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }

case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
l₁ l₂ : List β
⊢ (∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧
        mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = { toList := l₂ }) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ List.mapIdx f l₁' = l₁ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂

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

Tactic:
exact ⟨l₁.toArray, l₂.toArray, by simp⟩

Result:
no goals

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

Tactic:
obtain rfl := h₂

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

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁ l₂ : Array β
l : List α
⊢ mapIdx f { toList := l } = l₁ ++ l₂ ↔
    ∃ l₁' l₂', { toList := l } = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l₂ : Array β
l : List α
l₁ : List β
⊢ mapIdx f { toList := l } = { toList := l₁ } ++ l₂ ↔
    ∃ l₁' l₂',
      { toList := l } = l₁' ++ l₂' ∧ mapIdx f l₁' = { toList := l₁ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

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

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l₁ l₂ : Array β
l : List α
⊢ mapIdx f { toList := l } = l₁ ++ l₂ ↔
    ∃ l₁' l₂', { toList := l } = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

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

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

Result:
no goals