awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ ¬p ∣ m.gcd n

Tactic:
exact fun hpn ↦ hp.2 hp.1.1 <| hpn.trans <| gcd_dvd_right _ _

Premises used: And.right, And.left
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
⊢ Set.InvOn (fun (n : ℕ) ↦ n.factorization.support) (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) {s : Finset ℕ | ∀ p ∈ s, Prime p}
    {n : ℕ | Squarefree n}

Tactic:
⟨fun _s ↦ primeFactors_prod, fun _n ↦ prod_primeFactors_of_squarefree⟩

Premises used: Set.InvOn, Nat.prod_primeFactors_of_squarefree, And.intro, Nat.primeFactors_prod
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a

Tactic:
symm <| Nat.div_eq_of_eq_mul_left (Finset.prod_pos
    fun p hp => (prime_of_mem_primeFactorsList (List.mem_toFinset.mp (ht hp))).pos) ?_

Premises used: List.mem_toFinset, Nat.prime_of_mem_primeFactorsList, Nat.Prime.pos, Nat.div_eq_of_eq_mul_left, Finset.prod_pos, Iff.mp, symm
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
refine : n = HMul.hMul (α := ℕ) (∏ a ∈ n.primeFactors \ t, a) (∏ a ∈ t, a)
⊢ ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a

Tactic:
refine symm <| Nat.div_eq_of_eq_mul_left (Finset.prod_pos
    fun p hp => (prime_of_mem_primeFactorsList (List.mem_toFinset.mp (ht hp))).pos) ?_

Premises used: List.mem_toFinset, Nat.prime_of_mem_primeFactorsList, Nat.Prime.pos, Nat.div_eq_of_eq_mul_left, Finset.prod_pos, Iff.mp, symm
-- Module: Mathlib.Data.Nat.Squarefree
Goal:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
rw : n = ∏ x ∈ n.primeFactors, x
rw₁ rw₂ : n = n
⊢ n = HMul.hMul (α := ℕ) (∏ a ∈ n.primeFactors \ t, a) (∏ a ∈ t, a)

Tactic:
rw [Finset.prod_sdiff ht, prod_primeFactors_of_squarefree hn]

Premises used: Nat.prod_primeFactors_of_squarefree, Finset.prod_sdiff
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a : ℕ
ha : a ≤ a.pred
zero : ∀ (ha : 0 ≤ pred 0), IsMin (α := ℕ) 0
succ : ∀ (n : ℕ) (ha : n + 1 ≤ (n + 1).pred), IsMin (n + 1)
⊢ IsMin a

Tactic:
cases a
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n : ℕ
ha : 0 ≤ pred 0
⊢ IsMin (α := ℕ) 0

Tactic:
isMin_bot

Premises used: isMin_bot
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n : ℕ
ha : 0 ≤ pred 0
⊢ IsMin (α := ℕ) 0

Tactic:
exact isMin_bot

Premises used: isMin_bot
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n n_1 : ℕ
ha : n_1 + 1 ≤ (n_1 + 1).pred
⊢ IsMin (n_1 + 1)

Tactic:
(not_succ_le_self _ ha).elim

Premises used: False.elim, Nat.not_succ_le_self
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n n_1 : ℕ
ha : n_1 + 1 ≤ (n_1 + 1).pred
⊢ IsMin (n_1 + 1)

Tactic:
exact (not_succ_le_self _ ha).elim

Premises used: False.elim, Nat.not_succ_le_self
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a b : ℕ
h : a < b
zero : ∀ (h : a < 0), a ≤ pred 0
succ : ∀ (n : ℕ) (h : a < n + 1), a ≤ (n + 1).pred
⊢ a ≤ b.pred

Tactic:
cases b
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a : ℕ
h : a < 0
⊢ a ≤ pred 0

Tactic:
(a.not_lt_zero h).elim

Premises used: False.elim, Nat.not_lt_zero
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a : ℕ
h : a < 0
⊢ a ≤ pred 0

Tactic:
exact (a.not_lt_zero h).elim

Premises used: False.elim, Nat.not_lt_zero
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a n_1 : ℕ
h : a < n_1 + 1
⊢ a ≤ (n_1 + 1).pred

Tactic:
le_of_succ_le_succ h

Premises used: Nat.le_of_succ_le_succ
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a n_1 : ℕ
h : a < n_1 + 1
⊢ a ≤ (n_1 + 1).pred

Tactic:
exact le_of_succ_le_succ h

Premises used: Nat.le_of_succ_le_succ
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
⊢ Order.succ = succ

Tactic:
rfl

