n : ℕ
⊢ Prod.swap ⁻¹' ↑(divisorsAntidiagonal n) = ↑(divisorsAntidiagonal n)
n : ℕ
⊢ map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (divisorsAntidiagonal n) = divisorsAntidiagonal n
rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm,
  Set.image_swap_eq_preimage_swap]
case h
n : ℕ
x✝ : ℕ × ℕ
⊢ x✝ ∈ Prod.swap ⁻¹' ↑(divisorsAntidiagonal n) ↔ x✝ ∈ ↑(divisorsAntidiagonal n)
n : ℕ
⊢ Prod.swap ⁻¹' ↑(divisorsAntidiagonal n) = ↑(divisorsAntidiagonal n)
ext
no goals
case h
n : ℕ
x✝ : ℕ × ℕ
⊢ x✝ ∈ Prod.swap ⁻¹' ↑(divisorsAntidiagonal n) ↔ x✝ ∈ ↑(divisorsAntidiagonal n)
exact swap_mem_divisorsAntidiagonal