rw [← @Set.toFinset_card _ (A ∪ B) ab_fintype] at h2
case 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)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : Fintype.card ↑(A ∪ B) = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False
case 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)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
h2 : (A ∪ B).toFinset.card = 2 * m + 1
a_fintype : Fintype ↑A
b_fintype : Fintype ↑B
h3 : (A ∪ B).toFinset = A.toFinset ∪ B.toFinset
⊢ False