Theorem: zip_flat_index_go_length (MLIR/Util/KDTensor.lean)

State before:
α : Type u_1
xs : List α
⊢ ∀ (ix bound : ℕ) (H : ix + List.length xs = bound), List.length xs = List.length (zipFlatIndexGo xs ix bound H)
Tactic:
induction xs
State after:
case nil
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + List.length [] = bound), List.length [] = List.length (zipFlatIndexGo [] ix bound H)

case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (ix bound : ℕ) (H : ix + List.length tail✝ = bound),
    List.length tail✝ = List.length (zipFlatIndexGo tail✝ ix bound H)
⊢ ∀ (ix bound : ℕ) (H : ix + List.length (head✝ :: tail✝) = bound),
    List.length (head✝ :: tail✝) = List.length (zipFlatIndexGo (head✝ :: tail✝) ix bound H)

State before:
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + List.length [] = bound), List.length [] = List.length (zipFlatIndexGo [] ix bound H)
Tactic:
case nil => {
  intros; unfold zipFlatIndexGo; rfl;
}
State after:
no goals

State before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
⊢ ∀ (ix bound : ℕ) (H : ix + List.length (x :: xs') = bound),
    List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
Tactic:
case cons x xs' IND => {
  intros ix bound H;
  simp [zipFlatIndexGo];
  apply IND;
}
State after:
no goals

State before:
α : Type u_1
⊢ ∀ (ix bound : ℕ) (H : ix + List.length [] = bound), List.length [] = List.length (zipFlatIndexGo [] ix bound H)
Tactic:
intros
State after:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length (zipFlatIndexGo [] ix✝ bound✝ H✝)

State before:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length (zipFlatIndexGo [] ix✝ bound✝ H✝)
Tactic:
unfold zipFlatIndexGo
State after:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length []

State before:
α : Type u_1
ix✝ bound✝ : ℕ
H✝ : ix✝ + List.length [] = bound✝
⊢ List.length [] = List.length []
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
⊢ ∀ (ix bound : ℕ) (H : ix + List.length (x :: xs') = bound),
    List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
Tactic:
intros ix bound H
State after:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)

State before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length (x :: xs') = List.length (zipFlatIndexGo (x :: xs') ix bound H)
Tactic:
simp [zipFlatIndexGo]
State after:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length xs' = List.length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + List.length xs' = bound))

State before:
α : Type u_1
x : α
xs' : List α
IND : ∀ (ix bound : ℕ) (H : ix + List.length xs' = bound), List.length xs' = List.length (zipFlatIndexGo xs' ix bound H)
ix bound : ℕ
H : ix + List.length (x :: xs') = bound
⊢ List.length xs' = List.length (zipFlatIndexGo xs' (ix + 1) bound (_ : ix + 1 + List.length xs' = bound))
Tactic:
apply IND
State after:
no goals