awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
rw : Fintype.card (ZMod m × ZMod n)ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
rw₁ : Fintype.card ((ZMod m)ˣ × (ZMod n)ˣ) = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
rw₂ rw₃ : Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ

Tactic:
rw [Fintype.card_congr (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).toEquiv,
      Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv, Fintype.card_prod]

Premises used: Fintype.card_congr, RingEquiv.toMulEquiv, ZMod.chineseRemainder, MulEquiv.toEquiv, Fintype.card_prod, Units.mapEquiv, MulEquiv.prodUnits
-- Module: Mathlib.Data.Nat.Totient
Goal:
n d : ℕ
hnd : d ∣ n
inl : ∀ (hnd : 0 ∣ n), φ (n / 0) = #({k ∈ range n | n.gcd k = 0})
inr : ∀ (hd0 : d > 0), φ (n / d) = #({k ∈ range n | n.gcd k = d})
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})

Tactic:
rcases d.eq_zero_or_pos with (rfl | hd0)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = #({k ∈ range n | n.gcd k = 0})

Tactic:
simp [eq_zero_of_zero_dvd hnd]

Premises used: eq_zero_of_zero_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
inr : ∀ (x : ℕ), φ (d * x / d) = #({k ∈ range (d * x) | (d * x).gcd k = d})
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})

Tactic:
rcases hnd with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
inr : φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
⊢ φ (d * x / d) = #({k ∈ range (d * x) | (d * x).gcd k = d})

Tactic:
rw [Nat.mul_div_cancel_left x hd0]

Premises used: Nat.mul_div_cancel_left
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
inr : ∀ (a : ℕ) (ha : a ∈ {a ∈ range x | x.Coprime a}), d * a ∈ {k ∈ range (d * x) | (d * x).gcd k = d}
inr₁ :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ {a ∈ range x | x.Coprime a}) (a₂ : ℕ) (ha₂ : a₂ ∈ {a ∈ range x | x.Coprime a}),
    d * a₁ = d * a₂ → a₁ = a₂
inr₂ : ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ (a : ℕ) (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})

Tactic:
apply Finset.card_bij fun k _ => d * k

Premises used: HMul.hMul, Finset.card_bij
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
inr : ∀ a < x, x.gcd a = 1 → d * a < d * x ∧ (d * x).gcd (d * a) = d
⊢ ∀ (a : ℕ) (ha : a ∈ {a ∈ range x | x.Coprime a}), d * a ∈ {k ∈ range (d * x) | (d * x).gcd k = d}

Tactic:
simp only [mem_filter, mem_range, and_imp, Coprime]

Premises used: Nat.Coprime, and_imp, Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
ha : 0 < d
⊢ d * a < d * x

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
inr : ∀ (a : ℕ) (ha1 : a < x) (ha2 : x.gcd a = 1), (d * x).gcd (d * a) = d
⊢ ∀ a < x, x.gcd a = 1 → d * a < d * x ∧ (d * x).gcd (d * a) = d

Tactic:
refine fun a ha1 ha2 => ⟨by gcongr, ?_⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
inr : d * x.gcd a = d
inr₁ : d * 1 = d
inr₂ inr₃ : d = d
⊢ (d * x).gcd (d * a) = d

Tactic:
rw [gcd_mul_left, ha2, mul_one]

Premises used: Nat.gcd_mul_left, mul_one
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ {a ∈ range x | x.Coprime a}) (a₂ : ℕ) (ha₂ : a₂ ∈ {a ∈ range x | x.Coprime a}),
    d * a₁ = d * a₂ → a₁ = a₂

