case a
n : ℕ
⊢ map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ))
      (map
        { toFun := fun d => (n / d, d),
          inj' :=
            (_ :
              ∀ (p₁ p₂ : ℕ),
                (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                  ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
        (divisors n)) =
    map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (divisorsAntidiagonal n)
n : ℕ
⊢ map
      { toFun := fun d => (n / d, d),
        inj' :=
          (_ :
            ∀ (p₁ p₂ : ℕ),
              (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
      (divisors n) =
    divisorsAntidiagonal n
apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding
case a
n : ℕ
⊢ map
      (Function.Embedding.trans
        { toFun := fun d => (n / d, d),
          inj' :=
            (_ :
              ∀ (p₁ p₂ : ℕ),
                (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                  ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
        (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
      (divisors n) =
    map
      { toFun := fun d => (d, n / d),
        inj' :=
          (_ :
            ∀ (p₁ p₂ : ℕ),
              (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
      (divisors n)
case a
n : ℕ
⊢ map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ))
      (map
        { toFun := fun d => (n / d, d),
          inj' :=
            (_ :
              ∀ (p₁ p₂ : ℕ),
                (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                  ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
        (divisors n)) =
    map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (divisorsAntidiagonal n)
rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]
no goals
case a
n : ℕ
⊢ map
      (Function.Embedding.trans
        { toFun := fun d => (n / d, d),
          inj' :=
            (_ :
              ∀ (p₁ p₂ : ℕ),
                (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                  ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
        (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
      (divisors n) =
    map
      { toFun := fun d => (d, n / d),
        inj' :=
          (_ :
            ∀ (p₁ p₂ : ℕ),
              (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
      (divisors n)
rfl