Premises used: Order.succ, rfl
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
⊢ Order.pred = pred

Tactic:
rfl

Premises used: Order.pred, Nat.pred, rfl
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
a : ℕ
⊢ ∀ (n : ℕ), succ^[n] a = a + n

Tactic:
Order.succ_iterate a

Premises used: Order.succ, Order.succ_iterate
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
a n : ℕ
rw : (pred ∘ pred^[n]) a = (a - n).pred
⊢ pred^[n + 1] a = a - (n + 1)

Tactic:
rw [Function.iterate_succ', sub_succ]

Premises used: Function.iterate_succ', Nat.sub_succ
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
a n : ℕ
⊢ (pred ∘ pred^[n]) a = (a - n).pred

Tactic:
congr_arg _ (Nat.pred_iterate a n)

Premises used: congr_arg, Nat.pred
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
a n : ℕ
⊢ (pred ∘ pred^[n]) a = (a - n).pred

Tactic:
exact congr_arg _ (Nat.pred_iterate a n)

Premises used: congr_arg
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n : ℕ
⊢ m ⋖ n ↔ m + 1 = n

Tactic:
Order.covBy_iff_add_one_eq

Premises used: Order.covBy_iff_add_one_eq
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n : ℕ
⊢ m ≤ n.succ ↔ m = n.succ ∨ m ≤ n

Tactic:
Order.le_succ_iff_eq_or_le

Premises used: Order.succ, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a b : ℕ
h : a ≤ b
rw : succ^[b - a] a = b
rw₁ : a + (b - a) = b
rw₂ rw₃ : b = b
⊢ Order.succ^[b - a] a = b

Tactic:
rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]

Premises used: Nat.succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
m n a b : ℕ
h : a ≤ b
rw : pred^[b - a] b = a
rw₁ : b - (b - a) = a
rw₂ rw₃ : a = a
⊢ Order.pred^[b - a] b = a

Tactic:
rw [pred_eq_pred, Nat.pred_iterate, tsub_tsub_cancel_of_le h]

Premises used: Nat.pred_iterate, Nat.pred_eq_pred, tsub_tsub_cancel_of_le
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
P : ℕ → Prop
⊢ (∀ (i : ℕ), i ≠ 0 → P i) ↔ ∀ (i : ℕ), P (i + 1)

Tactic:
SuccOrder.forall_ne_bot_iff P

Premises used: SuccOrder.forall_ne_bot_iff
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
n : ℕ
a b : Fin n
⊢ a ⋖ b ↔ (↑a : ℕ) ⋖ (↑b : ℕ)

Tactic:
and_congr_right' ⟨fun h c ha hb ↦ @h ⟨c, hb.trans b.prop⟩ ha hb, fun h _c hc ↦ h hc⟩

Premises used: and_congr_right', CovBy, Iff.intro
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
n : ℕ
a b : Fin n
⊢ (↑a : ℕ) ⋖ (↑b : ℕ) ↔ a ⋖ b

Tactic:
Fin.covBy_iff.symm

Premises used: Fin.covBy_iff, Iff.symm
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
⊢ Eq (α := ℕ) (WithBot.succ 0) 1

Tactic:
rfl

Premises used: Order.succ, WithBot.succ, WithBot.recBotCoe, rfl
-- Module: Mathlib.Data.Nat.SuccPred
Goal:
⊢ Eq (α := ℕ) (WithBot.succ 1) 2

Tactic:
rfl

Premises used: Order.succ, WithBot.succ, WithBot.recBotCoe, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ φ 0 = 0

Tactic:
rfl

Premises used: Nat.totient, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ φ 1 = 1

Tactic:
rfl

Premises used: Nat.totient, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ φ n = #({a ∈ range n | n.Coprime a})

Tactic:
rfl