Tactic:
simp [hd0.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
inr : ∀ b < d * x, (d * x).gcd b = d → ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b
⊢ ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ (a : ℕ) (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b

Tactic:
simp only [mem_filter, mem_range, exists_prop, and_imp]

Premises used: and_imp, Finset.mem_range, exists_prop, Finset.mem_filter
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b < d * x, (d * x).gcd b = d → ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
fun b hb1 hb2 => ?_
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
inr : ∀ (b : ℕ) (hb1 : b < d * x) (hb2 : (d * x).gcd b = d), ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b
⊢ ∀ b < d * x, (d * x).gcd b = d → ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
refine fun b hb1 hb2 => ?_
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
rw : (d * x).gcd b ∣ b
⊢ d ∣ b

Tactic:
rw [← hb2]
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ (d * x).gcd b ∣ b

Tactic:
apply gcd_dvd_right

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ d ∣ b

Tactic:
have : d ∣ b := by
      rw [← hb2]
      apply gcd_dvd_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
this : d ∣ b
inr : ∀ (q : ℕ) (hb1 : d * q < d * x) (hb2 : (d * x).gcd (d * q) = d), ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = d * q
⊢ ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
rcases this with ⟨q, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = d * q

Tactic:
⟨q, ⟨⟨(mul_lt_mul_iff_right₀ hd0).1 hb1, ?_⟩, rfl⟩⟩

Premises used: mul_lt_mul_iff_right₀, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
inr : x.Coprime q
⊢ ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = d * q

Tactic:
refine ⟨q, ⟨⟨(mul_lt_mul_iff_right₀ hd0).1 hb1, ?_⟩, rfl⟩⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
inr : ∀ (hb2 : d * x.gcd q = d), x.Coprime q
inr₁ inr₂ inr₃ inr₄ : ∀ (hb2 : x.gcd q = 1), x.Coprime q
⊢ x.Coprime q

Tactic:
rwa [gcd_mul_left, mul_eq_left hd0.ne'] at hb2

Premises used: Nat.gcd_mul_left, Nat.mul_eq_left, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
inl : (divisors 0).sum φ = 0
inr : ∀ (hn : n > 0), n.divisors.sum φ = n
⊢ n.divisors.sum φ = n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ (divisors 0).sum φ = 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
inr : ∑ d ∈ n.divisors, φ (n / d) = n
⊢ n.divisors.sum φ = n

Tactic:
rw [← sum_div_divisors n φ]

Premises used: Nat.totient, Nat.sum_div_divisors
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
nth_rw : #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
nth_rw 1 [← card_range n]

Premises used: Finset.card_range
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩

Premises used: Iff.mpr, Nat.mem_divisors, LT.lt.ne', Finset.card_eq_sum_card_fiberwise, And.intro
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
refine : ∀ x ∈ (↑(range n) : Set ℕ), n.gcd x ∣ n
⊢ #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩

Premises used: Iff.mpr, Nat.mem_divisors, LT.lt.ne', Finset.card_eq_sum_card_fiberwise, And.intro
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
x : ℕ
h : x ∈ (↑(range n) : Set ℕ)
⊢ n.gcd x ∣ n

Tactic:
apply gcd_dvd_left

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
⊢ n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
have : n = ∑ d ∈ n.divisors, #{k ∈ range n | n.gcd k = d} := by
    nth_rw 1 [← card_range n]
    refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩
    apply gcd_dvd_left
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
inr : Eq (α := ℕ) (∑ d ∈ n.divisors, φ (n / d)) (∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d}))
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Tactic:
nth_rw 3 [this]
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ Eq (α := ℕ) (∑ d ∈ n.divisors, φ (n / d)) (∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d}))

Tactic:
sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)

Premises used: Nat.totient_div_of_dvd, Nat.dvd_of_mem_divisors, Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ Eq (α := ℕ) (∑ d ∈ n.divisors, φ (n / d)) (∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d}))

Tactic:
exact sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)

Premises used: Nat.totient_div_of_dvd, Nat.dvd_of_mem_divisors, Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ n.divisors.sum φ = n

Tactic:
sum_totient _

Premises used: Nat.sum_totient
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
h : ∑ m ∈ range n.succ with m ∣ n, φ m = n.divisors.sum φ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n

Tactic:
convert! sum_totient _ using 1

Premises used: Nat.sum_totient
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
h : Eq (α := ℕ) (∑ a ∈ Ico 0 n.succ, if a ∣ n then φ a else 0) (∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0)
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n.divisors.sum φ

