awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) ∣ a * b

Tactic:
exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)

Premises used: Nat.prod_primeFactors_dvd, mul_dvd_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
d : ℕ := a.gcd b
inl : φ 0 * φ b ≤ φ (0 * b)
inr : ∀ (ha0 : a > 0), φ a * φ b ≤ φ (a * b)
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
rcases eq_zero_or_pos a with (rfl | ha0)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
⊢ 0 < d

Tactic:
have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
apply : φ a * φ b * d ≤ φ (a * b) * d
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
apply le_of_mul_le_mul_right _ hd0

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
grw : φ (a.gcd b) * φ (a * b) ≤ φ (a * b) * d
grw₁ : φ (a * b) * φ (a.gcd b) ≤ φ (a * b) * d
grw₂ grw₃ : φ (a * b) * d ≤ φ (a * b) * d
⊢ φ a * φ b * d ≤ φ (a * b) * d

Tactic:
grw [← totient_gcd_mul_totient_mul a b, mul_comm, d.totient_le]

Premises used: Nat.totient_le, Nat.totient_gcd_mul_totient_mul, mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
inl : ∀ (h : 0 ∣ b), φ 0 ∣ φ b
inr : ∀ (ha0 : a ≠ 0), φ a ∣ φ b
⊢ φ a ∣ φ b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b

Tactic:
simp [zero_dvd_iff.1 h]

Premises used: zero_dvd_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
inr : ∀ (h : a ∣ 0), φ a ∣ φ 0
inr₁ : ∀ (hb0 : b ≠ 0), φ a ∣ φ b
⊢ φ a ∣ φ b

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a.primeFactors ⊆ b.primeFactors

Tactic:
have hab' := primeFactors_mono h hb0
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
inr :
  Dvd.dvd (α := ℕ) (a.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
    (b.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
⊢ φ a ∣ φ b

Tactic:
rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]

Premises used: Nat.totient_eq_prod_factorization
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ Dvd.dvd (α := ℕ) (a.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
    (b.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))

Tactic:
Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl

Premises used: mul_dvd_mul, Finsupp.prod_dvd_prod_of_subset_of_dvd, dvd_rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
inr :
  ∀ p ∈ a.factorization.support,
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
      p ^ HSub.hSub (α := ℕ) (β := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ Dvd.dvd (α := ℕ) (a.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
    (b.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))

Tactic:
refine Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl

Premises used: Finsupp.prod_dvd_prod_of_subset_of_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
p : ℕ
h_1 : p ∈ a.factorization.support
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)

Premises used: Iff.mpr, pow_dvd_pow, Nat.factorization_le_iff_dvd, tsub_le_tsub_right, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
p : ℕ
h_1 : p ∈ a.factorization.support
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)

Premises used: Iff.mpr, pow_dvd_pow, Nat.factorization_le_iff_dvd, tsub_le_tsub_right, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Totient
Goal:
p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n

Tactic:
have h1 := totient_gcd_mul_totient_mul p n
-- Module: Mathlib.Data.Nat.Totient
Goal:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n
⊢ φ p * φ (p * n) = φ p * (φ n * p)

Tactic:
rw [gcd_eq_left h, mul_assoc] at h1

Premises used: mul_assoc, Nat.gcd_eq_left
-- Module: Mathlib.Data.Nat.Totient
Goal:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n

