awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ Prime n → n.properDivisors = {1}

Tactic:
fun h => Prime.properDivisors h

Premises used: Nat.Prime.properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ Prime n → n.properDivisors = {1}

Tactic:
exact fun h => Prime.properDivisors h

Premises used: Nat.Prime.properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
zero : Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 1 ↔ Prime 0
succ : ∀ (n : ℕ), Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ↔ Prime (n + 1)
⊢ Eq (α := ℕ) (∑ x ∈ n.properDivisors, x) 1 ↔ Prime n

Tactic:
rcases n with - | n
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 1 ↔ Prime 0

Tactic:
simp [Nat.not_prime_zero]

Premises used: Nat.not_prime_zero
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
succ : Eq (α := ℕ) (∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x) 1 ↔ Prime (HAdd.hAdd (α := ℕ) 0 1)
succ₁ : ∀ (n : ℕ), Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ Prime (n + 1 + 1)
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ↔ Prime (n + 1)

Tactic:
cases n
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ Eq (α := ℕ) (∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x) 1 ↔ Prime (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp [Nat.not_prime_one]

Premises used: Nat.not_prime_one
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
succ : Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ (n + 1 + 1).properDivisors = {1}
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ Prime (n + 1 + 1)

Tactic:
rw [← properDivisors_eq_singleton_one_iff_prime]

Premises used: Nat.properDivisors_eq_singleton_one_iff_prime
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ (n + 1 + 1).properDivisors = {1}

Tactic:
⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩

Premises used: Eq.rec, Finset.sum_singleton, Iff.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
succ : ∀ (h : Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1), (n + 1 + 1).properDivisors = {1}
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ (n + 1 + 1).properDivisors = {1}

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1
succ : {1} = (n + 1 + 1).properDivisors
⊢ (n + 1 + 1).properDivisors = {1}

Tactic:
rw [@eq_comm (Finset ℕ) _ _]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1
⊢ {1} = (n + 1 + 1).properDivisors

Tactic:
apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

Premises used: Iff.mpr, Nat.one_mem_properDivisors_iff_one_lt, Nat.succ_lt_succ, Finset.singleton_subset_iff, Nat.eq_properDivisors_of_subset_of_sum_eq_sum, Finset.sum_singleton, Nat.succ_pos, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k x : ℕ
rw : (∃ (x_1 : ℕ), (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j
⊢ x ∈ (p ^ k).properDivisors ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j

Tactic:
rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]

Premises used: exists_and_right, Nat.mem_properDivisors, Nat.dvd_prime_pow
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k x : ℕ
simp : (∃ x_1 ≤ k, x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j < k, x = p ^ j
⊢ (∃ (x_1 : ℕ), (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j

Tactic:
simp only [exists_prop, and_assoc]

Premises used: exists_prop, and_assoc
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k x : ℕ
h : ∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
⊢ (∃ x_1 ≤ k, x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j < k, x = p ^ j

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k x a : ℕ
h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k → a < k ∧ x = p ^ a
h₁ : a < k ∧ x = p ^ a → a ≤ k ∧ x = p ^ a ∧ x < p ^ k
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k x a : ℕ
h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k
h₁ : ∀ (_h_left : a ≤ k) (h_right : p ^ a < p ^ k), a < k ∧ p ^ a = p ^ a
⊢ a < k ∧ x = p ^ a

Tactic:
rcases h with ⟨_h_left, rfl, h_right⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : p ^ a < p ^ k
⊢ a < k

Tactic:
rw [Nat.pow_lt_pow_iff_right pp.one_lt] at h_right

Premises used: Nat.Prime.one_lt, Nat.pow_lt_pow_iff_right
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : a < k
⊢ a < k ∧ p ^ a = p ^ a

Tactic:
⟨h_right, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : a < k
⊢ a < k ∧ p ^ a = p ^ a

Tactic:
exact ⟨h_right, rfl⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k x a : ℕ
h : a < k ∧ x = p ^ a
h₁ : ∀ (h_left : a < k), a ≤ k ∧ p ^ a = p ^ a ∧ p ^ a < p ^ k
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k

Tactic:
rcases h with ⟨h_left, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
h : a ≤ k ∧ p ^ a = p ^ a ∧ a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ p ^ a < p ^ k

Tactic:
rw [Nat.pow_lt_pow_iff_right pp.one_lt]

Premises used: Nat.Prime.one_lt, Nat.pow_lt_pow_iff_right
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ a < k

Tactic:
simp [h_left, le_of_lt]

Premises used: le_of_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k : ℕ
h : ∀ (a : ℕ), a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range k)
⊢ (p ^ k).properDivisors = map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range k)

Tactic:
ext a
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
h : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a
⊢ a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range k)

Tactic:
simp only [mem_properDivisors, mem_map, mem_range, Function.Embedding.coeFn_mk]

Premises used: Finset.mem_range, Function.Embedding.coeFn_mk, Nat.mem_properDivisors, Finset.mem_map
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).properDivisors ↔ ∃ (j : ℕ) (_ : j < k), a = p ^ j

Tactic:
have := mem_properDivisors_prime_pow pp k (x := a)
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ (p ^ k).properDivisors ↔ ∃ (j : ℕ) (_ : j < k), a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ (j : ℕ) (_ : j < k), a = p ^ j

Tactic:
rw [mem_properDivisors] at this

Premises used: Nat.mem_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ (j : ℕ) (_ : j < k), a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ (p ^ k).properDivisors, f x) (∏ x ∈ range k, f (p ^ x))

Tactic:
simp [h, properDivisors_prime_pow]

Premises used: Nat.properDivisors_prime_pow
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ (p ^ k).divisors, f x) (∏ x ∈ range (k + 1), f (p ^ x))