Tactic:
simp only [Nat.divisors, sum_filter, range_eq_Ico]

Premises used: Nat.divisors, Finset.range_eq_Ico, Finset.sum_filter
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
h :
  ((if 0 ∣ n then φ 0 else 0) + ∑ k ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ, if k ∣ n then φ k else 0) =
    ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0
h₁ : 0 < n.succ
⊢ Eq (α := ℕ) (∑ a ∈ Ico 0 n.succ, if a ∣ n then φ a else 0) (∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0)

Tactic:
rw [sum_eq_sum_Ico_succ_bot]

Premises used: Finset.sum_eq_sum_Ico_succ_bot
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ, if k ∣ n then φ k else 0) =
    ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ 0 < n.succ

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
rw :
  {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} =
    {x ∈ range (p ^ (n + 1)) | x ∉ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))}
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} =
    range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))

Tactic:
rw [sdiff_eq_filter]

Premises used: Finset.sdiff_eq_filter
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
H : ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} =
    {x ∈ range (p ^ (n + 1)) | x ∉ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))}

Tactic:
apply filter_congr

Premises used: Finset.filter_congr
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
H : ∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)
⊢ ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))

Tactic:
simp only [mem_range, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
            hp.coprime_iff_not_dvd]

Premises used: Finset.mem_image, not_exists, Finset.mem_range, Nat.succ_pos, Nat.Prime.coprime_iff_not_dvd, Nat.coprime_pow_left_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
H : ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
H₁ : (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ b < p ^ n

Tactic:
rcases h with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
left : b < p ^ n
⊢ b * p < p ^ (n + 1)

Tactic:
rcases h with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
left : b < p ^ n
ha₁ : b * p < p ^ (n + 1)
⊢ ¬p ∣ b * p

Tactic:
rcases h with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n b : ℕ
left : b < p ^ n
ha : b * p < p ^ (n + 1)
hap : ¬p ∣ b * p
⊢ False

Tactic:
hap (dvd_mul_left _ _)

Premises used: dvd_mul_left
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n b : ℕ
left : b < p ^ n
ha : b * p < p ^ (n + 1)
hap : ¬p ∣ b * p
⊢ False

Tactic:
exact hap (dvd_mul_left _ _)

Premises used: dvd_mul_left
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ p * b < p * p ^ n

Tactic:
rw [pow_succ'] at ha

Premises used: Nat.pow_succ'
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
ha₁ : p * b < p * p ^ n
⊢ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)

Tactic:
rw [pow_succ'] at ha

Premises used: Nat.pow_succ'
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False

Tactic:
h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩

Premises used: Nat.zero_le, lt_of_mul_lt_mul_left, And.intro, mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False

Tactic:
exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩

Premises used: Nat.zero_le, lt_of_mul_lt_mul_left, And.intro, mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p

Tactic:
have h1 : Function.Injective (· * p) := mul_left_injective₀ hp.ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
a : ℕ
simp : ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) a → a ∈ range (p ^ (n + 1))

Tactic:
simp only [mem_image, mem_range, exists_imp]

Premises used: Finset.mem_image, Finset.mem_range, exists_imp
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
b : ℕ
h : b < p ^ n
rw : b * p < p ^ n * p
⊢ b * p < p ^ (n + 1)

Tactic:
rw [Nat.pow_succ]

Premises used: Nat.pow_succ
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p

Tactic:
(mul_lt_mul_iff_left₀ hp.pos).2 h

Premises used: Iff.mpr, Nat.Prime.pos, mul_lt_mul_iff_left₀
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p

Tactic:
exact (mul_lt_mul_iff_left₀ hp.pos).2 h

Premises used: Iff.mpr, Nat.Prime.pos, mul_lt_mul_iff_left₀
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
⊢ image (fun (x : ℕ) ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))

