-- 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:
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]

Tactic:
simp only [getElem_mapFinIdx, getElem_take]

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
⊢ f (i + (take l₁.length l).length) (drop l₁.length l)[i] ⋯ = l₂[i]

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

Tactic:
refine ⟨by simp, fun i h => ?_⟩

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
⊢ ((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

Proof state:
case mpr.intro.intro.intro.intro.isTrue
α : 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
⊢ (l₁'.mapFinIdx fun i a h => f i a ⋯)[i] = f i (l₁' ++ l₂')[i] h

Tactic:
simp [getElem_append_left (by simpa using h')]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.isFalse
α : 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
this : i - l₁'.length + l₁'.length = i
⊢ (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

Tactic:
simp [getElem_append_right h', this]

Result:
no goals

Proof state:
α : 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 < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length
hi₂ : i < l₁.length
⊢ i < l.length

Tactic:
omega

Result:
no goals

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 < 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 + l₂'.length

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
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
this : l₁.length ≤ l.length
w : l₂[i + l₁.length - l₁.length] = f (i + l₁.length) l[i + l₁.length] ⋯
⊢ f (i + l₁.length) l[i + l₁.length] ⋯ = l₂[i]

Tactic:
simpa using w.symm

Result:
no goals

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
⊢ ?m.63951 < length ?m.63952

Tactic:
simpa using h'

Result:
no goals

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

Tactic:
simp

Result:
no goals

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
⊢ ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length = l₂.length

Tactic:
simp

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
⊢ l.length - l₁.length = l₂.length

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 + l₂'.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.isFalse
α : 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
⊢ (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

Tactic:
simp only [length_mapFinIdx, Nat.not_lt] at h'

Result:
case mpr.intro.intro.intro.intro.isFalse
α : 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
⊢ (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.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

Tactic:
simp

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
⊢ min l₁.length l.length = l₁.length

Proof state:
α : 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
this : l₁.length ≤ l.length
⊢ i + l₁.length < l.length

Tactic:
omega

Result:
no goals