Theorem: List.zip_flat_index_go_get (MLIR/Util/KDTensor.lean)

State before:
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < bound
Tactic:
rewrite [<- H]
State after:
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < ix + length xs

State before:
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < ix + length xs
Tactic:
simp [Nat.add_lt_add_left, GETIX]
State after:
no goals

State before:
α : Type u_1
⊢ ∀ (xs : List α) (ix bound : ℕ) (H : ix + length xs = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs),
    getF (zipFlatIndexGo xs ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs ix bound H)) =
      (getF xs deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
intros xs
State after:
α : Type u_1
xs : List α
⊢ ∀ (ix bound : ℕ) (H : ix + length xs = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs),
    getF (zipFlatIndexGo xs ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs ix bound H)) =
      (getF xs deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })

State before:
α : Type u_1
xs : List α
⊢ ∀ (ix bound : ℕ) (H : ix + length xs = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs),
    getF (zipFlatIndexGo xs ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs ix bound H)) =
      (getF xs deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
induction xs
State after:
case nil
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + length [] = bound) (deltaIx : ℕ) (GETIX : deltaIx < length []),
    getF (zipFlatIndexGo [] ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo [] ix bound H)) =
      (getF [] deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (ix bound : ℕ) (H : ix + length tail✝ = bound) (deltaIx : ℕ) (GETIX : deltaIx < length tail✝),
    getF (zipFlatIndexGo tail✝ ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo tail✝ ix bound H)) =
      (getF tail✝ deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
⊢ ∀ (ix bound : ℕ) (H : ix + length (head✝ :: tail✝) = bound) (deltaIx : ℕ) (GETIX : deltaIx < length (head✝ :: tail✝)),
    getF (zipFlatIndexGo (head✝ :: tail✝) ix bound H) deltaIx
        (_ : deltaIx < length (zipFlatIndexGo (head✝ :: tail✝) ix bound H)) =
      (getF (head✝ :: tail✝) deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })

State before:
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + length [] = bound) (deltaIx : ℕ) (GETIX : deltaIx < length []),
    getF (zipFlatIndexGo [] ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo [] ix bound H)) =
      (getF [] deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
case nil => {
    intros ix bound H deltaIx GETIX;
    simp [List.length, Nat.not_lt_zero] at GETIX;
}
State after:
no goals

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
⊢ ∀ (ix bound : ℕ) (H : ix + length (x :: xs') = bound) (deltaIx : ℕ) (GETIX : deltaIx < length (x :: xs')),
    getF (zipFlatIndexGo (x :: xs') ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo (x :: xs') ix bound H)) =
      (getF (x :: xs') deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
case cons x xs' IND => {
 intros ix bound H deltaIx GETIX; cases deltaIx;
 case zero => {
    simp;
    simp [zipFlatIndexGo, List.getF]
 }
 case succ deltaIx' => {
   simp [zipFlatIndexGo];
   simp [List.getF];
   rewrite [IND];
   simp [Nat.add_assoc, Nat.add_one, Nat.succ_add, Nat.add_succ];
   simp at GETIX;
   apply Nat.lt_of_succ_lt_succ;
   exact GETIX;
 }
}
State after:
no goals

State before:
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + length [] = bound) (deltaIx : ℕ) (GETIX : deltaIx < length []),
    getF (zipFlatIndexGo [] ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo [] ix bound H)) =
      (getF [] deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
intros ix bound H deltaIx GETIX
State after:
α : Type u_1
ix bound : ℕ
H : ix + length [] = bound
deltaIx : ℕ
GETIX : deltaIx < length []
⊢ getF (zipFlatIndexGo [] ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo [] ix bound H)) =
    (getF [] deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })

