case zero
n m : ℕ
a : Fin (zero + 1)
⊢ ↑(a - 1) = if a = 0 then zero else ↑a - 1

case succ
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
⊢ ↑(a - 1) = if a = 0 then Nat.succ n✝ else ↑a - 1
n✝ m n : ℕ
a : Fin (n + 1)
⊢ ↑(a - 1) = if a = 0 then n else ↑a - 1
cases n
case succ.inl
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : a = 0
⊢ ↑(a - 1) = Nat.succ n✝

case succ.inr
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ ↑(a - 1) = ↑a - 1
case succ
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
⊢ ↑(a - 1) = if a = 0 then Nat.succ n✝ else ↑a - 1
split_ifs with h
case succ.inr.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ Nat.succ n✝ + 1 ≤ ↑a + (n✝ + 1)
case succ.inr
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ ↑(a - 1) = ↑a - 1
rw [sub_eq_add_neg, val_add_eq_ite, coe_neg_one, if_pos, add_comm, add_tsub_add_eq_tsub_left]
case succ.inr.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ Nat.succ n✝ + 1 ≤ n✝ + 1 + ↑a
case succ.inr.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ Nat.succ n✝ + 1 ≤ ↑a + (n✝ + 1)
conv_rhs => rw [add_comm]
case succ.inr.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ ↑a ≠ 0
case succ.inr.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ Nat.succ n✝ + 1 ≤ n✝ + 1 + ↑a
rw [add_le_add_iff_left, Nat.one_le_iff_ne_zero]
no goals
case succ.inr.hc
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : ¬a = 0
⊢ ↑a ≠ 0
rwa [Fin.ext_iff] at h
no goals
case zero
n m : ℕ
a : Fin (zero + 1)
⊢ ↑(a - 1) = if a = 0 then zero else ↑a - 1
simp
no goals
case succ.inl
n m n✝ : ℕ
a : Fin (Nat.succ n✝ + 1)
h : a = 0
⊢ ↑(a - 1) = Nat.succ n✝
simp [h]