-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem snd_eq_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
    x.2 = l[x.1 - n]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega)

Proof state:
α : Type ?u.62273
x : Nat × α
n : Nat
l : List α
h : x ∈ enumFrom n l
⊢ x.fst - n < l.length

Tactic:
have := le_fst_of_mem_enumFrom h

Result:
α : Type ?u.62273
x : Nat × α
n : Nat
l : List α
h : x ∈ enumFrom n l
this : n ≤ x.fst
⊢ x.fst - n < l.length

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

Tactic:
have := le_fst_of_mem_enumFrom m

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

Proof state:
α : Type ?u.62273
x : Nat × α
n : Nat
l : List α
h : x ∈ enumFrom n l
this : n ≤ x.fst
⊢ x.fst - n < l.length

Tactic:
have := fst_lt_add_of_mem_enumFrom h

Result:
α : Type ?u.62273
x : Nat × α
n : Nat
l : List α
h : x ∈ enumFrom n l
this✝ : n ≤ x.fst
this : x.fst < n + l.length
⊢ x.fst - n < l.length

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

Tactic:
specialize ih m

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

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

Tactic:
have : x.1 - n = x.1 - (n + 1) + 1 := by
  have := le_fst_of_mem_enumFrom m
  omega

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.62273
x : Nat × α
n : Nat
l : List α
h : x ∈ enumFrom n l
this✝ : n ≤ x.fst
this : x.fst < n + l.length
⊢ x.fst - n < l.length

Tactic:
omega

Result:
no goals

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

Tactic:
simp [this, ih]

Result:
no goals

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

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

Result:
no goals

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

Tactic:
cases h

Result:
no goals

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

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

Result:
no goals