Premises used: Nat.totient, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
m : (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
⊢ (↑m : ℕ) ∈ {x ∈ range n | n.Coprime x}

Tactic:
simpa only [Finset.mem_filter, Finset.mem_range] using m.property

Premises used: Finset.mem_range, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
m : ↥({x ∈ range n | n.Coprime x})
⊢ Membership.mem (γ := Set ℕ) {m : ℕ | m < n ∧ n.Coprime m} (↑m : ℕ)

Tactic:
simpa only [Finset.mem_filter, Finset.mem_range] using m.property

Premises used: Finset.mem_range, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
m : (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
⊢ (fun (m : ↥({x ∈ range n | n.Coprime x})) ↦
        (Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | m < n ∧ n.Coprime m} x) (↑m : ℕ) ⋯ :
          { x : ℕ // Membership.mem (γ := Set ℕ) {m : ℕ | m < n ∧ n.Coprime m} x }))
      ((fun (m : (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)) ↦
          (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ {x ∈ range n | n.Coprime x}) (↑m : ℕ) ⋯ : ↥({x ∈ range n | n.Coprime x})))
        m) =
    m

Tactic:
simp only [Subtype.coe_eta]

Premises used: Subtype.coe_eta
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
m : ↥({x ∈ range n | n.Coprime x})
⊢ (fun (m : (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)) ↦
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ {x ∈ range n | n.Coprime x}) (↑m : ℕ) ⋯ : ↥({x ∈ range n | n.Coprime x})))
      ((fun (m : ↥({x ∈ range n | n.Coprime x})) ↦
          (Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | m < n ∧ n.Coprime m} x) (↑m : ℕ) ⋯ :
            { x : ℕ // Membership.mem (γ := Set ℕ) {m : ℕ | m < n ∧ n.Coprime m} x }))
        m) =
    m

Tactic:
simp only [Subtype.coe_eta]

Premises used: Subtype.coe_eta
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
e : (↑{m : ℕ | m < n ∧ n.Coprime m} : Type) ≃ ↥({x ∈ range n | n.Coprime x}) :=
  {
    toFun := fun (m : (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)) ↦
      Subtype.mk (p := fun (x : ℕ) ↦ x ∈ {x ∈ range n | n.Coprime x}) (↑m : ℕ) ⋯,
    invFun := fun (m : ↥({x ∈ range n | n.Coprime x})) ↦
      Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | m < n ∧ n.Coprime m} x) (↑m : ℕ) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
rw : #({a ∈ range n | n.Coprime a}) = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
rw₁ : #({a ∈ range n | n.Coprime a}) = Nat.card ↥({x ∈ range n | n.Coprime x})
rw₂ : #({a ∈ range n | n.Coprime a}) = Fintype.card ↥({x ∈ range n | n.Coprime x})
rw₃ rw₄ : #({a ∈ range n | n.Coprime a}) = #({x ∈ range n | n.Coprime x})
⊢ φ n = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)

Tactic:
rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]

Premises used: Nat.totient_eq_card_coprime, Nat.card_congr, Fintype.card_coe, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ φ n ≤ n

Tactic:
((range n).card_filter_le _).trans_eq (card_range n)

Premises used: LE.le.trans_eq, Finset.card_range, Nat.totient, Finset.range, Finset.card_filter_le
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 1 < n
⊢ 0 ∈ range n ∧ ¬n.Coprime 0

Tactic:
simp [hn.ne', pos_of_gt hn]

Premises used: pos_of_gt, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ φ 0 = 0 ↔ Eq (α := ℕ) 0 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
rw : (1 % (n + 1)).gcd (n + 1) = 1
rw₁ : (n + 1).gcd 1 = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ (n + 1).gcd (1 % (n + 1)) = 1

Tactic:
rw [gcd_comm, ← gcd_rec, gcd_one_right]

Premises used: Nat.gcd_one_right, Nat.gcd_rec, Nat.gcd_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
this : ∃ x < n + 1, (n + 1).gcd x = 1
⊢ φ (n + 1) = 0 ↔ n + 1 = 0

Tactic:
simpa [totient, filter_eq_empty_iff]

Premises used: Nat.totient, Finset.filter_eq_empty_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ 0 < φ n ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
inst : NeZero n
⊢ NeZero (φ n)

Tactic:
⟨(totient_pos.mpr <| NeZero.pos n).ne'⟩

Premises used: Iff.mpr, NeZero.mk, LT.lt.ne', NeZero.pos, Nat.totient_pos
-- Module: Mathlib.Data.Nat.Totient
Goal:
a n : ℕ
pp : Function.Periodic (β := Prop) (fun (x : ℕ) ↦ a.Coprime x) a
⊢ #({x ∈ Ico n (n + a) | a.Coprime x}) = φ a

Tactic:
rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]

Premises used: Nat.count_eq_card_filter_range, Nat.totient, Nat.filter_Ico_card_eq_of_periodic
-- Module: Mathlib.Data.Nat.Totient
Goal:
a n : ℕ
⊢ Function.Periodic (β := Prop) (fun (x : ℕ) ↦ a.Coprime x) a

Tactic:
periodic_coprime a

Premises used: Nat.periodic_coprime
-- Module: Mathlib.Data.Nat.Totient
Goal:
a n : ℕ
⊢ Function.Periodic (β := Prop) (fun (x : ℕ) ↦ a.Coprime x) a