Tactic:
have h2 : (range (p ^ n)).image (· * p) ⊆ range (p ^ (n + 1)) := fun a => by
        simp only [mem_image, mem_range, exists_imp]
        rintro b ⟨h, rfl⟩
        rw [Nat.pow_succ]
        exact (mul_lt_mul_iff_left₀ hp.pos).2 h
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
h2 : image (fun (x : ℕ) ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
rw : #(range (p ^ (n + 1))) - Finset.card (α := ℕ) (image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
rw₁ : #(range (p ^ (n + 1))) - #(range (p ^ n)) = p ^ n * (p - 1)
rw₂ : p ^ (n + 1) - #(range (p ^ n)) = p ^ n * (p - 1)
rw₃ : p ^ (n + 1) - p ^ n = p ^ n * (p - 1)
rw₄ : p ^ (n + 1) - 1 * p ^ n = 1 * p ^ n * (p - 1)
rw₅ : p * p ^ n - 1 * p ^ n = 1 * p ^ n * (p - 1)
rw₆ : (p - 1) * p ^ n = 1 * p ^ n * (p - 1)
rw₇ : (p - 1) * p ^ n = p ^ n * (p - 1)
rw₈ rw₉ : p ^ n * (p - 1) = p ^ n * (p - 1)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)

Tactic:
rw [card_sdiff_of_subset h2, Finset.card_image_of_injective _ h1, card_range, card_range, ←
        one_mul (p ^ n), pow_succ', ← tsub_mul, one_mul, mul_comm]

Premises used: Nat.pow_succ', Finset.card_sdiff_of_subset, Finset.card_range, Finset.card_image_of_injective, HPow.hPow, mul_comm, tsub_mul, one_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
rcases : ∀ (m : ℕ) (hn : 0 < m.succ), φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)

Tactic:
rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩

Premises used: Nat.exists_eq_succ_of_ne_zero, Iff.mp, pos_iff_ne_zero, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < m.succ
⊢ φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)

Tactic:
totient_prime_pow_succ hp _

Premises used: Nat.totient_prime_pow_succ, Nat.pred
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < m.succ
⊢ φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)

Tactic:
exact totient_prime_pow_succ hp _

Premises used: Nat.totient_prime_pow_succ
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
rw : p ^ HSub.hSub (α := ℕ) 1 1 * (p - 1) = HPow.hPow (β := ℕ) p 1 - 1
rw₁ : LT.lt (α := ℕ) 0 1
⊢ φ p = p - 1

Tactic:
rw [← pow_one p, totient_prime_pow hp]

Premises used: Nat.totient_prime_pow, pow_one
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
⊢ p ^ HSub.hSub (α := ℕ) 1 1 * (p - 1) = HPow.hPow (β := ℕ) p 1 - 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : Prime p
⊢ LT.lt (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p

Tactic:
⟨fun h => ?_, totient_prime⟩

Premises used: Nat.totient_prime, Iff.intro
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 0 < p
refine : ∀ (h : φ p = p - 1), Prime p
⊢ φ p = p - 1 ↔ Prime p

Tactic:
refine ⟨fun h => ?_, totient_prime⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 0 < p
h : φ p = p - 1
a : 1 ≤ p
a₁ : 1 ≠ p
⊢ 1 < p

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 0 < p
h : φ p = p - 1
a a₁ a₂ a₃ : 0 < p
⊢ 1 ≤ p

Tactic:
rwa [succ_le_iff]

Premises used: Nat.succ_le_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
hp : LT.lt (α := ℕ) 0 1
h : φ 1 = HSub.hSub (α := ℕ) 1 1
⊢ Eq (α := ℕ) 1 0

Tactic:
rw [totient_one, tsub_self] at h

Premises used: tsub_self, Nat.totient_one
-- Module: Mathlib.Data.Nat.Totient
Goal:
hp : LT.lt (α := ℕ) 0 1
h : Eq (α := ℕ) 1 0
⊢ False

Tactic:
one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
hp : LT.lt (α := ℕ) 0 1
h : Eq (α := ℕ) 1 0
⊢ False

Tactic:
exact one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 < p

Tactic:
replace hp : 1 < p := by
    apply lt_of_le_of_ne
    · rwa [succ_le_iff]
    · rintro rfl
      rw [totient_one, tsub_self] at h
      exact one_ne_zero h
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ #({a ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) p | p.Coprime a}) = #(Ico 1 p)

Tactic:
rw [totient_eq_card_coprime, range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico hp.le,
    Finset.filter_insert, if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)),
    ← Nat.card_Ico 1 p] at h

