internlm/Lean-Github huggingface dataset:
Theorem: List.zip_flat_index_go_get
Proof 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;
}
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof 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;
 }
}
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof 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
Proof 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) })
Theorem: List.zip_flat_index_go_get
Proof 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
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof 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
Proof 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) })
Theorem: List.zip_flat_index_go_get
Proof 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
Proof 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) })
Theorem: List.zip_flat_index_go_get
Proof 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]
}
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof 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;
}
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof 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
Proof 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) })
Theorem: List.zip_flat_index_go_get
Proof 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]
Proof state after:
no goals
Theorem: List.zip_flat_index_go_get
Proof 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]
Proof 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) })
Theorem: List.zip_flat_index_go_get
Proof 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]
Proof 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) })
Theorem: List.zip_flat_index_go_get
Proof 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]
Proof 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'
Theorem: List.zip_flat_index_go_get
Proof 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]
Proof 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'
Theorem: List.zip_flat_index_go_get
Proof 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
Proof 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'
Theorem: List.zip_flat_index_go_get
Proof 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
Proof 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')
Theorem: List.zip_flat_index_go_get
Proof 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
Proof state after:
no goals
Theorem: List.length_zip_flat_index
Proof state before:
α : Type u_1
xs : List α
⊢ length (zipFlatIndex xs) = length xs
Tactic:
apply Eq.symm
Proof state after:
case h
α : Type u_1
xs : List α
⊢ length xs = length (zipFlatIndex xs)
Theorem: List.length_zip_flat_index
Proof state before:
case h
α : Type u_1
xs : List α
⊢ length xs = length (zipFlatIndex xs)
Tactic:
apply zip_flat_index_go_length
Proof state after:
no goals
Theorem: List.zip_flat_index_get
Proof state before:
α : Type ?u.103966
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length (zipFlatIndex xs)
Tactic:
simp
Proof state after:
α : Type ?u.103966
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs
Theorem: List.zip_flat_index_get
Proof state before:
α : Type ?u.103966
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs
Tactic:
apply GETIX
Proof state after:
no goals
Theorem: List.zip_flat_index_get
Proof state before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getF (zipFlatIndex xs) getIx (_ : getIx < length (zipFlatIndex xs)) =
    (getF xs getIx GETIX, { ix := getIx, h_ix_inbound := GETIX })
Tactic:
simp[zipFlatIndex]
Proof state after:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getF (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs)) getIx
      (_ : getIx < length (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs))) =
    (getF xs getIx GETIX, { ix := getIx, h_ix_inbound := GETIX })
Theorem: List.zip_flat_index_get
Proof state before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getF (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs)) getIx
      (_ : getIx < length (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs))) =
    (getF xs getIx GETIX, { ix := getIx, h_ix_inbound := GETIX })
Tactic:
have RHS :  { ix := getIx, h_ix_inbound := GETIX : TensorFlatIndex (xs.length) } = {ix := 0 + getIx, h_ix_inbound := by { simp; apply GETIX } : TensorFlatIndex (xs.length)} := by {
  simp;
}
Proof state after:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
RHS : { ix := getIx, h_ix_inbound := GETIX } = { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) }
⊢ getF (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs)) getIx
      (_ : getIx < length (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs))) =
    (getF xs getIx GETIX, { ix := getIx, h_ix_inbound := GETIX })
Theorem: List.zip_flat_index_get
Proof state before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
RHS : { ix := getIx, h_ix_inbound := GETIX } = { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) }
⊢ getF (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs)) getIx
      (_ : getIx < length (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs))) =
    (getF xs getIx GETIX, { ix := getIx, h_ix_inbound := GETIX })
Tactic:
rewrite [RHS]
Proof state after:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
RHS : { ix := getIx, h_ix_inbound := GETIX } = { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) }
⊢ getF (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs)) getIx
      (_ : getIx < length (zipFlatIndexGo xs 0 (length xs) (_ : 0 + length xs = length xs))) =
    (getF xs getIx GETIX, { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) })