case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ ↑(↑rev i) = ↑{ val := a, isLt := (_ : a < Nat.succ n) }
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ ↑rev i = { val := a, isLt := (_ : a < Nat.succ n) }
ext
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ n + 1 - (↑i + 1) = a
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ ↑(↑rev i) = ↑{ val := a, isLt := (_ : a < Nat.succ n) }
dsimp
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ a + ↑i + 1 - (↑i + 1) = a
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ n + 1 - (↑i + 1) = a
conv_lhs =>
  congr
  rw [h]
no goals
case h
n✝ m n a : ℕ
i : Fin (n + 1)
h : n = a + ↑i
⊢ a + ↑i + 1 - (↑i + 1) = a
rw [add_assoc, add_tsub_cancel_right]