case zero
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
⊢ range (Nat.zero + 1) \ {0} = image Nat.succ (range Nat.zero)

case succ
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (Nat.succ k + 1) \ {0} = image Nat.succ (range (Nat.succ k))
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
n : ℕ
⊢ range (n + 1) \ {0} = image Nat.succ (range n)
induction' n with k hk
case succ
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (Nat.succ k + 1) \ {0} = image Nat.succ (insert k (range k))
case succ
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (Nat.succ k + 1) \ {0} = image Nat.succ (range (Nat.succ k))
conv_rhs => rw [range_succ]
case succ.h
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ ¬k + 1 ∈ {0}
case succ
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (Nat.succ k + 1) \ {0} = image Nat.succ (insert k (range k))
rw [range_succ, image_insert, ← hk, insert_sdiff_of_not_mem]
no goals
case succ.h
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ ¬k + 1 ∈ {0}
simp
no goals
case zero
α : Type ?u.151859
β : Type ?u.151862
γ : Type ?u.151865
⊢ range (Nat.zero + 1) \ {0} = image Nat.succ (range Nat.zero)
simp