n : ℕ
⊢ image (Prod.snd ∘ ↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ))) (divisorsAntidiagonal n) = divisors n
n : ℕ
⊢ image Prod.snd (divisorsAntidiagonal n) = divisors n
rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]
no goals
n : ℕ
⊢ image (Prod.snd ∘ ↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ))) (divisorsAntidiagonal n) = divisors n
exact image_fst_divisorsAntidiagonal