Succ Above of neq zero

lemma succAbove_of_neq_zero {n n1 : ℕ} {c : Fin (n + 1) → C} {c1 : Fin (n1 + 1) → C}    {σ : Fin (n1 + 1) → Fin (n + 1)} (i : Fin (n1 + 1))    (h : IsReindexing c c1 σ) (hi : σ i ≠ 0) :    IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove)      ((Fin.pred (σ i) hi).predAbove  ∘ σ ∘ i.succAbove) := by  have hpr : σ i = ((σ i).pred hi).succ := (Fin.succ_pred _ _).symm  have hne : ∀ x, σ (i.succAbove x) ≠ σ i := fun x heq =>    Fin.succAbove_ne i x (h.injective heq)  refine ⟨⟨?_, ?_⟩, ?_⟩  · intro x1 x2 h2    simp only [Function.comp_apply] at h2    apply i.succAbove_right_injective (h.injective ?_)    suffices h' :        ((σ i).pred hi).succ.succAbove (((σ i).pred hi).predAbove (σ (i.succAbove x1))) =        ((σ i).pred hi).succ.succAbove (((σ i).pred hi).predAbove (σ (i.succAbove x2))) by      rwa [Fin.succ_succAbove_predAbove (hpr ▸ hne x1),        Fin.succ_succAbove_predAbove (hpr ▸ hne x2)] at h'    simpa using h2  · intro k    simp only [Function.comp_apply]    suffices h' : ∃ a, σ (i.succAbove a) = (σ i).succAbove k by      conv => enter [1, a]; rw [← ((σ i).pred hi).succ.succAbove_right_injective.eq_iff]      obtain ⟨a, h'⟩ := h'      exact ⟨a, by rw [Fin.succ_succAbove_predAbove (hpr ▸ hne a), ← hpr]; exact h'⟩    obtain ⟨j, hj⟩ := h.surjective ((σ i).succAbove k)    simp only [← hj, h.injective.eq_iff, Fin.exists_succAbove_eq_iff, ne_eq]    rintro rfl    simp at hj  · intro x    simp only [h.preserve_color, Function.comp_apply]    congr 1    conv_lhs => enter[1]; rw [hpr]    exact Fin.succ_succAbove_predAbove (hpr ▸ hne x)