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

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1) ↔
    ∃ 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₂

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1) →
    ∃ 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₂

case mpr
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ 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₂) →
    ∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1

Proof state:
α : Type ?u.50384
β : Type ?u.50406
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
l₁' l₂' : List α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₁'.length
⊢ i < l.length

Tactic:
simp [w]

Result:
α : Type ?u.50384
β : Type ?u.50406
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
l₁' l₂' : List α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₁'.length
⊢ i < l₁'.length + l₂'.length

Proof state:
α : Type u_1
β : Type u_2
l₁' l₂' : List α
f : (i : Nat) → α → i < (l₁' ++ l₂').length → β
i : Nat
h : i < (l₁' ++ l₂').length
h'✝ : ¬i < (l₁'.mapFinIdx fun i a h => f i a ⋯).length
h' : l₁'.length ≤ i
⊢ i - l₁'.length + l₁'.length = i

Tactic:
omega

Result:
no goals

Proof state:
case mp.right.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ∀ (i : Nat) (h₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length)
    (h₂ : i < l₂.length), ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯)[i] = l₂[i]

Tactic:
intro i hi₁ hi₂

Result:
case mp.right.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length
hi₂ : i < l₂.length
⊢ ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯)[i] = l₂[i]

Proof state:
case mp.right
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯) = l₂

Tactic:
apply ext_getElem

Result:
case mp.right.hl
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length = l₂.length

case mp.right.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ∀ (i : Nat) (h₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length)
    (h₂ : i < l₂.length), ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯)[i] = l₂[i]

Proof state:
case mp.left
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯) = l₁

Tactic:
apply ext_getElem

Result:
case mp.left.hl
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length = l₁.length

case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ∀ (i : Nat) (h₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length) (h₂ : i < l₁.length),
    ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯)[i] = l₁[i]

Proof state:
case mp.right.hl
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ l.length - l₁.length = l₂.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁' l₂' : List α
f : (i : Nat) → α → i < (l₁' ++ l₂').length → β
i : Nat
h : i < (l₁' ++ l₂').length
⊢ ((l₁'.mapFinIdx fun i a h => f i a ⋯) ++ l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯)[i] = f i (l₁' ++ l₂')[i] h

Tactic:
rw [getElem_append]

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁' l₂' : List α
f : (i : Nat) → α → i < (l₁' ++ l₂').length → β
i : Nat
h : i < (l₁' ++ l₂').length
⊢ (if h' : i < (l₁'.mapFinIdx fun i a h => f i a ⋯).length then (l₁'.mapFinIdx fun i a h => f i a ⋯)[i]
    else (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯)[i - (l₁'.mapFinIdx fun i a h => f i a ⋯).length]) =
    f i (l₁' ++ l₂')[i] h

Proof state:
case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length
hi₂ : i < l₁.length
w : l₁[i] = f i l[i] ⋯
⊢ f i l[i] ⋯ = l₁[i]

Tactic:
exact w.symm

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ∃ 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₂

Tactic:
refine ⟨l.take l₁.length, l.drop l₁.length, by simp, ?_⟩

Result:
case mp
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯) = l₁ ∧
    ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯) = l₂

Proof state:
case mp.left.hl
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ min l₁.length l.length = l₁.length

Tactic:
omega

Result:
no goals