-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_cons_cons_zipIdx_snd (i : Nat) (l : List α) :
    (splitInTwo ⟨(a, i) :: (b, i+1) :: l.zipIdx (i+2), rfl⟩).2.1 =
      (splitInTwo ⟨a :: b :: l, rfl⟩).2.1.zipIdx (i+(l.length+3)/2)

Proof state:
case h.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝ : (l.length + 1 + 1 + 1) / 2 + j = 0
⊢ some (a, i) = Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) (some a)

Tactic:
simp

Result:
case h.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝ : (l.length + 1 + 1 + 1) / 2 + j = 0
⊢ i = i + (l.length + 3) / 2 + j

Proof state:
α : Type u_1
a b : α
i : Nat
l : List α
⊢ drop ((l.length + 1 + 1 + 1) / 2) ((a, i) :: (b, i + 1) :: l.zipIdx (i + 2)) =
    (drop ((l.length + 1 + 1 + 1) / 2) (a :: b :: l)).zipIdx (i + (l.length + 3) / 2)

Tactic:
ext1 j

Result:
case h
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
⊢ (drop ((l.length + 1 + 1 + 1) / 2) ((a, i) :: (b, i + 1) :: l.zipIdx (i + 2)))[j]? =
    ((drop ((l.length + 1 + 1 + 1) / 2) (a :: b :: l)).zipIdx (i + (l.length + 3) / 2))[j]?

Proof state:
case h.isFalse.isFalse.e_f
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ (fun a => (a, i + 2 + ((l.length + 1 + 1 + 1) / 2 + j - 1 - 1))) = fun a => (a, i + (l.length + 3) / 2 + j)

Tactic:
ext <;> simp

Result:
case h.isFalse.isFalse.e_f.h.snd
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
x✝ : α
⊢ i + 2 + ((l.length + 1 + 1 + 1) / 2 + j - 1 - 1) = i + (l.length + 3) / 2 + j

Proof state:
case h
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
⊢ (if (l.length + 1 + 1 + 1) / 2 + j = 0 then some (a, i)
    else
      if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some (b, i + 1)
      else (l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?) =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j))
      (if (l.length + 1 + 1 + 1) / 2 + j = 0 then some a
      else if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some b else l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?)

Tactic:
split

Result:
case h.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝ : (l.length + 1 + 1 + 1) / 2 + j = 0
⊢ some (a, i) = Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) (some a)

case h.isFalse
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
⊢ (if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some (b, i + 1)
    else (l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?) =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j))
      (if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some b else l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?)

Proof state:
case h.isFalse.isFalse
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ (l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]? =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?

Tactic:
simp only [getElem?_zipIdx]

Result:
case h.isFalse.isFalse
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ Option.map (fun a => (a, i + 2 + ((l.length + 1 + 1 + 1) / 2 + j - 1 - 1)))
      l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]? =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?

Proof state:
case h.isFalse
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
⊢ (if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some (b, i + 1)
    else (l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?) =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j))
      (if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some b else l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?)

Tactic:
split

Result:
case h.isFalse.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : (l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ some (b, i + 1) = Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) (some b)

case h.isFalse.isFalse
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ (l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]? =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?

Proof state:
case h.isFalse.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : (l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ i + 1 = i + (l.length + 3) / 2 + j

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
⊢ ((a, i) :: (b, i + 1) :: l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j]? =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) (a :: b :: l)[(l.length + 1 + 1 + 1) / 2 + j]?

Tactic:
rw [getElem?_cons, getElem?_cons, getElem?_cons, getElem?_cons]

Result:
case h
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
⊢ (if (l.length + 1 + 1 + 1) / 2 + j = 0 then some (a, i)
    else
      if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some (b, i + 1)
      else (l.zipIdx (i + 2))[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?) =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j))
      (if (l.length + 1 + 1 + 1) / 2 + j = 0 then some a
      else if (l.length + 1 + 1 + 1) / 2 + j - 1 = 0 then some b else l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?)

Proof state:
α : Type u_1
a b : α
i : Nat
l : List α
⊢ (splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), ⋯⟩).snd.val =
    (splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.zipIdx (i + (l.length + 3) / 2)

Tactic:
simp only [length_cons, splitInTwo_snd, length_zipIdx]

Result:
α : Type u_1
a b : α
i : Nat
l : List α
⊢ drop ((l.length + 1 + 1 + 1) / 2) ((a, i) :: (b, i + 1) :: l.zipIdx (i + 2)) =
    (drop ((l.length + 1 + 1 + 1) / 2) (a :: b :: l)).zipIdx (i + (l.length + 3) / 2)

Proof state:
case h.isFalse.isFalse.e_f.h.snd
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
x✝ : α
⊢ i + 2 + ((l.length + 1 + 1 + 1) / 2 + j - 1 - 1) = i + (l.length + 3) / 2 + j

Tactic:
omega

Result:
no goals

Proof state:
case h.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝ : (l.length + 1 + 1 + 1) / 2 + j = 0
⊢ i = i + (l.length + 3) / 2 + j

Tactic:
omega

Result:
no goals

Proof state:
case h.isFalse.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : (l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ some (b, i + 1) = Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) (some b)

Tactic:
simp

Result:
case h.isFalse.isTrue
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : (l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ i + 1 = i + (l.length + 3) / 2 + j

Proof state:
case h.isFalse.isFalse
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ Option.map (fun a => (a, i + 2 + ((l.length + 1 + 1 + 1) / 2 + j - 1 - 1)))
      l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]? =
    Option.map (fun a => (a, i + (l.length + 3) / 2 + j)) l[(l.length + 1 + 1 + 1) / 2 + j - 1 - 1]?

Tactic:
congr

Result:
case h.isFalse.isFalse.e_f
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝¹ : ¬(l.length + 1 + 1 + 1) / 2 + j = 0
h✝ : ¬(l.length + 1 + 1 + 1) / 2 + j - 1 = 0
⊢ (fun a => (a, i + 2 + ((l.length + 1 + 1 + 1) / 2 + j - 1 - 1))) = fun a => (a, i + (l.length + 3) / 2 + j)