Tactic:
exact periodic_coprime a

Premises used: Nat.periodic_coprime
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
rw : #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x})
| #({x ∈ Ico k (k + n) | a.Coprime x})

Tactic:
rw [← Nat.mod_add_div n a]

Premises used: Nat.mod_add_div
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
conv_lhs : #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x}) ≤ φ a * (n / a + 1)
⊢ #({x ∈ Ico k (k + n) | a.Coprime x}) ≤ φ a * (n / a + 1)

Tactic:
conv_lhs => rw [← Nat.mod_add_div n a]

Premises used: Nat.mod_add_div
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
zero :
  #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x}) * HAdd.hAdd (α := ℕ) 0 1
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ φ a * HAdd.hAdd (α := ℕ) 0 1

Tactic:
rw [← filter_coprime_Ico_eq_totient a k]

Premises used: Nat.filter_coprime_Ico_eq_totient
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
zero : #({x ∈ Ico k (k + n % a) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x})
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x}) * HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp only [add_zero, mul_one, mul_zero, zero_add]

Premises used: zero_add, MulZeroClass.mul_zero, mul_one, add_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
zero : n % a ≤ a
⊢ #({x ∈ Ico k (k + n % a) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x})

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ n % a ≤ a

Tactic:
le_of_lt (mod_lt n (pos_iff_ne_zero.mpr a_ne_zero))

Premises used: Iff.mpr, le_of_lt, Nat.mod_lt, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ n % a ≤ a

Tactic:
exact le_of_lt (mod_lt n (pos_iff_ne_zero.mpr a_ne_zero))

Premises used: Iff.mpr, le_of_lt, Nat.mod_lt, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + (n % a + a * i)) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + (n % a + a * (i + 1))) | a.Coprime x}) ≤ φ a * (i + 1 + 1)

Tactic:
?_
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
succ :
  ∀ (i : ℕ) (ih : #({x ∈ Ico k (k + (n % a + a * i)) | a.Coprime x}) ≤ φ a * (i + 1)),
    #({x ∈ Ico k (k + (n % a + a * (i + 1))) | a.Coprime x}) ≤ φ a * (i + 1 + 1)
⊢ #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x}) ≤ φ a * (n / a + 1)

Tactic:
induction n / a with
  | zero =>
    rw [← filter_coprime_Ico_eq_totient a k]
    simp only [add_zero, mul_one, mul_zero, zero_add]
    gcongr
    exact le_of_lt (mod_lt n (pos_iff_ne_zero.mpr a_ne_zero))
  | succ i ih => ?_

Premises used: Iff.mpr, le_of_lt, zero_add, Nat.mod_lt, MulZeroClass.mul_zero, Nat.filter_coprime_Ico_eq_totient, Nat.zero, mul_one, add_zero, Nat.succ, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + (n % a + a * i)) | a.Coprime x}) ≤ φ a * (i + 1)
succ :
  ∀ (ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)),
    #({x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤ φ a * i + φ a + φ a
⊢ #({x ∈ Ico k (k + (n % a + (a * i + a))) | a.Coprime x}) ≤ φ a * i + φ a + φ a

Tactic:
simp_rw [← add_assoc] at ih ⊢

Premises used: add_assoc
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
a₁ : Ico k (k + n % a + a * i + a) ⊆ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)
⊢ #({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})

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ Ico k (k + n % a + a * i + a) ⊆ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)

Tactic:
apply Ico_subset_Ico_union_Ico

Premises used: Finset.Ico_subset_Ico_union_Ico
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
rw :
  #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x} ∪
        {x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) +
      #({x ∈ Ico (k + n % a + a * i) (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}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a

Tactic:
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]

Premises used: HMul.hMul, HMod.hMod, HAdd.hAdd, Nat.filter_coprime_Ico_eq_totient, Finset.filter_union
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x} ∪
        {x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) +
      #({x ∈ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})

Tactic:
apply card_union_le

Premises used: Finset.card_union_le
-- Module: Mathlib.Data.Nat.Totient
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
grw : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * (i + 1) + φ a
grw₁ grw₂ : φ a * (i + 1) + φ a ≤ φ a * (i + 1) + φ a
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * i + φ a + φ a

Tactic:
grw [← mul_add_one, ih]

Premises used: Nat.mul_add_one
-- Module: Mathlib.Data.Nat.Totient
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
Ico₂ : #({x ∈ Finset.Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * i + φ a + φ a
⊢ #({x ∈ Finset.Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤ φ 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]

