awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n a b : ℕ
c : a < b
d : ℕ × ℕ
h :
  (have y := n / a;
    if a * y = n then some (a, y) else none) =
    some d
ha : ℕ × ℕ
h' :
  (have y := n / b;
    if b * y = n then some (b, y) else none) =
    some ha
rw : ∀ (h : a * (n / a) = n ∧ (a, n / a) = d) (ha : ℕ × ℕ) (h' : b * (n / b) = n ∧ (b, n / b) = ha), d.1 < ha.1
⊢ d.1 < ha.1

Tactic:
rw [Option.ite_none_right_eq_some, Option.some.injEq] at h h'

Premises used: Option.some.injEq, Option.ite_none_right_eq_some
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n a b : ℕ
c : a < b
d : ℕ × ℕ
h : a * (n / a) = n ∧ (a, n / a) = d
ha : ℕ × ℕ
h' : b * (n / b) = n ∧ (b, n / b) = ha
⊢ d.1 < ha.1

Tactic:
simpa [← h.right, ← h'.right]

Premises used: And.right
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
inl : List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)
inr : ∀ (hn : n ≠ 0), List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n ≠ 0
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
(List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ ?_

Premises used: Nat.divisorsAntidiagonalList, List.SortedLT.pairwise, Nat.one_ne_zero, List.Pairwise.filterMap, List.sortedLT_range'
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n ≠ 0
inr :
  ∀ (a a' : ℕ),
    a < a' →
      ∀ (b : ℕ × ℕ),
        (have y := n / a;
            if a * y = n then some (a, y) else none) =
            some b →
          ∀ (b' : ℕ × ℕ),
            (have y := n / a';
                if a' * y = n then some (a', y) else none) =
                some b' →
              b.2 > b'.2
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
refine (List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ ?_

Premises used: List.SortedLT.pairwise, Nat.one_ne_zero, List.Pairwise.filterMap, List.sortedLT_range'
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n ≠ 0
inr :
  ∀ (a a' : ℕ),
    a < a' →
      ∀ (a_2 b : ℕ),
        a * (n / a) = n → a = a_2 → n / a = b → ∀ (a b_1 : ℕ), a' * (n / a') = n → a' = a → n / a' = b_1 → b_1 < b
⊢ ∀ (a a' : ℕ),
    a < a' →
      ∀ (b : ℕ × ℕ),
        (have y := n / a;
            if a * y = n then some (a, y) else none) =
            some b →
          ∀ (b' : ℕ × ℕ),
            (have y := n / a';
                if a' * y = n then some (a', y) else none) =
                some b' →
              b.2 > b'.2

Tactic:
simp only [Option.ite_none_right_eq_some, Option.some.injEq, gt_iff_lt,
    and_imp, Prod.forall, Prod.mk.injEq]

Premises used: and_imp, Option.some.injEq, Prod.mk.injEq, gt_iff_lt, Prod.forall, Option.ite_none_right_eq_some
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n ≠ 0
a b : ℕ
hab : a < b
ha : a * (n / a) = n
hb : b * (n / b) = n
inr inr₁ inr₂ inr₃ : a < b
⊢ n / b < n / a

Tactic:
rwa [Nat.div_lt_div_left hn ⟨_, hb.symm⟩ ⟨_, ha.symm⟩]

Premises used: Nat.div_lt_div_left, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ (List.map Prod.fst n.divisorsAntidiagonalList).SortedLT

Tactic:
(List.pairwise_map.mpr <| pairwise_divisorsAntidiagonalList_fst).sortedLT

Premises used: Iff.mpr, Nat.pairwise_divisorsAntidiagonalList_fst, List.pairwise_map, List.Pairwise.sortedLT
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ (List.map Prod.snd n.divisorsAntidiagonalList).SortedGT

Tactic:
(List.pairwise_map.mpr <| pairwise_divisorsAntidiagonalList_snd).sortedGT

Premises used: Iff.mpr, List.Pairwise.sortedGT, List.pairwise_map, Nat.pairwise_divisorsAntidiagonalList_snd
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ ∀ (a : ℕ × ℕ), ¬a.1 < a.1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.divisorsAntidiagonal.val = (↑n.divisorsAntidiagonalList : Multiset (ℕ × ℕ))

Tactic:
rfl

Premises used: Multiset.filterMap, Nat.divisorsAntidiagonalList, Multiset.ofList, Nat.pred, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
a : ℕ × ℕ
rw : a ∈ n.divisorsAntidiagonalList.toFinset ↔ a.1 * a.2 = n ∧ n ≠ 0
rw₁ : a ∈ n.divisorsAntidiagonal ↔ a.1 * a.2 = n ∧ n ≠ 0
rw₂ rw₃ : a.1 * a.2 = n ∧ n ≠ 0 ↔ a.1 * a.2 = n ∧ n ≠ 0
⊢ a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0

Tactic:
rw [← List.mem_toFinset, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonal]

Premises used: List.mem_toFinset, Nat.mem_divisorsAntidiagonal, Nat.toFinset_divisorsAntidiagonalList
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
a : ℕ × ℕ
⊢ a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ Std.Asymm fun (x1 x2 : ℕ × ℕ) ↦ x1.2 < x2.2

Tactic:
have : Std.Asymm (α := ℕ × ℕ) (·.snd < ·.snd) := ⟨fun _ _ ↦ lt_asymm⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
this : Std.Asymm fun (x1 x2 : ℕ × ℕ) ↦ x1.2 < x2.2
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList

Tactic:
List.Perm.eq_of_pairwise' pairwise_divisorsAntidiagonalList_snd.reverse
    (pairwise_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id) ?_

Premises used: Nat.pairwise_divisorsAntidiagonalList_fst, id, List.Perm.eq_of_pairwise', List.Pairwise.map, Nat.pairwise_divisorsAntidiagonalList_snd, List.Pairwise.reverse
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
this : Std.Asymm fun (x1 x2 : ℕ × ℕ) ↦ x1.2 < x2.2
refine : n.divisorsAntidiagonalList.reverse.Perm (List.map Prod.swap n.divisorsAntidiagonalList)
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList

Tactic:
refine List.Perm.eq_of_pairwise' pairwise_divisorsAntidiagonalList_snd.reverse
    (pairwise_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id) ?_

Premises used: id, List.Perm.eq_of_pairwise', List.Pairwise.map, Nat.pairwise_divisorsAntidiagonalList_snd, List.Pairwise.reverse
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
this : Std.Asymm fun (x1 x2 : ℕ × ℕ) ↦ x1.2 < x2.2
⊢ n.divisorsAntidiagonalList.reverse.Perm (List.map Prod.swap n.divisorsAntidiagonalList)

Tactic:
simp [List.reverse_perm', List.perm_ext_iff_of_nodup nodup_divisorsAntidiagonalList
    (nodup_divisorsAntidiagonalList.map Prod.swap_injective), mul_comm]

Premises used: List.reverse_perm', List.Nodup.map, mul_comm, List.perm_ext_iff_of_nodup, Prod.swap_injective, Nat.nodup_divisorsAntidiagonalList
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 * p.2 = n

Tactic:
obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp

Premises used: Nat.mem_divisorsAntidiagonal, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 * p.2 = n
⊢ n ≠ 0

Tactic:
obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp

Premises used: Nat.mem_divisorsAntidiagonal, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 * p.2 = n
hp₂ : n ≠ 0
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0

Tactic:
mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)

Premises used: Eq.rec, Iff.mp, Eq.symm, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 * p.2 = n
hp₂ : n ≠ 0
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0

Tactic:
exact mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 ≠ 0

Tactic:
(ne_zero_of_mem_divisorsAntidiagonal hp).1

Premises used: Nat.ne_zero_of_mem_divisorsAntidiagonal, And.left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.2 ≠ 0

Tactic:
(ne_zero_of_mem_divisorsAntidiagonal hp).2

Premises used: Nat.ne_zero_of_mem_divisorsAntidiagonal, And.right
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
zero : n ∈ divisors 0 → n ≤ 0
succ : ∀ (m : ℕ), n ∈ (m + 1).divisors → n ≤ m + 1
⊢ n ∈ m.divisors → n ≤ m

Tactic:
rcases m with - | m
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n ∈ divisors 0 → n ≤ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
succ : n ∣ m + 1 → n ≤ m + 1
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Tactic:
simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]

Premises used: and_true, Nat.mem_divisors, Ne, Nat.succ_ne_zero, not_false_iff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
⊢ n ∣ m + 1 → n ≤ m + 1

Tactic:
Nat.le_of_dvd (Nat.succ_pos m)

Premises used: Nat.succ_pos, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
⊢ n ∣ m + 1 → n ≤ m + 1

Tactic:
exact Nat.le_of_dvd (Nat.succ_pos m)

Premises used: Nat.succ_pos, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
⊢ m.divisors ⊆ n.divisors

Tactic:
Finset.subset_iff.2 fun _x hx => Nat.mem_divisors.mpr ⟨(Nat.mem_divisors.mp hx).1.trans h, hzero⟩

Premises used: Iff.mpr, Nat.mem_divisors, And.left, Finset.subset_iff, And.intro, Iff.mp, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
a : n.divisors ⊆ Ico 1 (n + 1)
⊢ #n.divisors ≤ #(Ico 1 (n + 1))

Tactic:
apply card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.divisors ⊆ Ico 1 (n + 1)

Tactic:
simp only [divisors, filter_subset]

Premises used: Finset.filter_subset, Nat.divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
rw : n + 1 - 1 = n
rw₁ rw₂ : n = n
⊢ #(Ico 1 (n + 1)) = n

Tactic:
rw [card_Ico, add_tsub_cancel_right]

Premises used: Nat.card_Ico, add_tsub_cancel_right
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
hx : x ∈ m.divisors
⊢ x ∈ n.properDivisors

Tactic:
Nat.mem_properDivisors.2
      ⟨(Nat.mem_divisors.1 hx).1.trans h,
        lt_of_le_of_lt (divisor_le hx)
          (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩

Premises used: Iff.mpr, lt_of_le_of_lt, Nat.mem_divisors, And.left, And.intro, Iff.mp, Nat.mem_properDivisors, Nat.divisor_le, lt_of_le_of_ne, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
hx : x ∈ m.divisors
⊢ x ∈ n.properDivisors

Tactic:
exact
    Nat.mem_properDivisors.2
      ⟨(Nat.mem_divisors.1 hx).1.trans h,
        lt_of_le_of_lt (divisor_le hx)
          (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩

Premises used: Iff.mpr, lt_of_le_of_lt, Nat.mem_divisors, And.left, And.intro, Iff.mp, Nat.mem_properDivisors, Nat.divisor_le, lt_of_le_of_ne, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
h : ∀ (k : ℕ), k ∈ {d ∈ n.divisors | d ∣ m} ↔ k ∈ m.divisors
⊢ {d ∈ n.divisors | d ∣ m} = m.divisors

Tactic:
ext k
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
h : (k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0
⊢ k ∈ {d ∈ n.divisors | d ∣ m} ↔ k ∈ m.divisors

Tactic:
simp_rw [mem_filter, mem_divisors]

Premises used: Nat.mem_divisors, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ (k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0

Tactic:
⟨fun ⟨_, hkm⟩ ↦ ⟨hkm, ne_zero_of_dvd_ne_zero hn hm⟩, fun ⟨hk, _⟩ ↦ ⟨⟨hk.trans hm, hn⟩, hk⟩⟩

Premises used: _private.0.Nat.divisors_filter_dvd_of_dvd.match_2, Dvd.dvd, _private.0.Nat.divisors_filter_dvd_of_dvd.match_1, Ne, And, And.intro, Iff.intro, ne_zero_of_dvd_ne_zero, OfNat.ofNat, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ (k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0

Tactic:
exact ⟨fun ⟨_, hkm⟩ ↦ ⟨hkm, ne_zero_of_dvd_ne_zero hn hm⟩, fun ⟨hk, _⟩ ↦ ⟨⟨hk.trans hm, hn⟩, hk⟩⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : ∀ (a : ℕ), a ∈ divisors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a
⊢ divisors 0 = ∅

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a : ℕ
⊢ a ∈ divisors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : ∀ (a : ℕ), a ∈ properDivisors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a
⊢ properDivisors 0 = ∅

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a : ℕ
⊢ a ∈ properDivisors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.divisors.Nonempty
hn : n = 0
m : ℕ
hm : m ∈ n.divisors
⊢ False

Tactic:
simp [hn] at hm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
contrapose! : n.divisors.Nonempty ↔ n ≠ 0
⊢ n.divisors = ∅ ↔ n = 0

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.divisors.Nonempty ↔ n ≠ 0

Tactic:
nonempty_divisors

Premises used: Nat.nonempty_divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.divisors.Nonempty ↔ n ≠ 0

Tactic:
exact nonempty_divisors

Premises used: Nat.nonempty_divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.properDivisors ⊆ n.divisors

Tactic:
filter_subset_filter _ <| Ico_subset_Ico_right n.le_succ

Premises used: Finset.Ico_subset_Ico_right, Finset.filter_subset_filter, Set.Mem, setOf, Nat.le_succ
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : ∀ (a : ℕ), a ∈ divisors 1 ↔ Membership.mem (γ := Finset ℕ) {1} a
⊢ divisors 1 = {1}

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a : ℕ
⊢ a ∈ divisors 1 ↔ Membership.mem (γ := Finset ℕ) {1} a

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
rw : Eq (α := Finset ℕ) ({d ∈ Ico 1 1 | d ∣ 1}) ∅
rw₁ : Eq (α := Finset ℕ) ({d ∈ ∅ | d ∣ 1}) ∅
rw₂ rw₃ : Eq (α := Finset ℕ) ∅ ∅
⊢ properDivisors 1 = ∅

Tactic:
rw [properDivisors, Ico_self, filter_empty]

Premises used: Finset.Ico_self, Finset.filter_empty, Nat.properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
h : m ∈ n.divisors
zero : ∀ (h : 0 ∈ n.divisors), LT.lt (α := ℕ) 0 0
succ : ∀ (n_1 : ℕ) (h : n_1 + 1 ∈ n.divisors), 0 < n_1 + 1
⊢ 0 < m

Tactic:
cases m
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : 0 ∈ n.divisors
⊢ n = 0 ∧ n ≠ 0

Tactic:
rw [mem_divisors, zero_dvd_iff (a := n)] at h

Premises used: Nat.mem_divisors, zero_dvd_iff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ LT.lt (α := ℕ) 0 0

Tactic:
cases h.2 h.1

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n n_1 : ℕ
h : n_1 + 1 ∈ n.divisors
⊢ 0 < n_1 + 1

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
h : m ∈ n.properDivisors
⊢ 0 < m

Tactic:
pos_of_mem_divisors (properDivisors_subset_divisors h)

Premises used: Nat.properDivisors_subset_divisors, Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
rw : 1 ∣ n ∧ 1 < n ↔ 1 < n
rw₁ rw₂ : 1 < n ↔ 1 < n
⊢ 1 ∈ n.properDivisors ↔ 1 < n

Tactic:
rw [mem_properDivisors, and_iff_right (one_dvd _)]

Premises used: and_iff_right, one_dvd, Nat.mem_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.divisors.sup id = n

Tactic:
le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_

Premises used: Finset.sup_le, le_antisymm, Nat.divisor_le
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
refine : n ≤ n.divisors.sup id
⊢ n.divisors.sup id = n

Tactic:
refine le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_

Premises used: Finset.sup_le, le_antisymm, Nat.divisor_le
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
inl : 0 ≤ (divisors 0).sup id
inr : ∀ (hn : n ≠ 0), n ≤ n.divisors.sup id
⊢ n ≤ n.divisors.sup id

Tactic:
rcases Decidable.eq_or_ne n 0 with rfl | hn

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ 0 ≤ (divisors 0).sup id

Tactic:
apply zero_le

Premises used: Nat.zero_le
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
Finset.le_sup (f := id) <| mem_divisors_self n hn

Premises used: Nat.mem_divisors_self, Finset.le_sup
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
exact Finset.le_sup (f := id) <| mem_divisors_self n hn

Premises used: Nat.mem_divisors_self, Finset.le_sup
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
h : m ∈ n.properDivisors
⊢ 1 < n

Tactic:
lt_of_le_of_lt (pos_of_mem_properDivisors h) (mem_properDivisors.1 h).2

Premises used: Nat.pos_of_mem_properDivisors, lt_of_le_of_lt, And.right, Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
h : m ∈ n.properDivisors
⊢ m ∣ n

Tactic:
obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h

Premises used: Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
⊢ m < n

Tactic:
obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h

Premises used: Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
rwa : m * 1 < n
rwa₁ rwa₂ rwa₃ rwa₄ : m < n
⊢ 1 < n / m

Tactic:
rwa [Nat.lt_div_iff_mul_lt' h_dvd, mul_one]

Premises used: Nat.lt_div_iff_mul_lt', mul_one
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
hn : n ≠ 0
⊢ m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k

Tactic:
⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩

Premises used: Nat.one_lt_div_of_mem_properDivisors, HDiv.hDiv, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
hn : n ≠ 0
refine_1 : ∀ (h : m ∈ n.properDivisors), n = m * (n / m)
refine_2 : (∃ k > 1, n = m * k) → m ∈ n.properDivisors
⊢ m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k

Tactic:
refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

Tactic:
(Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm

Premises used: And.left, Iff.mp, Nat.mem_properDivisors, Eq.symm, Nat.mul_div_cancel'
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

Tactic:
exact (Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm

Premises used: And.left, Iff.mp, Nat.mem_properDivisors, Eq.symm, Nat.mul_div_cancel'
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m k : ℕ
hk : k > 1
hn : m * k ≠ 0
⊢ m ≠ 0 ∧ k ≠ 0

Tactic:
rw [mul_ne_zero_iff] at hn

Premises used: mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩

Premises used: Iff.mpr, Nat.pos_of_ne_zero, And.left, And.intro, Exists.intro, Nat.mem_properDivisors, lt_mul_of_one_lt_right, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
exact mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩

Premises used: Iff.mpr, Nat.pos_of_ne_zero, And.left, And.intro, Exists.intro, Nat.mem_properDivisors, lt_mul_of_one_lt_right, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.properDivisors.Nonempty ↔ 1 < n

Tactic:
⟨fun ⟨_m, hm⟩ ↦ one_lt_of_mem_properDivisors hm, fun hn ↦
    ⟨1, one_mem_properDivisors_iff_one_lt.2 hn⟩⟩

Premises used: Iff.mpr, Nat.one_mem_properDivisors_iff_one_lt, LT.lt, Iff.intro, Exists.intro, Nat.one_lt_of_mem_properDivisors, _private.0.Nat.nonempty_properDivisors.match_1, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
contrapose! : n.properDivisors.Nonempty ↔ 1 < n
⊢ n.properDivisors = ∅ ↔ n ≤ 1

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.properDivisors.Nonempty ↔ 1 < n

Tactic:
nonempty_properDivisors

Premises used: Nat.nonempty_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.properDivisors.Nonempty ↔ 1 < n

Tactic:
exact nonempty_properDivisors

Premises used: Nat.nonempty_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : ∀ (a : ℕ × ℕ), a ∈ divisorsAntidiagonal 0 ↔ Membership.mem (γ := Finset (ℕ × ℕ)) ∅ a
⊢ divisorsAntidiagonal 0 = ∅

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a : ℕ × ℕ
⊢ a ∈ divisorsAntidiagonal 0 ↔ Membership.mem (γ := Finset (ℕ × ℕ)) ∅ a

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : ∀ (a : ℕ × ℕ), a ∈ divisorsAntidiagonal 1 ↔ Membership.mem (γ := Finset (ℕ × ℕ)) {(1, 1)} a
⊢ divisorsAntidiagonal 1 = {(1, 1)}

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a : ℕ × ℕ
⊢ a ∈ divisorsAntidiagonal 1 ↔ Membership.mem (γ := Finset (ℕ × ℕ)) {(1, 1)} a

Tactic:
simp [mul_eq_one, Prod.ext_iff]

Premises used: Prod.ext_iff, mul_eq_one
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
x : ℕ × ℕ
rw : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x ∈ n.divisorsAntidiagonal
rw₁ : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
rw₂ : x.swap.2 * x.swap.1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
rw₃ rw₄ : (x.2, x.1).2 * (x.2, x.1).1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal

Tactic:
rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]

Premises used: Nat.mem_divisorsAntidiagonal, mul_comm, Prod.swap
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n x y : ℕ
hn : n ≠ 0
⊢ (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
rw [mem_divisorsAntidiagonal] at h

Premises used: Nat.mem_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.1 ∈ n.divisors

Tactic:
simp [Dvd.intro _ h.1, h.2]

Premises used: Dvd.intro, And.right, And.left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.2 ∈ n.divisors

Tactic:
simp [Dvd.intro_left _ h.1, h.2]

Premises used: Dvd.intro_left, And.right, And.left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
rw : Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) = (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal

Tactic:
rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm,
    Set.image_swap_eq_preimage_swap]

Premises used: Set.image_swap_eq_preimage_swap, Equiv.coe_toEmbedding, Finset.coe_inj, Equiv.coe_prodComm, Finset.coe_map
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h :
  ∀ (x : ℕ × ℕ), x ∈ Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) ↔ x ∈ (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
⊢ Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) = (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) ↔ x ∈ (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))

Tactic:
swap_mem_divisorsAntidiagonal

Premises used: Nat.swap_mem_divisorsAntidiagonal, Set.Mem, setOf, Multiset.Mem, Set.preimage
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) ↔ x ∈ (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))

Tactic:
exact swap_mem_divisorsAntidiagonal

Premises used: Nat.swap_mem_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : ∀ (a : ℕ), a ∈ image Prod.fst n.divisorsAntidiagonal ↔ a ∈ n.divisors
⊢ image Prod.fst n.divisorsAntidiagonal = n.divisors

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n a : ℕ
⊢ a ∈ image Prod.fst n.divisorsAntidiagonal ↔ a ∈ n.divisors

Tactic:
simp [Dvd.dvd, @eq_comm _ n (_ * _)]

Premises used: Dvd.dvd, eq_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
rw :
  image (Function.comp (β := ℕ × ℕ) Prod.snd (⇑(Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ))
      n.divisorsAntidiagonal =
    n.divisors
⊢ image Prod.snd n.divisorsAntidiagonal = n.divisors

Tactic:
rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]

Premises used: Nat.map_swap_divisorsAntidiagonal, Finset.map_eq_image, Finset.image_image