case zero
a b c : ℕ
⊢ image (fun j => zero - 1 - j) (range zero) = range zero

case succ
a b c n✝ : ℕ
⊢ image (fun j => succ n✝ - 1 - j) (range (succ n✝)) = range (succ n✝)
a b c n : ℕ
⊢ image (fun j => n - 1 - j) (range n) = range n
cases n
no goals
case zero
a b c : ℕ
⊢ image (fun j => zero - 1 - j) (range zero) = range zero
rw [range_zero, image_empty]
case succ
a b c n✝ : ℕ
⊢ Ico (succ n✝ - 1 + 1 - succ n✝) (succ n✝ - 1 + 1 - 0) = Ico 0 (succ n✝)
case succ
a b c n✝ : ℕ
⊢ image (fun j => succ n✝ - 1 - j) (range (succ n✝)) = range (succ n✝)
rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]
no goals
case succ
a b c n✝ : ℕ
⊢ Ico (succ n✝ - 1 + 1 - succ n✝) (succ n✝ - 1 + 1 - 0) = Ico 0 (succ n✝)
simp_rw [succ_sub_succ, tsub_zero, tsub_self]