Tactic:
simpa [(totient_pos.2 hp.pos).ne', mul_comm] using h1

Premises used: Iff.mpr, Nat.Prime.pos, LT.lt.ne', mul_comm, Nat.totient_pos
-- Module: Mathlib.Data.Nat.Totient
Goal:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
rw : p.Coprime n
⊢ φ (p * n) = (p - 1) * φ n

Tactic:
rw [totient_mul _, totient_prime hp]

Premises used: Nat.totient_prime, Nat.totient_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n

Tactic:
simpa [h] using coprime_or_dvd_of_prime hp n

Premises used: Nat.coprime_or_dvd_of_prime
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : Even n
⊢ φ (2 * n) = 2 * φ n

Tactic:
totient_mul_of_prime_of_dvd prime_two hn.two_dvd

Premises used: Nat.totient_mul_of_prime_of_dvd, Nat.prime_two, Even.two_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : Odd n
rw : HSub.hSub (α := ℕ) 2 1 * φ n = φ n
rw₁ : 1 * φ n = φ n
rw₂ rw₃ : φ n = φ n
⊢ φ (2 * n) = φ n

Tactic:
rw [totient_mul_of_prime_of_not_dvd prime_two hn.not_two_dvd_nat, Nat.add_one_sub_one 1, one_mul]

Premises used: Nat.add_one_sub_one, Nat.totient_mul_of_prime_of_not_dvd, Nat.prime_two, Odd.not_two_dvd_nat, OfNat.ofNat, one_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
pos : ∀ (ha : a = 0), a = b ∨ 2 * a = b
neg : ∀ (ha : ¬a = 0), a = b ∨ 2 * a = b
⊢ a = b ∨ 2 * a = b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : a = 0
⊢ b = 0

Tactic:
rw [ha, totient_zero, eq_comm, totient_eq_zero] at h'

Premises used: Nat.totient_zero, eq_comm, Nat.totient_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : a = 0
h'₁ : b = 0
⊢ a = 0

Tactic:
rw [ha, totient_zero, eq_comm, totient_eq_zero] at h'

Premises used: Nat.totient_zero, eq_comm, Nat.totient_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : b = 0
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
simp [ha, h']
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
pos : ∀ (hb : b = 0), a = b ∨ 2 * a = b
neg : ∀ (hb : ¬b = 0), a = b ∨ 2 * a = b
⊢ a = b ∨ 2 * a = b

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
⊢ a = 0

Tactic:
rw [hb, totient_zero, totient_eq_zero] at h'

Premises used: Nat.totient_zero, Nat.totient_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
h'₁ : a = 0
⊢ ¬a = 0

Tactic:
rw [hb, totient_zero, totient_eq_zero] at h'

Premises used: Nat.totient_zero, Nat.totient_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
h'₁ : a = 0
ha₁ : ¬a = 0
⊢ b = 0

Tactic:
rw [hb, totient_zero, totient_eq_zero] at h'

Premises used: Nat.totient_zero, Nat.totient_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
False.elim (ha h')

Premises used: False.elim
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
exact False.elim (ha h')

Premises used: False.elim
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : ¬b = 0
neg : ∀ (c : ℕ) (h' : φ a = φ (a * c)) (hb : ¬a * c = 0), a = a * c ∨ 2 * a = a * c
⊢ a = b ∨ 2 * a = b

Tactic:
obtain ⟨c, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
this : a.Coprime c
⊢ c = 1 ∨ c = 2

Tactic:
rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'

Premises used: Iff.mpr, Iff.not, Nat.mul_eq_left, Nat.totient_mul, eq_comm, Nat.totient_eq_zero, Nat.totient_eq_one_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
this : a.Coprime c
h'₁ : c = 1 ∨ c = 2
⊢ ¬a * c = 0

Tactic:
rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'

Premises used: Iff.mpr, Iff.not, Nat.mul_eq_left, Nat.totient_mul, eq_comm, Nat.totient_eq_zero, Nat.totient_eq_one_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
this : a.Coprime c
h'₁ : c = 1 ∨ c = 2
hb₁ : ¬a * c = 0
⊢ a.Coprime c

Tactic:
rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'

Premises used: Iff.mpr, Iff.not, Nat.mul_eq_left, Nat.totient_mul, eq_comm, Nat.totient_eq_zero, Nat.totient_eq_one_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : c = 1 ∨ c = 2
hb : ¬a * c = 0
this : a.Coprime c
inl : ∀ (hb : ¬a * 1 = 0) (this : a.Coprime 1), a = a * 1 ∨ 2 * a = a * 1
inr : ∀ (hb : ¬a * 2 = 0) (this : a.Coprime 2), a = a * 2 ∨ 2 * a = a * 2
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
obtain rfl | rfl := h'

Premises used: rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
hb : ¬a * 1 = 0
this : a.Coprime 1
⊢ a = a * 1 ∨ 2 * a = a * 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
hb : ¬a * 2 = 0
this : a.Coprime 2
⊢ a = a * 2 ∨ 2 * a = a * 2

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
neg : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
suffices a.Coprime c by
    rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'
    obtain rfl | rfl := h'
    · simp
    · simp [mul_comm]
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
⊢ a.Coprime c

Tactic:
coprime_of_dvd fun p hp hap ↦ ?_

Premises used: Nat.coprime_of_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
neg : ∀ (p : ℕ) (hp : Prime p) (hap : p ∣ a), ¬p ∣ c
⊢ a.Coprime c

Tactic:
refine coprime_of_dvd fun p hp hap ↦ ?_

Premises used: Nat.coprime_of_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ φ a = φ (p * a * d)

Tactic:
rw [← mul_assoc, mul_comm a] at h'

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
h'₁ : φ a = φ (p * a * d)
⊢ ¬a * (p * d) = 0

Tactic:
rw [← mul_assoc, mul_comm a] at h'

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
h'₁ : φ a = φ (p * a * d)
hb₁ : ¬a * (p * d) = 0
⊢ φ a < φ (p * a * d)

Tactic:
rw [← mul_assoc, mul_comm a] at h'

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (p * a * d)
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False

Tactic:
h'.not_lt this

Premises used: Eq.not_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (p * a * d)
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False

Tactic:
exact h'.not_lt this

Premises used: Eq.not_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
neg : φ a < φ (p * a * d)
⊢ False

Tactic:
suffices a.totient < (p * a * d).totient by
    rw [← mul_assoc, mul_comm a] at h'
    exact h'.not_lt this
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
neg : φ a < φ (a * p * d)
⊢ φ a < φ (p * a * d)

Tactic:
rw [mul_comm p]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (a * p * d)

Tactic:
lt_of_lt_of_le ?_ (Nat.le_of_dvd ?_ (totient_dvd_of_dvd ⟨d, rfl⟩))

Premises used: Nat.totient_dvd_of_dvd, Exists.intro, Nat.le_of_dvd, rfl, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
neg : φ a < φ (a * p)
neg₁ : 0 < φ (a * p * d)
⊢ φ a < φ (a * p * d)

Tactic:
refine lt_of_lt_of_le ?_ (Nat.le_of_dvd ?_ (totient_dvd_of_dvd ⟨d, rfl⟩))

Premises used: Nat.totient_dvd_of_dvd, Exists.intro, Nat.le_of_dvd, rfl, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
neg : 1 < p
neg₁ : 0 < φ a
⊢ φ a < φ (a * p)

Tactic:
rw [mul_comm, totient_mul_of_prime_of_dvd hp hap, Nat.lt_mul_iff_one_lt_left]

Premises used: Nat.totient_mul_of_prime_of_dvd, Nat.lt_mul_iff_one_lt_left, mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 1 < p

Tactic:
hp.one_lt

Premises used: Nat.Prime.one_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 1 < p

Tactic:
exact hp.one_lt

Premises used: Nat.Prime.one_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 0 < φ a

Tactic:
totient_pos.mpr <| pos_of_ne_zero ha

Premises used: Iff.mpr, pos_of_ne_zero, Nat.totient_pos
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 0 < φ a

Tactic:
exact totient_pos.mpr <| pos_of_ne_zero ha

Premises used: Iff.mpr, pos_of_ne_zero, Nat.totient_pos
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
rwa rwa₁ rwa₂ rwa₃ : a * (p * d) ≠ 0
⊢ a * p * d ≠ 0

Tactic:
rwa [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ 0 < φ (a * p * d)

Tactic:
exact totient_pos.mpr <| zero_lt_of_ne_zero (by rwa [mul_assoc])

Premises used: Iff.mpr, Nat.zero_lt_of_ne_zero, Nat.totient_pos
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
pos : ∀ (ha' : a = 0), a = b
neg : ∀ (ha' : ¬a = 0), a = b
⊢ a = b

Tactic:
by_cases ha' : a = 0
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : a = 0
⊢ b = 0

Tactic:
rw [ha', totient_zero, eq_comm, totient_eq_zero] at h'

Premises used: Nat.totient_zero, eq_comm, Nat.totient_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : a = 0
h'₁ : b = 0
⊢ a = 0

Tactic:
rw [ha', totient_zero, eq_comm, totient_eq_zero] at h'

Premises used: Nat.totient_zero, eq_comm, Nat.totient_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : b = 0
ha' pos : a = 0
pos₁ pos₂ : Eq (α := ℕ) 0 0
⊢ a = b

Tactic:
rw [h', ha']
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
⊢ a = b

Tactic:
(eq_or_eq_of_totient_eq_totient h h').resolve_right fun h ↦ ?_

Premises used: Nat.eq_or_eq_of_totient_eq_totient, Or.resolve_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
neg : ∀ (h : 2 * a = b), False
⊢ a = b

Tactic:
refine (eq_or_eq_of_totient_eq_totient h h').resolve_right fun h ↦ ?_

Premises used: Nat.eq_or_eq_of_totient_eq_totient, Or.resolve_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h_1 : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
h : 2 * a = b
⊢ Eq (α := ℕ) 2 1

Tactic:
rw [← h, totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha), eq_comm,
    mul_eq_right (totient_eq_zero.not.mpr ha')] at h'

Premises used: Iff.mpr, Nat.totient_mul_of_prime_of_dvd, Iff.not, Nat.mul_eq_right, eq_comm, Nat.totient_eq_zero, Nat.prime_two, Iff.mp, even_iff_two_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h_1 : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
h : 2 * a = b
h'₁ : Eq (α := ℕ) 2 1
⊢ ¬a = 0

Tactic:
rw [← h, totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha), eq_comm,
    mul_eq_right (totient_eq_zero.not.mpr ha')] at h'

Premises used: Iff.mpr, Nat.totient_mul_of_prime_of_dvd, Iff.not, Nat.mul_eq_right, eq_comm, Nat.totient_eq_zero, Nat.prime_two, Iff.mp, even_iff_two_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h_1 : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
h : 2 * a = b
h'₁ : Eq (α := ℕ) 2 1
ha'₁ : ¬a = 0
⊢ 2 * a = b

Tactic:
rw [← h, totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha), eq_comm,
    mul_eq_right (totient_eq_zero.not.mpr ha')] at h'

Premises used: Iff.mpr, Nat.totient_mul_of_prime_of_dvd, Iff.not, Nat.mul_eq_right, eq_comm, Nat.totient_eq_zero, Nat.prime_two, Iff.mp, even_iff_two_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
h_1 : a ∣ b
ha : Even a
h' : Eq (α := ℕ) 2 1
ha' : ¬a = 0
h : 2 * a = b
⊢ False

Tactic:
lia
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
rw : p ^ (k - 1) ≤ p ^ (k - 1) * (k * (p - 1))
⊢ p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))

Tactic:
rw [mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ p ^ (k - 1) ≤ p ^ (k - 1) * (k * (p - 1))

Tactic:
le_mul_of_one_le_right (Nat.zero_le _) ?_

Premises used: Nat.zero_le, le_mul_of_one_le_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
refine : 1 ≤ k * (p - 1)
⊢ p ^ (k - 1) ≤ p ^ (k - 1) * (k * (p - 1))

Tactic:
refine le_mul_of_one_le_right (Nat.zero_le _) ?_

Premises used: Nat.zero_le, le_mul_of_one_le_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ 1 ≤ k * (p - 1)

Tactic:
Right.one_le_mul hk <| Nat.le_sub_one_of_lt <| hp.one_lt

Premises used: Nat.Prime.one_lt, Right.one_le_mul, Nat.le_sub_one_of_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ 1 ≤ k * (p - 1)

Tactic:
exact Right.one_le_mul hk <| Nat.le_sub_one_of_lt <| hp.one_lt

Premises used: Nat.Prime.one_lt, Right.one_le_mul, Nat.le_sub_one_of_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))

Tactic:
have h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1)) := by
    rw [mul_left_comm]
    refine le_mul_of_one_le_right (Nat.zero_le _) ?_
    exact Right.one_le_mul hk <| Nat.le_sub_one_of_lt <| hp.one_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
simp_rw : p ^ (k * (p ^ (k - 1) * (p - 1))) / p ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
⊢ (p ^ k) ^ φ (p ^ k) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
simp_rw [Nat.totient_prime_pow hp hk, Nat.primeFactors_prime_pow hk.ne' hp, Finset.prod_singleton,
    Nat.mul_div_left _ (Nat.sub_pos_of_lt hp.one_lt), ← pow_mul]

Premises used: Finset.prod_singleton, Nat.Prime.one_lt, Nat.totient_prime_pow, Nat.sub_pos_of_lt, pow_mul, LT.lt.ne', Nat.mul_div_left, Nat.primeFactors_prime_pow
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
rw : p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1))) / p ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
rw [Nat.pow_div h hp.pos]

Premises used: Nat.Prime.pos, Nat.pow_div
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
simp_rw :
  p ^ (k * (p ^ (k - 1) * p) - k * p ^ (k - 1) - p ^ (k - 1)) =
    p ^ (p ^ (k - 1) * (p * k) - p ^ (k - 1) * k - p ^ (k - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
simp_rw [Nat.sub_mul, one_mul, Nat.mul_sub, mul_one]

Premises used: Nat.sub_mul, mul_one, Nat.mul_sub, one_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * p) - k * p ^ (k - 1) - p ^ (k - 1)) =
    p ^ (p ^ (k - 1) * (p * k) - p ^ (k - 1) * k - p ^ (k - 1))

Tactic:
ring_nf
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 0 < n
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
have := Nat.prod_primeFactors_dvd n
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 0 < n
this : ∏ p ∈ n.primeFactors, p ∣ n
⊢ ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n

Tactic:
rw [← Nat.pow_dvd_pow_iff (Nat.totient_pos.mpr hn).ne', ← Finset.prod_pow] at this

Premises used: Iff.mpr, Nat.pow_dvd_pow_iff, LT.lt.ne', Nat.totient_pos, Finset.prod_pow
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
dvd_trans (Finset.prod_dvd_prod_of_dvd _ _ fun p hp ↦ ?_) this

Premises used: Finset.prod_dvd_prod_of_dvd, dvd_trans
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
refine : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), p ^ (φ n / (p - 1)) ∣ p ^ φ n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
refine dvd_trans (Finset.prod_dvd_prod_of_dvd _ _ fun p hp ↦ ?_) this

Premises used: Finset.prod_dvd_prod_of_dvd, dvd_trans
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ p ^ (φ n / (p - 1)) ∣ p ^ φ n

Tactic:
Nat.pow_dvd_pow p <| Nat.div_le_self _ _

Premises used: Nat.div_le_self, Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 0 < n
this : ∏ x ∈ n.primeFactors, x ^ φ n ∣ n ^ φ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ p ^ (φ n / (p - 1)) ∣ p ^ φ n

Tactic:
exact Nat.pow_dvd_pow p <| Nat.div_le_self _ _

Premises used: Nat.div_le_self, Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)
rw : WellFounded (α := Upto p) (InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ))
⊢ WellFounded (Upto.GT p)

Tactic:
rw [this]
-- Module: Mathlib.Data.Nat.Upto
Goal:
p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ)
⊢ WellFounded (α := Upto p) (InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) fun (y : Upto p) ↦ x - (↑y : ℕ))

Tactic:
(measure _).wf

Premises used: InvImage, WellFoundedRelation.wf