Tactic:
simp [h, divisors_prime_pow]

Premises used: Nat.divisors_prime_pow
-- Module: Mathlib.NumberTheory.Divisors
Goal:
M : Type u_1
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
rw :
  Eq.{u_1 + 1} (α := M)
    (∏ x ∈ n.divisors,
      f (({ toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } : (a : ℕ) → ℕ × ℕ) x).1
        (({ toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } : (a : ℕ) → ℕ × ℕ) x).2)
    (∏ i ∈ n.divisors, f i (n / i))
⊢ Eq.{u_1 + 1} (α := M) (∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2) (∏ i ∈ n.divisors, f i (n / i))

Tactic:
rw [← map_div_right_divisors, Finset.prod_map]

Premises used: Nat.map_div_right_divisors, Finset.prod_map
-- Module: Mathlib.NumberTheory.Divisors
Goal:
M : Type u_1
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ Eq.{u_1 + 1} (α := M)
    (∏ x ∈ n.divisors,
      f (({ toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } : (a : ℕ) → ℕ × ℕ) x).1
        (({ toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } : (a : ℕ) → ℕ × ℕ) x).2)
    (∏ i ∈ n.divisors, f i (n / i))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
M : Type u_1
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
rw :
  Eq.{u_1 + 1} (α := M)
    (∏ x ∈ n.divisorsAntidiagonal,
      f (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).1
        (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).2)
    (∏ i ∈ n.divisors, f (n / i) i)
⊢ Eq.{u_1 + 1} (α := M) (∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2) (∏ i ∈ n.divisors, f (n / i) i)

Tactic:
rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]

Premises used: Nat.map_swap_divisorsAntidiagonal, Finset.prod_map
-- Module: Mathlib.NumberTheory.Divisors
Goal:
M : Type u_1
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ Eq.{u_1 + 1} (α := M)
    (∏ x ∈ n.divisorsAntidiagonal,
      f (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).1
        (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).2)
    (∏ i ∈ n.divisors, f (n / i) i)

Tactic:
prod_divisorsAntidiagonal fun i j => f j i

Premises used: Nat.prod_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.Divisors
Goal:
M : Type u_1
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ Eq.{u_1 + 1} (α := M)
    (∏ x ∈ n.divisorsAntidiagonal,
      f (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).1
        (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).2)
    (∏ i ∈ n.divisors, f (n / i) i)

