-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem fst_eq_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) :
    x.1 = l[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega)

Proof state:
case nil
α : Type u_1
x : α × Nat
k : Nat
h : x ∈ [].zipIdx k
⊢ x.fst = [][x.snd - k]

Tactic:
cases h

Result:
no goals

Proof state:
α : Type u_1
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.fst = l[x.snd - k]

Tactic:
induction l generalizing k with
| nil => cases h
| cons hd tl ih =>
  cases h with
  | head h => simp
  | tail h m =>
    specialize ih m
    have : x.2 - k = x.2 - (k + 1) + 1 := by
      have := le_snd_of_mem_zipIdx m
      omega
    simp [this, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α × Nat
hd : α
tl : List α
ih : ∀ {k : Nat} (h : x ∈ tl.zipIdx k), x.fst = tl[x.snd - k]
k : Nat
h : x ∈ (hd :: tl).zipIdx k
⊢ x.fst = (hd :: tl)[x.snd - k]

Tactic:
cases h with
| head h => simp
| tail h m =>
  specialize ih m
  have : x.2 - k = x.2 - (k + 1) + 1 := by
    have := le_snd_of_mem_zipIdx m
    omega
  simp [this, ih]

Result:
no goals

Proof state:
α : Type ?u.50288
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
this : k ≤ x.snd
⊢ x.snd - k < l.length

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.50288
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
this✝ : k ≤ x.snd
this : x.snd < k + l.length
⊢ x.snd - k < l.length

Proof state:
case cons.tail
α : Type u_1
x : α × Nat
hd : α
tl : List α
k : Nat
m : Mem x (tl.zipIdx (k + 1))
ih : x.fst = tl[x.snd - (k + 1)]
⊢ x.fst = (hd :: tl)[x.snd - k]

Tactic:
have : x.2 - k = x.2 - (k + 1) + 1 := by
  have := le_snd_of_mem_zipIdx m
  omega

Result:
case cons.tail
α : Type u_1
x : α × Nat
hd : α
tl : List α
k : Nat
m : Mem x (tl.zipIdx (k + 1))
ih : x.fst = tl[x.snd - (k + 1)]
this : x.snd - k = x.snd - (k + 1) + 1
⊢ x.fst = (hd :: tl)[x.snd - k]

Proof state:
α : Type u_1
x : α × Nat
hd : α
tl : List α
k : Nat
m : Mem x (tl.zipIdx (k + 1))
ih : x.fst = tl[x.snd - (k + 1)]
this : k + 1 ≤ x.snd
⊢ x.snd - k = x.snd - (k + 1) + 1

Tactic:
omega

Result:
no goals

Proof state:
case cons.tail
α : Type u_1
x : α × Nat
hd : α
tl : List α
ih : ∀ {k : Nat} (h : x ∈ tl.zipIdx k), x.fst = tl[x.snd - k]
k : Nat
m : Mem x (tl.zipIdx (k + 1))
⊢ x.fst = (hd :: tl)[x.snd - k]

Tactic:
specialize ih m

Result:
case cons.tail
α : Type u_1
x : α × Nat
hd : α
tl : List α
k : Nat
m : Mem x (tl.zipIdx (k + 1))
ih : x.fst = tl[x.snd - (k + 1)]
⊢ x.fst = (hd :: tl)[x.snd - k]

Proof state:
case cons.head
α : Type u_1
hd : α
tl : List α
k : Nat
ih : ∀ {k_1 : Nat} (h : (hd, k) ∈ tl.zipIdx k_1), (hd, k).fst = tl[(hd, k).snd - k_1]
⊢ (hd, k).fst = (hd :: tl)[(hd, k).snd - k]

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.50288
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
this✝ : k ≤ x.snd
this : x.snd < k + l.length
⊢ x.snd - k < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.50288
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd - k < l.length

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.50288
x : α × Nat
l : List α
k : Nat
h : x ∈ l.zipIdx k
this : k ≤ x.snd
⊢ x.snd - k < l.length

Proof state:
α : Type u_1
x : α × Nat
hd : α
tl : List α
k : Nat
m : Mem x (tl.zipIdx (k + 1))
ih : x.fst = tl[x.snd - (k + 1)]
⊢ x.snd - k = x.snd - (k + 1) + 1

Tactic:
have := le_snd_of_mem_zipIdx m

Result:
α : Type u_1
x : α × Nat
hd : α
tl : List α
k : Nat
m : Mem x (tl.zipIdx (k + 1))
ih : x.fst = tl[x.snd - (k + 1)]
this : k + 1 ≤ x.snd
⊢ x.snd - k = x.snd - (k + 1) + 1

Proof state:
case cons.tail
α : Type u_1
x : α × Nat
hd : α
tl : List α
k : Nat
m : Mem x (tl.zipIdx (k + 1))
ih : x.fst = tl[x.snd - (k + 1)]
this : x.snd - k = x.snd - (k + 1) + 1
⊢ x.fst = (hd :: tl)[x.snd - k]

Tactic:
simp [this, ih]

Result:
no goals