obtain ⟨z, hz⟩ : ∃ z, x = (2 * m + 1) + z := exists_add_of_le H
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
⊢ False
case a.intro
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
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
z : ℕ
hz : x = 2 * m + 1 + z
⊢ False