State before:
α : Type u_1
ix bound : ℕ
H : ix + length [] = bound
deltaIx : ℕ
GETIX : deltaIx < length []
⊢ getF (zipFlatIndexGo [] ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo [] ix bound H)) =
    (getF [] deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
simp [List.length, Nat.not_lt_zero] at GETIX
State after:
no goals

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
⊢ ∀ (ix bound : ℕ) (H : ix + length (x :: xs') = bound) (deltaIx : ℕ) (GETIX : deltaIx < length (x :: xs')),
    getF (zipFlatIndexGo (x :: xs') ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo (x :: xs') ix bound H)) =
      (getF (x :: xs') deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
intros ix bound H deltaIx GETIX
State after:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx : ℕ
GETIX : deltaIx < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx : ℕ
GETIX : deltaIx < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
Tactic:
cases deltaIx
State after:
case zero
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
GETIX : Nat.zero < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) Nat.zero (_ : Nat.zero < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') Nat.zero GETIX, { ix := ix + Nat.zero, h_ix_inbound := (_ : ix + Nat.zero < bound) })

case succ
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
n✝ : ℕ
GETIX : Nat.succ n✝ < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) (Nat.succ n✝)
      (_ : Nat.succ n✝ < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') (Nat.succ n✝) GETIX, { ix := ix + Nat.succ n✝, h_ix_inbound := (_ : ix + Nat.succ n✝ < bound) })

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
GETIX : Nat.zero < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) Nat.zero (_ : Nat.zero < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') Nat.zero GETIX, { ix := ix + Nat.zero, h_ix_inbound := (_ : ix + Nat.zero < bound) })
Tactic:
case zero => {
   simp;
   simp [zipFlatIndexGo, List.getF]
}
State after:
no goals

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) (Nat.succ deltaIx')
      (_ : Nat.succ deltaIx' < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') (Nat.succ deltaIx') GETIX,
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })
Tactic:
case succ deltaIx' => {
  simp [zipFlatIndexGo];
  simp [List.getF];
  rewrite [IND];
  simp [Nat.add_assoc, Nat.add_one, Nat.succ_add, Nat.add_succ];
  simp at GETIX;
  apply Nat.lt_of_succ_lt_succ;
  exact GETIX;
}
State after:
no goals

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
GETIX : Nat.zero < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) Nat.zero (_ : Nat.zero < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') Nat.zero GETIX, { ix := ix + Nat.zero, h_ix_inbound := (_ : ix + Nat.zero < bound) })
Tactic:
simp
State after:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
GETIX : Nat.zero < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) 0 (_ : Nat.zero < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') 0 GETIX, { ix := ix, h_ix_inbound := (_ : ix < bound) })

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
GETIX : Nat.zero < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) 0 (_ : Nat.zero < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') 0 GETIX, { ix := ix, h_ix_inbound := (_ : ix < bound) })
Tactic:
simp [zipFlatIndexGo, List.getF]
State after:
no goals

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ getF (zipFlatIndexGo (x :: xs') ix bound H) (Nat.succ deltaIx')
      (_ : Nat.succ deltaIx' < length (zipFlatIndexGo (x :: xs') ix bound H)) =
    (getF (x :: xs') (Nat.succ deltaIx') GETIX,
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })
Tactic:
simp [zipFlatIndexGo]
State after:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ getF
      ((x, { ix := ix, h_ix_inbound := (_ : ix < bound) }) ::
        zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound))
      (Nat.succ deltaIx')
      (_ :
        Nat.succ deltaIx' <
          length
            ((x, { ix := ix, h_ix_inbound := (_ : ix < bound) }) ::
              zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound))) =
    (getF (x :: xs') (Nat.succ deltaIx') GETIX,
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ getF
      ((x, { ix := ix, h_ix_inbound := (_ : ix < bound) }) ::
        zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound))
      (Nat.succ deltaIx')
      (_ :
        Nat.succ deltaIx' <
          length
            ((x, { ix := ix, h_ix_inbound := (_ : ix < bound) }) ::
              zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound))) =
    (getF (x :: xs') (Nat.succ deltaIx') GETIX,
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })
Tactic:
simp [List.getF]
State after:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ getF (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound)) deltaIx'
      (_ : deltaIx' < length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound))) =
    (getF xs' deltaIx' (_ : deltaIx' < length xs'),
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ getF (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound)) deltaIx'
      (_ : deltaIx' < length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + length xs' = bound))) =
    (getF xs' deltaIx' (_ : deltaIx' < length xs'),
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })
Tactic:
rewrite [IND]
State after:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ (getF xs' deltaIx' ?GETIX, { ix := ix + 1 + deltaIx', h_ix_inbound := (_ : ix + 1 + deltaIx' < bound) }) =
    (getF xs' deltaIx' (_ : deltaIx' < length xs'),
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })

case GETIX
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ deltaIx' < length xs'

State before:
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ (getF xs' deltaIx' ?GETIX, { ix := ix + 1 + deltaIx', h_ix_inbound := (_ : ix + 1 + deltaIx' < bound) }) =
    (getF xs' deltaIx' (_ : deltaIx' < length xs'),
      { ix := ix + Nat.succ deltaIx', h_ix_inbound := (_ : ix + Nat.succ deltaIx' < bound) })

case GETIX
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ deltaIx' < length xs'
Tactic:
simp [Nat.add_assoc, Nat.add_one, Nat.succ_add, Nat.add_succ]
State after:
case GETIX
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ deltaIx' < length xs'

State before:
case GETIX
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < length (x :: xs')
⊢ deltaIx' < length xs'
Tactic:
simp at GETIX
State after:
case GETIX
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < Nat.succ (length xs')
⊢ deltaIx' < length xs'

State before:
case GETIX
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < Nat.succ (length xs')
⊢ deltaIx' < length xs'
Tactic:
apply Nat.lt_of_succ_lt_succ
State after:
case GETIX.a
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < Nat.succ (length xs')
⊢ Nat.succ deltaIx' < Nat.succ (length xs')

State before:
case GETIX.a
α : Type u_1
x : α
xs' : List α
IND :
  ∀ (ix bound : ℕ) (H : ix + length xs' = bound) (deltaIx : ℕ) (GETIX : deltaIx < length xs'),
    getF (zipFlatIndexGo xs' ix bound H) deltaIx (_ : deltaIx < length (zipFlatIndexGo xs' ix bound H)) =
      (getF xs' deltaIx GETIX, { ix := ix + deltaIx, h_ix_inbound := (_ : ix + deltaIx < bound) })
ix bound : ℕ
H : ix + length (x :: xs') = bound
deltaIx' : ℕ
GETIX : Nat.succ deltaIx' < Nat.succ (length xs')
⊢ Nat.succ deltaIx' < Nat.succ (length xs')
Tactic:
exact GETIX
State after:
no goals