awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Finset.Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
Ico :
  #({x ∈ Finset.Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Finset.Ico k (k + n % a + a * i) ∪ Finset.Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})
⊢ #({x ∈ Finset.Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤ φ a * i + φ a + φ a
have Ico₁ : #({x ∈ Finset.Ico k (k + n % a + a * i) ∪ Finset.Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
  #({x ∈ Finset.Ico k (k + n % a + a * i) | a.Coprime x}) + φ a
Tactic: calc
    #{x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}
      ≤ #{x ∈ Ico k (k + n % a + a * i) ∪
        Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x} := by
      gcongr
      apply Ico_subset_Ico_union_Ico
    _ ≤ #{x ∈ Ico k (k + n % a + a * i) | a.Coprime x} + a.totient := by
      rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
      apply card_union_le
    _ ≤ a.totient * i + a.totient + a.totient := by grw [← mul_add_one, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Finset.Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
Ico :
  #({x ∈ Finset.Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Finset.Ico k (k + n % a + a * i) ∪ Finset.Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})
Ico₁ :
  #({x ∈ Finset.Ico k (k + n % a + a * i) ∪ Finset.Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Finset.Ico k (k + n % a + a * i) | a.Coprime x}) + φ a
⊢ #({x ∈ Finset.Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤ φ a * i + φ a + φ a
have Ico₂ : #({x ∈ Finset.Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * i + φ a + φ a
Tactic: calc
    #{x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}
      ≤ #{x ∈ Ico k (k + n % a + a * i) ∪
        Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x} := by
      gcongr
      apply Ico_subset_Ico_union_Ico
    _ ≤ #{x ∈ Ico k (k + n % a + a * i) | a.Coprime x} + a.totient := by
      rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
      apply card_union_le
    _ ≤ a.totient * i + a.totient + a.totient := by grw [← mul_add_one, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
inst : NeZero n
inst_1 : Fintype (ZMod n)ˣ
⊢ Fintype.card { x : ZMod n // x.val.Coprime n } = φ n
have obtain : ∀ (m : ℕ) [inst : NeZero (m + 1)] [Fintype (ZMod (m + 1))ˣ],
  Fintype.card { x : ZMod (m + 1) // x.val.Coprime (m + 1) } = φ (m + 1)
Tactic: obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
Cleared hypotheses: n, inst, inst_1
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m : ℕ
inst : NeZero (m + 1)
inst_1 : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x : ZMod (m + 1) // x.val.Coprime (m + 1) } = φ (m + 1)
have simp : Eq (α := ℕ) (∑ a : ZMod (m + 1), if a.val.Coprime (m + 1) then 1 else 0)
  (∑ i : Fin (m + 1), if (↑i : ℕ).Coprime (m + 1) then 1 else 0)
Tactic: simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ←
        Fin.sum_univ_eq_sum_range, @Nat.coprime_comm (m + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : 2 < n
⊢ Even (φ n)
have this : Fact (1 < n)
Tactic: haveI : Fact (1 < n) := ⟨one_lt_two.trans hn⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)
have this₁ : NeZero n
Tactic: haveI : NeZero n := NeZero.of_gt hn
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this_2 : NeZero n
this : 2 = orderOf (G := (ZMod n)ˣ) (-1)
⊢ Even (φ n)
have rw : orderOf (G := (ZMod n)ˣ) (-1) ∣ Fintype.card (ZMod n)ˣ
Tactic: rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)
have suffices : 2 = orderOf (G := (ZMod n)ˣ) (-1)
Tactic: suffices 2 = orderOf (-1 : (ZMod n)ˣ) by
    rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
    exact orderOf_dvd_card
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (G := (ZMod n)ˣ) (-1)
have rw : 2 = orderOf (G := ZMod n) (↑(-1) : ZMod n)
Tactic: rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this : NeZero n
rw : 2 = orderOf (G := ZMod n) (↑(-1) : ZMod n)
⊢ 2 = orderOf (G := (ZMod n)ˣ) (-1)
have rw₁ : 2 = orderOf (G := ZMod n) (-1)
Tactic: rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this : NeZero n
rw : 2 = orderOf (G := ZMod n) (↑(-1) : ZMod n)
rw₁ : 2 = orderOf (G := ZMod n) (-1)
⊢ 2 = orderOf (G := (ZMod n)ˣ) (-1)
have rw₂ : Eq (α := ℕ) 2 (if ringChar (ZMod n) = 2 then 1 else 2)
Tactic: rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this : NeZero n
rw : 2 = orderOf (G := ZMod n) (↑(-1) : ZMod n)
rw₁ : 2 = orderOf (G := ZMod n) (-1)
rw₂ : Eq (α := ℕ) 2 (if ringChar (ZMod n) = 2 then 1 else 2)
⊢ 2 = orderOf (G := (ZMod n)ˣ) (-1)
have rw₃ : Eq (α := ℕ) 2 (if n = 2 then 1 else 2)
Tactic: rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this : NeZero n
rw : 2 = orderOf (G := ZMod n) (↑(-1) : ZMod n)
rw₁ : 2 = orderOf (G := ZMod n) (-1)
rw₂ : Eq (α := ℕ) 2 (if ringChar (ZMod n) = 2 then 1 else 2)
rw₃ : Eq (α := ℕ) 2 (if n = 2 then 1 else 2)
⊢ 2 = orderOf (G := (ZMod n)ˣ) (-1)
have rw₄ : Eq (α := ℕ) 2 2
Tactic: rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n
have inl : ∀ (h : m = 0), φ (m * n) = φ m * φ n
Tactic: rcases Nat.mul_eq_zero.1 hmn0 with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : m * n = 0
inl : ∀ (h : m = 0), φ (m * n) = φ m * φ n
⊢ φ (m * n) = φ m * φ n
have inr : ∀ (h : n = 0), φ (m * n) = φ m * φ n
Tactic: rcases Nat.mul_eq_zero.1 hmn0 with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
⊢ φ (m * n) = φ m * φ n
have this : NeZero (m * n)
Tactic: haveI : NeZero (m * n) := ⟨hmn0⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n
have this₁ : NeZero m
Tactic: haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n
have this₁ : NeZero n
Tactic: haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n
have simp : Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
Tactic: simp only [← ZMod.card_units_eq_totient]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this_2 : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
have rw : Fintype.card (ZMod m × ZMod 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)ˣ
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
have rw₁ : Fintype.card ((ZMod m)ˣ × (ZMod 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)ˣ
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
have rw₂ : Fintype.card (ZMod m)ˣ * Fintype.card (ZMod 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})
have inl : ∀ (hnd : 0 ∣ n), φ (n / 0) = #({k ∈ range n | n.gcd k = 0})
Tactic: rcases d.eq_zero_or_pos with (rfl | hd0)
Cleared hypotheses: d, hnd
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n d : ℕ
hnd : d ∣ n
inl : ∀ (hnd : 0 ∣ n), φ (n / 0) = #({k ∈ range n | n.gcd k = 0})
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})
have inr : ∀ (hd0 : d > 0), φ (n / d) = #({k ∈ range n | n.gcd k = d})
Tactic: rcases d.eq_zero_or_pos with (rfl | hd0)
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})
have inr : ∀ (x : ℕ), φ (d * x / d) = #({k ∈ range (d * x) | (d * x).gcd k = d})
Tactic: rcases hnd with ⟨x, rfl⟩
Cleared hypotheses: n, hnd
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = #({k ∈ range (d * x) | (d * x).gcd k = d})
have inr : φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
Tactic: rw [Nat.mul_div_cancel_left x hd0]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
have inr : ∀ (a : ℕ) (ha : a ∈ {a ∈ range x | x.Coprime a}), d * a ∈ {k ∈ range (d * x) | (d * x).gcd k = d}
Tactic: apply Finset.card_bij fun k _ => d * k
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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}
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
have 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₂
Tactic: apply Finset.card_bij fun k _ => d * k
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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₂
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
have inr₂ : ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ (a : ℕ) (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b
Tactic: apply Finset.card_bij fun k _ => d * k
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ (a : ℕ) (ha : a ∈ {a ∈ range x | x.Coprime a}), d * a ∈ {k ∈ range (d * x) | (d * x).gcd k = d}
have inr : ∀ a < x, x.gcd a = 1 → d * a < d * x ∧ (d * x).gcd (d * a) = d
Tactic: simp only [mem_filter, mem_range, and_imp, Coprime]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ d * a < d * x
have ha : 0 < d
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a < x, x.gcd a = 1 → d * a < d * x ∧ (d * x).gcd (d * a) = d
have inr : ∀ (a : ℕ) (ha1 : a < x) (ha2 : x.gcd a = 1), (d * x).gcd (d * a) = d
Tactic: refine fun a ha1 ha2 => ⟨by gcongr, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ (d * x).gcd (d * a) = d
have inr : d * x.gcd a = d
Tactic: rw [gcd_mul_left, ha2, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
inr : d * x.gcd a = d
⊢ (d * x).gcd (d * a) = d
have inr₁ : d * 1 = d
Tactic: rw [gcd_mul_left, ha2, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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
⊢ (d * x).gcd (d * a) = d
have inr₂ : d = d
Tactic: rw [gcd_mul_left, ha2, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ (a : ℕ) (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b
have inr : ∀ b < d * x, (d * x).gcd b = d → ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b
Tactic: simp only [mem_filter, mem_range, exists_prop, and_imp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ d ∣ b
have rw : (d * x).gcd b ∣ b
Tactic: rw [← hb2]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b
have this : d ∣ b
Tactic: have : d ∣ b := by
      rw [← hb2]
      apply gcd_dvd_right
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
this : d ∣ b
⊢ ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = b
have inr : ∀ (q : ℕ) (hb1 : d * q < d * x) (hb2 : (d * x).gcd (d * q) = d), ∃ (a : ℕ), (a < x ∧ x.Coprime a) ∧ d * a = d * q
Tactic: rcases this with ⟨q, rfl⟩
Cleared hypotheses: b, hb1, hb2, this
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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
have inr : x.Coprime q
Tactic: refine ⟨q, ⟨⟨(mul_lt_mul_iff_right₀ hd0).1 hb1, ?_⟩, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ x.Coprime q
have inr : ∀ (hb2 : d * x.gcd q = d), x.Coprime q
Tactic: rwa [gcd_mul_left, mul_eq_left hd0.ne'] at hb2
Cleared hypotheses: hb2
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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
⊢ x.Coprime q
have inr₁ : ∀ (hb2 : x.gcd q = 1), x.Coprime q
Tactic: rwa [gcd_mul_left, mul_eq_left hd0.ne'] at hb2
Cleared hypotheses: hb2
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ n.divisors.sum φ = n
have inl : (divisors 0).sum φ = 0
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
inl : (divisors 0).sum φ = 0
⊢ n.divisors.sum φ = n
have inr : ∀ (hn : n > 0), n.divisors.sum φ = n
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : n > 0
⊢ n.divisors.sum φ = n
have inr : ∑ d ∈ n.divisors, φ (n / d) = n
Tactic: rw [← sum_div_divisors n φ]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : n > 0
⊢ n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
have nth_rw : #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
Tactic: nth_rw 1 [← card_range n]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
have refine : ∀ x ∈ (↑(range n) : Set ℕ), n.gcd x ∣ n
Tactic: refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : n > 0
⊢ ∑ d ∈ n.divisors, φ (n / d) = n
have this : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
⊢ ∑ d ∈ n.divisors, φ (n / d) = n
have inr : Eq (α := ℕ) (∑ d ∈ n.divisors, φ (n / d)) (∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d}))
Tactic: nth_rw 3 [this]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n
have h : ∑ m ∈ range n.succ with m ∣ n, φ m = n.divisors.sum φ
Tactic: convert! sum_totient _ using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n.divisors.sum φ
have 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)
Tactic: simp only [Nat.divisors, sum_filter, range_eq_Ico]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ 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)
have 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
Tactic: rw [sum_eq_sum_Ico_succ_bot]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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
⊢ 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)
have h₁ : 0 < n.succ
Tactic: rw [sum_eq_sum_Ico_succ_bot]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} =
    range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))
