Theorem: get_eq_getzip (Pdl/Modelgraphs.lean)

State before:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = (((x, X) :: δ.zip (l ++ [Y])).get ⟨↑i, h⟩).2
Tactic:
simp only [←List.zip_cons_cons]
State after:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = (((x :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, h⟩).2

State before:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = (((x :: δ).zip (X :: (l ++ [Y]))).get ⟨↑i, h⟩).2
Tactic:
rw [List.get_zip]
State after:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = ((x :: δ).get ⟨↑⟨↑i, h⟩, ⋯⟩, (X :: (l ++ [Y])).get ⟨↑⟨↑i, h⟩, ⋯⟩).2

State before:
α : Type u_1
l : List α
α✝ : Type u_2
x : α✝
δ : List α✝
X Y : α
i : Fin (l ++ [Y]).length
h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length
⊢ (X :: (l ++ [Y])).get i.castSucc = ((x :: δ).get ⟨↑⟨↑i, h⟩, ⋯⟩, (X :: (l ++ [Y])).get ⟨↑⟨↑i, h⟩, ⋯⟩).2
Tactic:
rfl
State after:
no goals