case inl
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : ↑castSucc a < b
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)

case inr
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₂ : b ≤ ↑castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
obtain h₁ | h₂ := lt_or_le (castSucc a) b
case inl.h
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : ↑castSucc a < b
⊢ ↑castSucc (succ a) < succ b

case inl.h
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : ↑castSucc a < b
⊢ ↑castSucc (succ a) < succ b
case inl
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : ↑castSucc a < b
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
rw [Fin.predAbove_above _ _ h₁, Fin.succ_pred, Fin.predAbove_above, Fin.pred_succ]
no goals
case inl.h
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : ↑castSucc a < b
⊢ ↑castSucc (succ a) < succ b

case inl.h
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₁ : ↑castSucc a < b
⊢ ↑castSucc (succ a) < succ b
simpa only [lt_iff_val_lt_val, coe_castSucc, val_succ, add_lt_add_iff_right] using
  h₁
case inr.zero
n m : ℕ
a : Fin zero
b : Fin (zero + 1)
h₂ : b ≤ ↑castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)

case inr.succ
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
case inr
n✝ m n : ℕ
a : Fin n
b : Fin (n + 1)
h₂ : b ≤ ↑castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
cases' n with n
case inr.zero.h
n m : ℕ
a : Fin zero
b : Fin (zero + 1)
h₂ : b ≤ ↑castSucc a
⊢ False
case inr.zero
n m : ℕ
a : Fin zero
b : Fin (zero + 1)
h₂ : b ≤ ↑castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
exfalso
no goals
case inr.zero.h
n m : ℕ
a : Fin zero
b : Fin (zero + 1)
h₂ : b ≤ ↑castSucc a
⊢ False
exact not_lt_zero' a.is_lt
case inr.succ
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ castPred (succ b) = succ (castPred b)
case inr.succ
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ predAbove (succ a) (succ b) = succ (predAbove a b)
rw [Fin.predAbove_below a b h₂,
  Fin.predAbove_below a.succ b.succ
    (by
      simpa only [le_iff_val_le_val, val_succ, coe_castSucc, add_le_add_iff_right] using h₂)]
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
case inr.succ
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ castPred (succ b) = succ (castPred b)
ext
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
h₀ : ↑b < n + 1
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
have h₀ : (b : ℕ) < n + 1 := by
  simp only [le_iff_val_le_val, coe_castSucc] at h₂
  simpa only [lt_succ_iff] using h₂.trans a.is_le
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
h₀ : ↑b < n + 1
h₁ : ↑(succ b) < n + 2
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
h₀ : ↑b < n + 1
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
have h₁ : (b.succ : ℕ) < n + 2 := by
  rw [← Nat.succ_lt_succ_iff] at h₀
  simpa only [val_succ] using h₀
no goals
case inr.succ.h
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
h₀ : ↑b < n + 1
h₁ : ↑(succ b) < n + 2
⊢ ↑(castPred (succ b)) = ↑(succ (castPred b))
simp only [coe_castPred b h₀, coe_castPred b.succ h₁, val_succ]
no goals
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ succ b ≤ ↑castSucc (succ a)
simpa only [le_iff_val_le_val, val_succ, coe_castSucc, add_le_add_iff_right] using h₂
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : ↑b ≤ ↑a
⊢ ↑b < n + 1
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
⊢ ↑b < n + 1
simp only [le_iff_val_le_val, coe_castSucc] at h₂
no goals
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : ↑b ≤ ↑a
⊢ ↑b < n + 1
simpa only [lt_succ_iff] using h₂.trans a.is_le
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
h₀ : Nat.succ ↑b < Nat.succ (n + 1)
⊢ ↑(succ b) < n + 2
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
h₀ : ↑b < n + 1
⊢ ↑(succ b) < n + 2
rw [← Nat.succ_lt_succ_iff] at h₀
no goals
n✝ m n : ℕ
a : Fin (Nat.succ n)
b : Fin (Nat.succ n + 1)
h₂ : b ≤ ↑castSucc a
h₀ : Nat.succ ↑b < Nat.succ (n + 1)
⊢ ↑(succ b) < n + 2
simpa only [val_succ] using h₀