case a.mk
n d nd : ℕ
⊢ (d, nd) ∈
      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) ↔
    (d, nd) ∈ divisorsAntidiagonal n
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) =
    divisorsAntidiagonal n
ext ⟨d, nd⟩
case a.mk
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
case a.mk
n d nd : ℕ
⊢ (d, nd) ∈
      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) ↔
    (d, nd) ∈ divisorsAntidiagonal n
simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors,
  Prod.ext_iff, exists_prop, and_left_comm, exists_eq_left]
case a.mk.mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0

case a.mk.mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
case a.mk
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
constructor
case a.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0
case a.mk.mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0
rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩
case a.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0
case a.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0
rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
no goals
case a.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0
exact ⟨rfl, hn⟩
case a.mk.mpr.intro
d nd : ℕ
hn : d * nd ≠ 0
⊢ (d ∣ d * nd ∧ d * nd ≠ 0) ∧ d * nd / d = nd
case a.mk.mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
rintro ⟨rfl, hn⟩
no goals
case a.mk.mpr.intro
d nd : ℕ
hn : d * nd ≠ 0
⊢ (d ∣ d * nd ∧ d * nd ≠ 0) ∧ d * nd / d = nd
exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