Tactic:
exact prod_divisorsAntidiagonal fun i j => f j i

Premises used: Nat.prod_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.primeFactors = {p ∈ n.divisors | Prime p}

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
simp_rw : {p ∈ {p ∈ n.divisors | Prime p} | p ∣ m} = {p ∈ m.divisors | Prime p}
simp_rw₁ : {p ∈ {p ∈ n.divisors | p ∣ m} | Prime p} = {p ∈ m.divisors | Prime p}
⊢ {p ∈ n.primeFactors | p ∣ m} = m.primeFactors

Tactic:
simp_rw [primeFactors_eq_to_filter_divisors_prime, filter_comm,
    divisors_filter_dvd_of_dvd hn hmn]

Premises used: Nat.primeFactors_eq_to_filter_divisors_prime, Nat.divisors_filter_dvd_of_dvd, Finset.filter_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
pos : ∀ (hn : n = 0), image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
neg : ∀ (hn : ¬n = 0), image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
⊢ image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n = 0
⊢ image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
neg : ∀ (a : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a ↔ a ∈ n.divisors
⊢ image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors

Tactic:
ext a
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
neg : Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a → a ∈ n.divisors
neg₁ : a ∈ n.divisors → Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a ↔ a ∈ n.divisors

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
neg : (∃ a_1 ∈ n.divisors, n / a_1 = a) → a ∈ n.divisors
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a → a ∈ n.divisors

Tactic:
rw [mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∈ n.divisors
hx2 : n / x = a
neg : ∀ (hx1 : x ∣ n ∧ n ≠ 0) (hx2 : n / x = a), a ∣ n ∧ n ≠ 0
⊢ a ∈ n.divisors

Tactic:
rw [mem_divisors] at *

Premises used: Nat.mem_divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n ∧ n ≠ 0

Tactic:
⟨?_, hn⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
neg : a ∣ n
⊢ a ∣ n ∧ n ≠ 0

Tactic:
refine ⟨?_, hn⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
neg : n / x ∣ n
⊢ a ∣ n

Tactic:
rw [← hx2]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ n / x ∣ n

Tactic:
div_dvd_of_dvd hx1.1

Premises used: And.left, Nat.div_dvd_of_dvd
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ n / x ∣ n

Tactic:
exact div_dvd_of_dvd hx1.1

Premises used: And.left, Nat.div_dvd_of_dvd
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
neg : a ∣ n ∧ n ≠ 0 → ∃ a_2 ∈ n.divisors, n / a_2 = a
⊢ a ∈ n.divisors → Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a

Tactic:
rw [mem_divisors, mem_image]

Premises used: Finset.mem_image, Nat.mem_divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
h1 : a ∣ n
⊢ ∃ a_1 ∈ n.divisors, n / a_1 = a

Tactic:
⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩

Premises used: Iff.mpr, Nat.mem_divisors, HDiv.hDiv, And.intro, Exists.intro, Nat.div_dvd_of_dvd, Nat.div_div_self
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
h1 : a ∣ n
⊢ ∃ a_1 ∈ n.divisors, n / a_1 = a

Tactic:
exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
pos : ∀ (hn : n = 0), ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
neg : ∀ (hn : ¬n = 0), ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
neg : ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f
neg₁ : Set.InjOn (HDiv.hDiv n) (↑n.divisors : Set ℕ)
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
rw [← prod_image]

Premises used: Finset.prod_image
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ x ∈ n.divisors, f x = f x

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f

Tactic:
exact prod_congr (image_div_divisors_eq_divisors n) (by simp)

Premises used: Nat.image_div_divisors_eq_divisors, Finset.prod_congr
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ (↑n.divisors : Set ℕ)
y : ℕ
hy : y ∈ (↑n.divisors : Set ℕ)
h : n / x = n / y
neg : ∀ (hx : x ∣ n ∧ n ≠ 0) ⦃y : ℕ⦄ (hy : y ∣ n ∧ n ≠ 0) (h : n / x = n / y), x = y
⊢ x = y

Tactic:
rw [mem_coe, mem_divisors] at hx hy

Premises used: Nat.mem_divisors, Finset.mem_coe
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y

Tactic:
(div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Premises used: Nat.div_eq_iff_eq_of_dvd_dvd, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y

Tactic:
exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Premises used: Nat.div_eq_iff_eq_of_dvd_dvd, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℕ
hab : a.Coprime b
simp : ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
⊢ Disjoint (filter IsPrimePow a.divisors) (filter IsPrimePow b.divisors)

Tactic:
simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]

Premises used: Nat.mem_divisors, and_imp, Finset.mem_filter, Finset.disjoint_left, not_and
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℕ
hab : a.Coprime b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False

Tactic:
hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)

Premises used: Nat.eq_one_of_dvd_coprimes, IsPrimePow.ne_one
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℕ
hab : a.Coprime b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False

Tactic:
exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)