have 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))}
Tactic: rw [sdiff_eq_filter]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime 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))}
have H : ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))
Tactic: apply filter_congr
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))
have H : ∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)
Tactic: simp only [mem_range, coprime_pow_left_iff n.succ_pos, mem_image, not_exists,
            hp.coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
have H : ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
H : ¬p ∣ a → ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
have H₁ : (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
have left : b < p ^ n
Tactic: rcases h with ⟨_, rfl⟩
Cleared hypotheses: a, ha, hap, h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
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
⊢ False
have ha₁ : b * p < p ^ (n + 1)
Tactic: rcases h with ⟨_, rfl⟩
Cleared hypotheses: a, ha, hap, h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
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)
⊢ False
have hap₁ : ¬p ∣ b * p
Tactic: rcases h with ⟨_, rfl⟩
Cleared hypotheses: a, ha, hap, h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p ^ (n + 1)
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
have ha₁ : p * b < p * p ^ n
Tactic: rw [pow_succ'] at ha
Cleared hypotheses: ha, h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
Tactic: have h1 : Function.Injective (· * p) := mul_left_injective₀ hp.ne_zero
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
a : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) a → a ∈ range (p ^ (n + 1))
have simp : ∀ (x : ℕ), x < p ^ n ∧ x * p = a → a < p ^ (n + 1)
Tactic: simp only [mem_image, mem_range, exists_imp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ (n + 1)
have rw : b * p < p ^ n * p
Tactic: rw [Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * p
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have h2 : 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
-- 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))
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw : #(range (p ^ (n + 1))) - Finset.card (α := ℕ) (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]
-- 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)
⊢ #(range (p ^ (n + 1)) \ image (fun (x : ℕ) ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)
have rw₁ : #(range (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]