-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_append_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {l₁ l₂ : Array β} :
    l.mapFinIdx f = l₁ ++ l₂ ↔
      ∃ (l₁' : Array α) (l₂' : Array α) (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₁'.size) a (by simp [w]; omega)) = l₂

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : (i : Nat) → α → i < { toList := l₁ ++ l₂ }.size → β
⊢ ∃ h,
    (l₁.toArray.mapFinIdx fun i a h_1 => f i a ⋯) = { toList := l₁.mapFinIdx fun i a h => f i a ⋯ } ∧
      (l₂.toArray.mapFinIdx fun i a h_1 => f (i + l₁.toArray.size) a ⋯) =
        { toList := l₂.mapFinIdx fun i a h => f (i + l₁.length) a ⋯ }

Tactic:
simp_all

Result:
no goals

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

Tactic:
simp only [List.mapFinIdx_toArray, List.append_toArray, mk.injEq, List.mapFinIdx_eq_append_iff,
  toArray_eq_append_iff]

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l₁ 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₂' h,
      (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = { toList := l₁ } ∧
        (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = { toList := l₂ }

Proof state:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
l₁✝ l₂✝ : List β
l₁ l₂ : List α
f : (i : Nat) → α → i < { toList := { toList := l₁ }.toList ++ { toList := l₂ }.toList }.size → β
h₁ : (l₁.mapFinIdx fun i a h => f i a ⋯) = l₁✝
h₂ : (l₂.mapFinIdx fun i a h => f (i + l₁.length) a ⋯) = l₂✝
⊢ ∃ 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:
obtain rfl := h₁

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

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

Tactic:
rcases l₂ with ⟨l₂⟩

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

Proof state:
α : Type ?u.78996
β : Type ?u.79017
l : Array α
f : (i : Nat) → α → i < l.size → β
l₁ l₂ : Array β
l₁' l₂' : Array α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₂'.size
⊢ i + l₁'.size < l.size

Tactic:
simp [w]

Result:
α : Type ?u.78996
β : Type ?u.79017
l : Array α
f : (i : Nat) → α → i < l.size → β
l₁ l₂ : Array β
l₁' l₂' : Array α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₂'.size
⊢ i + l₁'.size < l₁'.size + l₂'.size

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

Tactic:
obtain rfl := h₂

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

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l₁ 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₂' h,
      (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = { toList := l₁ } ∧
        (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = { toList := l₂ }

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l₁ 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₂' h,
      (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = { toList := l₁ } ∧
        (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = { toList := l₂ }

case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l₁ l₂ : List β
⊢ (∃ l₁' l₂' h,
      (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = { toList := l₁ } ∧
        (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = { toList := l₂ }) →
    ∃ 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₂

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : (i : Nat) → α → i < { toList := { toList := l₁ }.toList ++ { toList := l₂ }.toList }.size → β
⊢ ∃ w,
    ((l₁.mapFinIdx fun i a h => f i a ⋯) = l₁.mapFinIdx fun i a h => f i a ⋯) ∧
      (l₂.mapFinIdx fun i a h => f (i + l₁.length) a ⋯) = l₂.mapFinIdx fun i a h => f (i + l₁.length) a ⋯

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type ?u.78996
β : Type ?u.79017
l : Array α
f : (i : Nat) → α → i < l.size → β
l₁ l₂ : Array β
l₁' l₂' : Array α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₁'.size
⊢ i < l.size

Tactic:
simp [w]

Result:
α : Type ?u.78996
β : Type ?u.79017
l : Array α
f : (i : Nat) → α → i < l.size → β
l₁ l₂ : Array β
l₁' l₂' : Array α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₁'.size
⊢ i < l₁'.size + l₂'.size

Proof state:
case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l₁ l₂ : List β
⊢ (∃ l₁' l₂' h,
      (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = { toList := l₁ } ∧
        (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = { toList := l₂ }) →
    ∃ 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:
rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
l₁✝ l₂✝ : List β
l₁ l₂ : List α
f : (i : Nat) → α → i < { toList := { toList := l₁ }.toList ++ { toList := l₂ }.toList }.size → β
h₁ : ({ toList := l₁ }.mapFinIdx fun i a h => f i a ⋯) = { toList := l₁✝ }
h₂ : ({ toList := l₂ }.mapFinIdx fun i a h => f (i + { toList := l₁ }.size) a ⋯) = { toList := l₂✝ }
⊢ ∃ 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₂✝