Premises used: Nat.eq_one_of_dvd_coprimes, IsPrimePow.ne_one
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
h : ∀ (n1 n2 : ℕ), (n1, n2) ∈ n.divisorsAntidiagonal ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
⊢ n.divisorsAntidiagonal = {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
ext ⟨n1, n2⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
h : (n1, n2).1 * (n1, n2).2 = n ∧ n ≠ 0 ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
⊢ (n1, n2) ∈ n.divisorsAntidiagonal ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
rw [Nat.mem_divisorsAntidiagonal]

Premises used: Nat.mem_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
h : n1 * n2 = n ∧ ¬n = 0 ↔ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
⊢ (n1, n2).1 * (n1, n2).2 = n ∧ n ≠ 0 ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
simp only [ne_eq, Finset.mem_filter, Finset.mem_product, Finset.mem_Ioc]

Premises used: ne_eq, Finset.mem_filter, Finset.mem_Ioc, Finset.mem_product
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
h : n1 * n2 = n ∧ ¬n = 0 → ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
h₁ : ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n → n1 * n2 = n ∧ ¬n = 0
⊢ n1 * n2 = n ∧ ¬n = 0 ↔ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
h : ((0 < n1 ∧ n1 ≤ n1 * n2) ∧ 0 < n2 ∧ n2 ≤ n1 * n2) ∧ n1 * n2 = n1 * n2
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n1 * n2

Tactic:
grw [← hn]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
h : (0 < n1 ∧ 1 ≤ n2) ∧ 0 < n2 ∧ 1 ≤ n1
⊢ ((0 < n1 ∧ n1 ≤ n1 * n2) ∧ 0 < n2 ∧ n2 ≤ n1 * n2) ∧ n1 * n2 = n1 * n2

Tactic:
simp (disch := lia) only [le_mul_iff_one_le_right, le_mul_iff_one_le_left, and_true]

Premises used: and_true, le_mul_iff_one_le_right, le_mul_iff_one_le_left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ (0 < n1 ∧ 1 ≤ n2) ∧ 0 < n2 ∧ 1 ≤ n1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
hn1 : 0 < n1 ∧ n1 ≤ N
hn2 : 0 < n2 ∧ n2 ≤ N
hn3 : n1 * n2 = n
⊢ n1 * n2 = n ∧ ¬n = 0

Tactic:
⟨hn3, n_ne_zero⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
hn1 : 0 < n1 ∧ n1 ≤ N
hn2 : 0 < n2 ∧ n2 ≤ N
hn3 : n1 * n2 = n
⊢ n1 * n2 = n ∧ ¬n = 0

Tactic:
exact ⟨hn3, n_ne_zero⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
q : ℕ
hq : 1 < q
k_1 : ℕ
k : ℕ × ℕ
hk :
  k ∈
    map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ instAddMonoid _ k_1)