Premises used: dvd_zero, Finset.insert_Ico_add_one_left_eq_Ico, Nat.totient_eq_card_coprime, Nat.not_coprime_of_dvd_of_dvd, Nat.card_Ico, Finset.filter_insert, Finset.range_eq_Ico, OfNat.ofNat, dvd_refl, if_neg
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
h : φ p = p - 1
hp : 1 < p
h₁ : #({a ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) p | p.Coprime a}) = #(Ico 1 p)
⊢ 1 < p

Tactic:
rw [totient_eq_card_coprime, range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico hp.le,
    Finset.filter_insert, if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)),
    ← Nat.card_Ico 1 p] at h

Premises used: dvd_zero, Finset.insert_Ico_add_one_left_eq_Ico, Nat.totient_eq_card_coprime, Nat.not_coprime_of_dvd_of_dvd, Nat.card_Ico, Finset.filter_insert, Finset.range_eq_Ico, OfNat.ofNat, dvd_refl, if_neg
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
h : #({a ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) p | p.Coprime a}) = #(Ico 1 p)
hp : 1 < p
⊢ Prime p

Tactic:
p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨?_, hn⟩

Premises used: Iff.mpr, Finset.filter_card_eq, And.intro, Nat.prime_of_coprime, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
h : #({a ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) p | p.Coprime a}) = #(Ico 1 p)
hp : 1 < p
hp₁ : ∀ (n : ℕ) (hn : n < p) (hnz : n ≠ 0), HAdd.hAdd (α := ℕ) 0 1 ≤ n
⊢ Prime p

Tactic:
refine
    p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨?_, hn⟩

Premises used: Iff.mpr, Finset.filter_card_eq, And.intro, Nat.prime_of_coprime, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
h : #({a ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) p | p.Coprime a}) = #(Ico 1 p)
hp : 1 < p
n : ℕ
hn : n < p
hnz : n ≠ 0
⊢ HAdd.hAdd (α := ℕ) 0 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 1 < p
inst : Fintype (ZMod p)ˣ
⊢ NeZero p

Tactic:
haveI : NeZero p := ⟨(pos_of_gt hp).ne'⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 1 < p
inst : Fintype (ZMod p)ˣ
this : NeZero p
rw : φ p ≤ p - 1
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1

Tactic:
rw [ZMod.card_units_eq_totient p]

Premises used: ZMod.card_units_eq_totient
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 1 < p
inst : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1

Tactic:
Nat.le_sub_one_of_lt (Nat.totient_lt p hp)

Premises used: Nat.le_sub_one_of_lt, Nat.totient_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
hp : 1 < p
inst : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1

Tactic:
exact Nat.le_sub_one_of_lt (Nat.totient_lt p hp)

Premises used: Nat.le_sub_one_of_lt, Nat.totient_lt
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
inst : Fintype (ZMod p)ˣ
inl : ∀ [inst : Fintype (ZMod 0)ˣ], Prime 0 ↔ Fintype.card (ZMod 0)ˣ = HSub.hSub (α := ℕ) 0 1
inr : ∀ (hp : NeZero p), Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rcases eq_zero_or_neZero p with rfl | hp

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
inst : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = HSub.hSub (α := ℕ) 0 1

Tactic:
simp [ZMod, not_prime_zero, zero_tsub]

Premises used: ZMod, Nat.not_prime_zero, zero_tsub
-- Module: Mathlib.Data.Nat.Totient
Goal:
p : ℕ
inst : Fintype (ZMod p)ˣ
hp : NeZero p
inr : Prime p ↔ φ p = p - 1
inr₁ inr₂ : Prime p ↔ Prime p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]

Premises used: ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime, NeZero.pos
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ φ 2 = 1

Tactic:
(totient_prime prime_two).trans rfl

Premises used: Nat.totient_prime, Nat.prime_two, rfl, Eq.trans