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

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

Tactic:
simp only [length_cons, splitInTwo_fst, length_zipIdx]

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

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

Tactic:
ext <;> simp

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
rw [getElem?_take, getElem?_zipIdx, getElem?_take]

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

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

Tactic:
ext1 j

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

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

Tactic:
split

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

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

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

Tactic:
simp

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp

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

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

Tactic:
split

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

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

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

Tactic:
split

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

case h.isFalse
α : Type u_1
a b : α
i : Nat
l : List α
j : Nat
h✝ : ¬j < (l.length + 1 + 1 + 1) / 2
⊢ none = Option.map (fun a => (a, i + j)) none

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

Tactic:
simp only [getElem?_zipIdx]

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

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

Tactic:
congr

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

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

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

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
omega

Result:
no goals