obtain :
  ∀ (i : ℕ × ℕ) (hi : i ∈ @antidiagonal _ instAddMonoid _ k_1)
    (hk :
      Membership.mem (α := ℕ × ℕ)
        (map
          ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
            { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
          (@antidiagonal _ instAddMonoid _ k_1))
        (({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
                { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ } :
              (a : ℕ × ℕ) → ℕ × ℕ)
            i :
          ℕ × ℕ)),
    Membership.mem (α := ℕ × ℕ) (q ^ k_1).divisorsAntidiagonal
      (({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
              { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ } :
            (a : ℕ × ℕ) → ℕ × ℕ)
          i :
        ℕ × ℕ)
⊢ k ∈ (q ^ k_1).divisorsAntidiagonal

Tactic:
obtain ⟨i, hi, rfl⟩ := Finset.mem_map.mp hk

Premises used: Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
q : ℕ
hq : 1 < q
k : ℕ
i : ℕ × ℕ
hi : i ∈ @antidiagonal _ instAddMonoid _ k
hk :
  Membership.mem (α := ℕ × ℕ)
    (map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ instAddMonoid _ k))
    (({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ } :
          (a : ℕ × ℕ) → ℕ × ℕ)
        i :
      ℕ × ℕ)
⊢ Membership.mem (α := ℕ × ℕ) (q ^ k).divisorsAntidiagonal
    (({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ } :
          (a : ℕ × ℕ) → ℕ × ℕ)
        i :
      ℕ × ℕ)

Tactic:
simp [Nat.mem_divisorsAntidiagonal, ← Finset.mem_antidiagonal.mp hi, pow_add, ne_zero_of_lt hq]

Premises used: ne_zero_of_lt, Nat.mem_divisorsAntidiagonal, pow_add, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
xy : ℤ × ℤ
x y z_1 z : ℤ
s : Finset ℕ := z.natAbs.divisors
⊢ Disjoint (map Nat.castEmbedding s) (map negNatCast s)

Tactic:
simp +contextual [s, disjoint_left, Eq.comm, forall_comm (β := _ = _)]

Premises used: forall_comm, Eq.comm, Finset.disjoint_left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
xy : ℤ × ℤ
x y z : ℤ
n : ℕ
s : Finset (ℕ × ℕ) := n.divisorsAntidiagonal
⊢ Disjoint (map (Function.Embedding.prodMap Nat.castEmbedding Nat.castEmbedding) s)
    (map (negNatCast.prodMap negNatCast) s)

Tactic:
simp +contextual [s, disjoint_left, eq_comm]

Premises used: eq_comm, Finset.disjoint_left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
xy : ℤ × ℤ
x y z : ℤ
n : ℕ
s : Finset (ℕ × ℕ) := (n + 1).divisorsAntidiagonal
⊢ Disjoint (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) s)
    (map (negNatCast.prodMap Nat.castEmbedding) s)

Tactic:
simp +contextual [s, disjoint_left, eq_comm, forall_comm (α := _ * _ = _)]

Premises used: forall_comm, eq_comm, Finset.disjoint_left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
x z : ℤ
⊢ x ∈ z.divisors ↔ ∃ y ∈ z.natAbs.divisors, (↑y : ℤ) = x ∨ -(↑y : ℤ) = x

Tactic:
simp [← exists_or, ← and_or_left, divisors]

Premises used: Int.divisors, and_or_left, exists_or
-- Module: Mathlib.NumberTheory.Divisors
Goal:
x z : ℤ
y : ℕ
⊢ (↑y : ℤ) = x ∨ -(↑y : ℤ) = x ↔ y = x.natAbs

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
x z : ℤ
⊢ x ∈ z.divisors ↔ x ∣ z ∧ z ≠ 0

Tactic:
simp [mem_divisors_iff_natAbs_mem_divisors_natAbs]

Premises used: Int.mem_divisors_iff_natAbs_mem_divisors_natAbs
-- Module: Mathlib.NumberTheory.Divisors
Goal:
x z : ℤ
h : x ∈ z.divisors
⊢ x ∣ z

Tactic:
(mem_divisors.mp h).1

Premises used: Int.mem_divisors, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
x z : ℤ
h : x ∈ z.divisors
⊢ z ≠ 0

Tactic:
(mem_divisors.mp h).2

Premises used: Int.mem_divisors, And.right, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
⊢ 1 ∈ z.divisors ↔ z ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
⊢ -1 ∈ z.divisors ↔ z ≠ 0

Tactic:
simp