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

State before:
α : Type ?u.103966
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length (zipFlatIndex xs)
Tactic:
simp
State after:
α : Type ?u.103966
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs

State before:
α : Type ?u.103966
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs
Tactic:
apply GETIX
State after:
no goals

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]
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 })

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;
}
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 })

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]
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) })

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 := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) })
Tactic:
apply List.zip_flat_index_go_get (xs := xs) (ix := 0) (bound := List.length xs) (deltaIx := getIx) (GETIX := GETIX)
State after:
no goals

State before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ 0 + getIx < length xs
Tactic:
simp
State after:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs

State before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ getIx < length xs
Tactic:
apply GETIX
State after:
no goals

State before:
α : Type u_1
xs : List α
getIx : ℕ
GETIX : getIx < length xs
⊢ { ix := getIx, h_ix_inbound := GETIX } = { ix := 0 + getIx, h_ix_inbound := (_ : 0 + getIx < length xs) }
Tactic:
simp
State after:
no goals