succAbove and predAbove lemmas

Stream: Is there code for X?

[Wrenna Robson]

In an application I am considering, I needed the following:

lemma nonsense {i k} {j : Fin (m + 3)} :
(j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k) :=  sorry

Now, experimenting with various test values seems to indicate that this is true. But I can't find a proof for it. Can anyone suggest a good approach, or lemmas that I am missing (or that we are missing) that makes it more straightforward?

I also had this, which I could prove, but not nicely.

lemma succAbove_succAbove_predAbove {i : Fin (m + 1)} {j : Fin (m + 2)} :
(j.succAbove i).succAbove (i.predAbove j) = j := by
by_cases h : Fin.castSucc i < j
· rw [Fin.succAbove_below _ _ h, Fin.succAbove_predAbove (ne_of_lt h).symm]
· rw [not_lt] at h
  rw [Fin.succAbove_above _ _ h, Fin.predAbove_below _ _ h, Fin.succAbove_below] <;>
  rw [Fin.castSucc_castPred (lt_of_le_of_lt h (Fin.castSucc_lt_last _))]
  exact lt_of_le_of_lt h (Fin.castSucc_lt_succ _)

[Eric Wieser]

Proof by ugly case bash:

import Mathlib.Data.Fin.Basic
import Mathlib.Tactic

lemma nonsense {i k} {j : Fin (m + 3)} :
    (j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k) := by
  ext
  simp [Fin.succAbove, Fin.predAbove, Fin.lt_def]
  split_ifs <;> simp_all
  · linarith
  · have : (1 : ℕ) ≤ j := by linarith
    rw [lt_tsub_iff_left_of_le this] at *
    linarith
  · linarith
  · linarith
  · linarith
  · linarith
  · linarith
  · linarith

[Eric Wieser]

(the sorry is easy)

[Wrenna Robson]

Weird that one step needs that sorry to work

[Eric Wieser]

linarith is bad at Nat subtraction

[Wrenna Robson]

So am I so I can't complain too much

[Wrenna Robson]

-- FIN LEMMA
lemma succAbove_succAbove_predAbove_succAbove_eq_succAbove_succAbove {j : Fin (m + 2)} :
(j.succAbove i).succAbove ((i.predAbove j).succAbove k) = j.succAbove (i.succAbove k) := by
  ext
  dsimp [Fin.succAbove, Fin.predAbove]
  rcases j.succAbove_lt_ge i with (h | h) <;>
  [ simp only [h, dite_true, Fin.coe_pred, ge_iff_le, lt_tsub_iff_right, Fin.dite_val,
    Fin.coe_castSucc, Fin.val_succ] ;
    simp only [h.not_lt, dite_false, Fin.coe_castLT, Fin.dite_val, Fin.coe_castSucc, Fin.val_succ]] <;>
  rcases i.succAbove_lt_ge k with (h₂ | h₂) <;>
  simp only [Fin.lt_def, Fin.le_def, Fin.coe_castSucc] at h h₂
  · simp only [h, ite_true, h₂]
    by_cases h₃ : (k + 1 : ℕ) < (j : ℕ)
    · simp only [Nat.lt_of_succ_lt, h₃, ite_true, h₂]
    · exfalso
      rw [not_lt] at h₃
      exact (Nat.le_of_lt_succ (lt_of_lt_of_le h h₃)).not_lt h₂
  · simp only [h, ite_true, ite_false, h₂.not_lt]
    by_cases h₃ : (k + 1 : ℕ) < (j : ℕ) <;>
    simp only [h₃, ite_true, ite_false, ite_eq_right_iff, self_eq_add_right]
    · exact h₂.not_lt
    · rw [not_lt] at h₃
      exact (lt_of_lt_of_le h h₃).le.not_lt
  · simp only [h₂, ite_true, ite_false, h.not_lt]
    by_cases h₃ : (k : ℕ) < (j : ℕ) <;>
    simp only [h₃, ite_true, ite_false, ite_eq_left_iff, not_lt, add_right_eq_self]
    · exact h₂.le.not_lt
    · rw [Nat.succ_le_succ_iff]
      exact h₂.not_le
  · simp only [h.not_lt, ite_false]
    by_cases h₃ : (k : ℕ) < (j : ℕ) <;>
    simp only [h₃, Nat.succ_lt_succ_iff, h₂.not_lt, ite_false, ite_true]
    · exfalso
      exact h₃.not_le (h.trans h₂)
    · rw [not_lt] at h₃
      simp only [(h₃.trans (Nat.le_succ _)).not_lt, ite_false]

[Wrenna Robson]

This is just the ugly case bash with extra steps. But it may be more fertile ground for golfing.