awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₂ : p ^ (n + 1) - #(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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₃ : p ^ (n + 1) - 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₄ : p ^ (n + 1) - 1 * p ^ n = 1 * 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₅ : p * p ^ n - 1 * p ^ n = 1 * 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₆ : (p - 1) * p ^ n = 1 * 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₇ : (p - 1) * 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₈ : p ^ n * (p - 1) = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)
have rcases : ∀ (m : ℕ) (hn : 0 < m.succ), φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)
Tactic: rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
⊢ φ p = p - 1
have rw : p ^ HSub.hSub (α := ℕ) 1 1 * (p - 1) = HPow.hPow (β := ℕ) p 1 - 1
Tactic: rw [← pow_one p, totient_prime_pow hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
rw : p ^ HSub.hSub (α := ℕ) 1 1 * (p - 1) = HPow.hPow (β := ℕ) p 1 - 1
⊢ φ p = p - 1
have rw₁ : LT.lt (α := ℕ) 0 1
Tactic: rw [← pow_one p, totient_prime_pow hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p
have refine : ∀ (h : φ p = p - 1), Prime p
Tactic: refine ⟨fun h => ?_, totient_prime⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 1 < p
have a : 1 ≤ p
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : 0 < p
h : φ p = p - 1
a : 1 ≤ p
⊢ 1 < p
have a₁ : 1 ≠ p
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
hp : LT.lt (α := ℕ) 0 1
h : φ 1 = HSub.hSub (α := ℕ) 1 1
⊢ False
have h₁ : Eq (α := ℕ) 1 0
Tactic: rw [totient_one, tsub_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ Prime p
have hp₁ : 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
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p : ℕ
h : φ p = p - 1
hp : 1 < p
⊢ Prime p
have h₁ : #({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
Cleared hypotheses: h, hp
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
h : #({a ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) p | p.Coprime a}) = #(Ico 1 p)
hp : 1 < p
⊢ Prime p
have hp₁ : ∀ (n : ℕ) (hn : n < p) (hnz : n ≠ 0), HAdd.hAdd (α := ℕ) 0 1 ≤ n
Tactic: refine
    p.prime_of_coprime hp fun n hn hnz => Finset.filter_card_eq h n <| Finset.mem_Ico.mpr ⟨?_, hn⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p : ℕ
hp : 1 < p
inst : Fintype (ZMod p)ˣ
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1
have this : NeZero p
Tactic: haveI : NeZero p := ⟨(pos_of_gt hp).ne'⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : 1 < p
inst : Fintype (ZMod p)ˣ
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1
have rw : φ p ≤ p - 1
Tactic: rw [ZMod.card_units_eq_totient p]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
inst : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
have inl : ∀ [inst : Fintype (ZMod 0)ˣ], Prime 0 ↔ Fintype.card (ZMod 0)ˣ = HSub.hSub (α := ℕ) 0 1
Tactic: rcases eq_zero_or_neZero p with rfl | hp
Cleared hypotheses: p, inst
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
inst : Fintype (ZMod p)ˣ
inl : ∀ [inst : Fintype (ZMod 0)ˣ], Prime 0 ↔ Fintype.card (ZMod 0)ˣ = HSub.hSub (α := ℕ) 0 1
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
have inr : ∀ (hp : NeZero p), Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
Tactic: rcases eq_zero_or_neZero p with rfl | hp
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
inst : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
have inr : Prime p ↔ φ p = p - 1
Tactic: rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
inst : Fintype (ZMod p)ˣ
hp : NeZero p
inr : Prime p ↔ φ p = p - 1
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
have inr₁ : Prime p ↔ Prime p
Tactic: rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ Odd (φ n) ↔ n = 1 ∨ n = 2
have zero : Odd (φ 0) ↔ Eq (α := ℕ) 0 1 ∨ Eq (α := ℕ) 0 2
Tactic: rcases n with _ | _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
zero : Odd (φ 0) ↔ Eq (α := ℕ) 0 1 ∨ Eq (α := ℕ) 0 2
⊢ Odd (φ n) ↔ n = 1 ∨ n = 2
have succ : Odd (φ (HAdd.hAdd (α := ℕ) 0 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 = 2
Tactic: rcases n with _ | _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
zero : Odd (φ 0) ↔ Eq (α := ℕ) 0 1 ∨ Eq (α := ℕ) 0 2
succ : Odd (φ (HAdd.hAdd (α := ℕ) 0 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 = 2
⊢ Odd (φ n) ↔ n = 1 ∨ n = 2
have succ₁ : Odd (φ (HAdd.hAdd (α := ℕ) 0 1 + 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 + 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 + 1 = 2
Tactic: rcases n with _ | _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
zero : Odd (φ 0) ↔ Eq (α := ℕ) 0 1 ∨ Eq (α := ℕ) 0 2
succ : Odd (φ (HAdd.hAdd (α := ℕ) 0 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 = 2
succ₁ : Odd (φ (HAdd.hAdd (α := ℕ) 0 1 + 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 + 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 + 1 = 2
⊢ Odd (φ n) ↔ n = 1 ∨ n = 2
have succ₂ : ∀ (n : ℕ), Odd (φ (n + 1 + 1 + 1)) ↔ n + 1 + 1 + 1 = 1 ∨ n + 1 + 1 + 1 = 2
Tactic: rcases n with _ | _ | _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
have this : 3 ≤ n + 3
Tactic: have : 3 ≤ n + 3 := le_add_self
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
have simp : φ (n + 3) = 1 ↔ n + 3 = 2
Tactic: simp only [succ_succ_ne_one, false_or]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
han : 0 < a
ha : φ a ≤ 1
⊢ a ∣ 2
have inl : ∀ (han : LT.lt (α := ℕ) 0 1) (ha : φ 1 ≤ 1), Dvd.dvd (α := ℕ) 1 2
Tactic: rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl
Cleared hypotheses: a, han, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
han : 0 < a
ha : φ a ≤ 1
inl : ∀ (han : LT.lt (α := ℕ) 0 1) (ha : φ 1 ≤ 1), Dvd.dvd (α := ℕ) 1 2
⊢ a ∣ 2
have inr : ∀ (han : LT.lt (α := ℕ) 0 2) (ha : φ 2 ≤ 1), Dvd.dvd (α := ℕ) 2 2
Tactic: rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl
Cleared hypotheses: a, han, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
⊢ (φ m).Coprime (φ n) ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
have mp : (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
mp : (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
⊢ (φ m).Coprime (φ n) ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
have mpr : (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2 → (φ m).Coprime (φ n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
⊢ (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
have mp : ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)
Tactic: rw [← not_imp_not]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
⊢ ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)
have mp : 2 ∣ φ m ∧ 2 ∣ φ n → ¬(φ m).Coprime (φ n)
Tactic: simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
⊢ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2 → (φ m).Coprime (φ n)
have mpr : φ m = 1 ∨ φ n = 1 → (φ m).Coprime (φ n)
Tactic: simp_rw [← totient_eq_one_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
h : φ m = 1
⊢ (φ m).Coprime (φ n)
have mpr : Coprime 1 (φ n)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime (φ n)
have mpr : (φ m).Coprime 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ φ n = n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)
have rw : Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ φ (p ^ k))
  (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
Tactic: rw [multiplicative_factorization φ (@totient_mul) totient_one hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ φ (p ^ k))
    (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
have apply : ∀ x ∈ n.factorization.support,
  φ (HPow.hPow (β := ℕ) x ((n.factorization : (a : ℕ) → ℕ) x : ℕ)) =
    x ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ) * (x - 1)
Tactic: apply Finsupp.prod_congr _
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ φ (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)
have h : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ φ (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)
have rw : p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) =
  p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)
Tactic: rw [totient_prime_pow (prime_of_mem_primeFactors hp) h]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
have pos : ∀ (hn : n = 0), φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
pos : ∀ (hn : n = 0), φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
have neg : ∀ (hn : ¬n = 0), φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
have neg : HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
  n * ∏ p ∈ n.primeFactors, (p - 1)
Tactic: rw [totient_eq_prod_factorization hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
⊢ HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
    n * ∏ p ∈ n.primeFactors, (p - 1)
have neg : HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
  HMul.hMul (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ n.primeFactors, (p - 1))
Tactic: nth_rw 3 [← prod_factorization_pow_eq_self hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
⊢ HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
    HMul.hMul (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ n.primeFactors, (p - 1))
have neg : Eq (α := ℕ) (n.factorization.prod fun (a b : ℕ) ↦ a ^ (b - 1) * (a - 1) * a)
  (n.factorization.prod fun (a b : ℕ) ↦ a ^ b * (a - 1))
Tactic: simp only [prod_primeFactors_prod_factorization, ← Finsupp.prod_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
⊢ Eq (α := ℕ) (n.factorization.prod fun (a b : ℕ) ↦ a ^ (b - 1) * (a - 1) * a)
    (n.factorization.prod fun (a b : ℕ) ↦ a ^ b * (a - 1))
have neg : ∀ (p : ℕ) (hp : p ∈ n.factorization.support),
  p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
Tactic: refine Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
have hp₁ : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
have neg : p * (p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)) =
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
Tactic: rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  p * (p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
have neg₁ : p * p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) =
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
Tactic: rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  p * (p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₁ :
  p * p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
have neg₂ : p ^ (HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)).succ * (p - 1) =
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
Tactic: rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  p * (p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₁ :
  p * p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₂ :
  p ^ (HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)).succ * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
have neg₃ : p ^ (pred ((n.factorization : (a : ℕ) → ℕ) p)).succ * (p - 1) =
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
Tactic: rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  p * (p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₁ :
  p * p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₂ :
  p ^ (HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)).succ * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₃ :
  p ^ (pred ((n.factorization : (a : ℕ) → ℕ) p)).succ * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
have neg₄ : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1) =
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
Tactic: rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)
have rw : LT.lt (α := ℕ) 0 (∏ p ∈ n.primeFactors, p)
Tactic: rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm,
    Nat.mul_div_assoc _ (prod_primeFactors_dvd n), mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
have pos : ∀ (hn : n = 0), (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
Tactic: by_cases hn : n = 0