-- Mathlib/Order/Fin/Basic.lean
lemma predAbove_right_monotone (p : Fin n) : Monotone p.predAbove := fun a b H => by
  dsimp [predAbove]
  split_ifs with ha hb hb
  all_goals simp only [le_iff_val_le_val, coe_pred]
  · exact pred_le_pred H
  · calc
      _ ≤ _ := Nat.pred_le _
      _ ≤ _ := H
  · exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)
  · exact H

Proof state:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ a.pred ⋯ ≤ b.pred ⋯

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.pred ⋯ ≤ b.castPred ⋯

case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ a.castPred ⋯ ≤ b.pred ⋯

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.castPred ⋯ ≤ b.castPred ⋯

Tactic:
all_goals simp only [le_iff_val_le_val, coe_pred]

Result:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ ↑a - 1 ≤ ↑b - 1

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)

case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Proof state:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

Tactic:
exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)

Result:
no goals

Proof state:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ ↑a - 1 ≤ ↑b - 1

Tactic:
exact pred_le_pred H

Result:
no goals

Proof state:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯) ≤ if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯

Tactic:
split_ifs with ha hb hb

Result:
case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ a.pred ⋯ ≤ b.pred ⋯

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.pred ⋯ ≤ b.castPred ⋯

case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ a.castPred ⋯ ≤ b.pred ⋯

case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.castPred ⋯ ≤ b.castPred ⋯

Proof state:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
exact H

Result:
no goals

Proof state:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ a.castPred ⋯ ≤ b.castPred ⋯

Tactic:
simp only [le_iff_val_le_val, coe_pred]

Result:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Proof state:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ p.predAbove a ≤ p.predAbove b

Tactic:
dsimp [predAbove]

Result:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯) ≤ if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯

Proof state:
case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)

Tactic:
calc
  _ ≤ _ := Nat.pred_le _
  _ ≤ _ := H

Result:
no goals