Premises used: HMul.hMul, Finset.Ico, Nat.totient, HMod.hMod, HAdd.hAdd
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
inst : NeZero n
inst_1 : Fintype (ZMod n)ˣ
⊢ ∃ (m : ℕ), n = m + 1

Tactic:
exists_eq_succ_of_ne_zero NeZero.out

Premises used: Nat.exists_eq_succ_of_ne_zero, NeZero.out
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
inst : NeZero n
inst_1 : Fintype (ZMod n)ˣ
obtain :
  ∀ (m : ℕ) [inst : NeZero (m + 1)] [Fintype (ZMod (m + 1))ˣ],
    Fintype.card { x : ZMod (m + 1) // x.val.Coprime (m + 1) } = φ (m + 1)
⊢ Fintype.card { x : ZMod n // x.val.Coprime n } = φ n

Tactic:
obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out

Premises used: Nat.exists_eq_succ_of_ne_zero, NeZero.out, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
m : ℕ
inst : NeZero (m + 1)
inst_1 : Fintype (ZMod (m + 1))ˣ
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)
⊢ Fintype.card { x : ZMod (m + 1) // x.val.Coprime (m + 1) } = φ (m + 1)

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)]

Premises used: Finset.card_eq_sum_ones, Fin.sum_univ_eq_sum_range, Fintype.card_subtype, Nat.totient, Nat.coprime_comm, Finset.sum_filter
-- Module: Mathlib.Data.Nat.Totient
Goal:
m : ℕ
inst : NeZero (m + 1)
inst_1 : Fintype (ZMod (m + 1))ˣ
⊢ 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:
rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 2 < n
⊢ Fact (1 < n)

Tactic:
haveI : Fact (1 < n) := ⟨one_lt_two.trans hn⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ NeZero n

Tactic:
haveI : NeZero n := NeZero.of_gt hn
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this_2 : NeZero n
this : 2 = orderOf (G := (ZMod n)ˣ) (-1)
rw : orderOf (G := (ZMod n)ˣ) (-1) ∣ Fintype.card (ZMod n)ˣ
⊢ Even (φ n)

Tactic:
rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]

Premises used: ZMod.card_units_eq_totient, even_iff_two_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this_2 : NeZero n
this : 2 = orderOf (G := (ZMod n)ˣ) (-1)
⊢ orderOf (G := (ZMod n)ˣ) (-1) ∣ Fintype.card (ZMod n)ˣ

Tactic:
orderOf_dvd_card

Premises used: orderOf_dvd_card
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this_2 : NeZero n
this : 2 = orderOf (G := (ZMod n)ˣ) (-1)
⊢ orderOf (G := (ZMod n)ˣ) (-1) ∣ Fintype.card (ZMod n)ˣ

Tactic:
exact orderOf_dvd_card

Premises used: orderOf_dvd_card
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : 2 < n
this_1 : Fact (1 < n)
this : NeZero n
suffices : 2 = orderOf (G := (ZMod n)ˣ) (-1)
⊢ Even (φ n)

Tactic:
suffices 2 = orderOf (-1 : (ZMod n)ˣ) by
    rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
    exact orderOf_dvd_card
-- Module: Mathlib.Data.Nat.Totient
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)
rw₄ rw₅ : Eq (α := ℕ) 2 2
⊢ 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']

Premises used: Units.coe_neg_one, ringChar.eq, orderOf_units, ZMod, LT.lt.ne', orderOf_neg_one, if_neg
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : m * n = 0
inl : ∀ (h : m = 0), φ (m * n) = φ m * φ n
inr : ∀ (h : n = 0), φ (m * n) = φ m * φ n
⊢ φ (m * n) = φ m * φ n

Tactic:
rcases Nat.mul_eq_zero.1 hmn0 with h | h

Premises used: Iff.mp, Nat.mul_eq_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h_1 : m.Coprime n
hmn0 : m * n = 0
h : m = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
simp only [totient_zero, mul_zero, zero_mul, h]

Premises used: MulZeroClass.zero_mul, Nat.totient_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h_1 : m.Coprime n
hmn0 : m * n = 0
h : n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
simp only [totient_zero, mul_zero, zero_mul, h]

Premises used: MulZeroClass.zero_mul, Nat.totient_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
⊢ NeZero (m * n)

Tactic:
haveI : NeZero (m * n) := ⟨hmn0⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ NeZero m

Tactic:
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this : NeZero m
⊢ NeZero n

Tactic:
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
-- 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
simp : Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
⊢ φ (m * n) = φ m * φ n

Tactic:
simp only [← ZMod.card_units_eq_totient]

Premises used: ZMod.card_units_eq_totient