unfold_let NN A at *
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
x : ℕ
hx : x ∈ A ∪ f '' NN \ f '' (f '' NN)
⊢ x ∈ NN \ f '' (f '' NN)
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' Set.univ \ f '' (f '' Set.univ)
ab_disjoint : Disjoint (Set.univ \ f '' Set.univ) B
x : ℕ
hx : x ∈ Set.univ \ f '' Set.univ ∪ f '' Set.univ \ f '' (f '' Set.univ)
⊢ x ∈ Set.univ \ f '' (f '' Set.univ)