Step table

theorem step_table (n e : ℕ) :    step (L := L) (ξ := ξ) n (table (L := L) (ξ := ξ) n e) = encode (ofNat (L := L) (ξ := ξ) n e) := by  rw [step, table_length]  cases e with  | zero => simp [ofNat]  | succ d =>  show stepBody (L := L) (ξ := ξ) n (table (L := L) (ξ := ξ) n (d + 1)) d = _  rw [stepBody, ofNat]  by_cases h0 : (Nat.unpair d).1 = 0  · rw [if_pos h0, h0]    by_cases hz : (Nat.unpair d).2 < n    · rw [if_pos hz, dif_pos hz]      simp [encode_eq_toNat, toNat]    · rw [if_neg hz, dif_neg hz]      simp  by_cases h1 : (Nat.unpair d).1 = 1  · rw [if_neg h0, if_pos h1, h1]    rcases hx : (decode (Nat.unpair d).2 : Option ξ) with _ | x    · simp    · rw [if_neg (by simp)]      simp [encode_eq_toNat, toNat]  by_cases h2 : (Nat.unpair d).1 = 2  · rw [if_neg h0, if_neg h1, if_pos h2, h2]    simp only []    rcases hv : (Nat.unpair (Nat.unpair (Nat.unpair d).2).2).2.natToVec        (Nat.unpair (Nat.unpair d).2).1 with _ | v'    · rw [if_neg ?_]      · simp      · rintro ⟨hlen, -, -⟩        obtain ⟨w, hw⟩ := Nat.natToVec_isSome_of_length hlen        rw [hw] at hv        exact absurd hv (by simp)    · have hl : (Nat.unpair (Nat.unpair (Nat.unpair d).2).2).2.natToList = List.ofFn v' :=        Nat.natToVec_eq_some_iff.mp hv      have hlen : (Nat.unpair (Nat.unpair (Nat.unpair d).2).2).2.natToList.length          = (Nat.unpair (Nat.unpair d).2).1 := by rw [hl]; simp      have hlt : ∀ i, v' i < d + 1 := fun i ↦        Nat.lt_succ_iff.mpr <| le_trans (le_of_lt <| Nat.lt_of_eq_natToVec hv i)          <| le_trans (Nat.unpair_right_le _) <| le_trans (Nat.unpair_right_le _)          <| Nat.unpair_right_le _      rcases hf : (decode (Nat.unpair (Nat.unpair (Nat.unpair d).2).2).1 :          Option (L.Func (Nat.unpair (Nat.unpair d).2).1)) with _ | f      · rw [if_neg ?_]        · simp        · rintro ⟨-, hne, -⟩          exact hne (by simp)      · rcases hg : (Matrix.getM fun i ↦ ofNat (L := L) (ξ := ξ) n (v' i)) with _ | t        · obtain ⟨i₀, hi₀⟩ : ∃ i, ofNat (L := L) (ξ := ξ) n (v' i) = none := by            by_contra hcon            push Not at hcon            choose t ht using fun i ↦ Option.ne_none_iff_exists'.mp (hcon i)            rw [Matrix.getM_option_eq_some_iff.mpr ht] at hg            exact absurd hg (by simp)          rw [if_neg ?_]          · simp [hg]          · rintro ⟨-, -, hne⟩            refine hne (stepVec_eq_zero (j := v' i₀) ?_ ?_)            · rw [hl]; exact List.mem_ofFn.mpr ⟨i₀, rfl⟩            · rw [table_getD (hlt i₀), hi₀]; simp        · have hT : ∀ i, (table (L := L) (ξ := ξ) n (d + 1)).getD (v' i) 0              = encode (t i) + 1 := fun i ↦ by            rw [table_getD (hlt i), Matrix.getM_option_eq_some_iff.mp hg i]            simp          have hsv : stepVec (table (L := L) (ξ := ξ) n (d + 1))              (Nat.natToList (Nat.unpair (Nat.unpair (Nat.unpair d).2).2).2)              = Matrix.vecToNat (fun i ↦ encode (t i)) + 1 := by            rw [hl]; exact stepVec_ofFn hT          rw [if_pos ⟨hlen, by simp, by rw [hsv]; simp⟩, hsv]          simp [hg, encode_eq_toNat, toNat]  · rw [if_neg h0, if_neg h1, if_neg h2]    match hi : (Nat.unpair d).1 with    | 0 => exact absurd hi h0    | 1 => exact absurd hi h1    | 2 => exact absurd hi h2    | k + 3 => simp