awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : 0 < n
set set₁ : ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₂ set₃ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty), ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₄ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (hs : s ∈ S), ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₅ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (hs : s < n + 1 ∧ s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2),
      ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₆ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a : ℕ) (hsa : n = s * a) (b : ℕ) (hsb : s = HPow.hPow (β := ℕ) b 2),
      ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
set₇ :
  let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
  ∀ (hSne : S.Nonempty),
    let s := S.max' hSne;
    ∀ (a : ℕ) (hn : 0 < s * a) (hsa : n = s * a) (b : ℕ) (hsb : s = HPow.hPow (β := ℕ) b 2),
      ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
⊢ ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
have set₈ : let S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ (x : ℕ), s = HPow.hPow (β := ℕ) x 2};
∀ (hSne : S.Nonempty),
  let s := S.max' hSne;
  ∀ (a : ℕ) (hn : 0 < s * a) (hsa : n = s * a) (b : ℕ) (hsb : s = HPow.hPow (β := ℕ) b 2) (hlts : 0 < s) (hlta : 0 < a),
    ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
Tactic: classical
  set S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
  have hSne : S.Nonempty := by
    use 1
    have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
    simp [S, h1]
  let s := Finset.max' S hSne
  have hs : s ∈ S := Finset.max'_mem S hSne
  simp only [S, Finset.mem_filter, Finset.mem_range] at hs
  obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs
  rw [hsa] at hn
  obtain ⟨hlts, hlta⟩ := CanonicallyOrderedAdd.mul_pos.mp hn
  rw [hsb] at hsa hn hlts
  refine ⟨a, b, hlta, (pow_pos_iff two_ne_zero).mp hlts, hsa.symm, ?_⟩
  rintro x ⟨y, hy⟩
  rw [Nat.isUnit_iff]
  by_contra hx
  refine Nat.lt_le_asymm ?_ (Finset.le_max' S ((b * x) ^ 2) ?_)
  · convert!
      lt_mul_of_one_lt_right hlts
        (one_lt_pow two_ne_zero (one_lt_iff_ne_zero_and_ne_one.mpr ⟨fun h => by simp_all, hx⟩))
    using 1
    rw [mul_pow]
  · simp_rw [S, hsa, Finset.mem_filter, Finset.mem_range]
    refine ⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩ <;> use y <;> rw [hy] <;> ring
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h : 0 < n
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)
have obtain : ∀ (a₁ b₁ : ℕ) (ha₁ : 0 < a₁) (hb₁ : 0 < b₁) (hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n) (hab₂ : Squarefree a₁),
  ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)
Tactic: obtain ⟨a₁, b₁, ha₁, hb₁, hab₁, hab₂⟩ := sq_mul_squarefree_of_pos h
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)
have refine_1 : HPow.hPow (β := ℕ) (b₁.pred + 1) 2 * (a₁.pred + 1) = n
Tactic: refine ⟨a₁.pred, b₁.pred, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : HPow.hPow (β := ℕ) b₁ 2 * a₁ = n
hab₂ : Squarefree a₁
refine_1 : HPow.hPow (β := ℕ) (b₁.pred + 1) 2 * (a₁.pred + 1) = n
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) (b + 1) 2 * (a + 1) = n ∧ Squarefree (a + 1)
have refine_2 : Squarefree (a₁.pred + 1)
Tactic: refine ⟨a₁.pred, b₁.pred, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
have zero : ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = 0 ∧ Squarefree a
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
zero : ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = 0 ∧ Squarefree a
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n ∧ Squarefree a
have succ : ∀ (n : ℕ), ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a
have succ : ∀ (a b : ℕ) (h₁ : HPow.hPow (β := ℕ) b 2 * a = n.succ) (h₂ : Squarefree a),
  ∃ (a : ℕ) (b : ℕ), HPow.hPow (β := ℕ) b 2 * a = n + 1 ∧ Squarefree a
Tactic: obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
m n : ℕ
⊢ Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n
have rw : IsRelPrime m n ∧ Squarefree m ∧ Squarefree n ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n
Tactic: rw [_root_.squarefree_mul_iff, Nat.coprime_iff_isRelPrime]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
m n : ℕ
rw : IsRelPrime m n ∧ Squarefree m ∧ Squarefree n ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n
⊢ Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n
have rw₁ : IsRelPrime m n ∧ Squarefree m ∧ Squarefree n ↔ IsRelPrime m n ∧ Squarefree m ∧ Squarefree n
Tactic: rw [_root_.squarefree_mul_iff, Nat.coprime_iff_isRelPrime]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).Coprime n
have this : (m / m.gcd n).Coprime (m.gcd n)
Tactic: have : Coprime (m / gcd m n) (gcd m n) :=
    coprime_of_squarefree_mul <| by simpa [Nat.div_mul_cancel, gcd_dvd_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, p = n
have rw : ∏ p ∈ n.primeFactorsList.toFinset, p = n
Tactic: rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList,
    List.map_id', Nat.prod_primeFactorsList hn.ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : Squarefree n
rw : ∏ p ∈ n.primeFactorsList.toFinset, p = n
⊢ ∏ p ∈ n.primeFactors, p = n
have rw₁ : List.prod (List.map (fun (p : ℕ) ↦ p) n.primeFactorsList) = n
Tactic: rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList,
    List.map_id', Nat.prod_primeFactorsList hn.ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : Squarefree n
rw : ∏ p ∈ n.primeFactorsList.toFinset, p = n
rw₁ : List.prod (List.map (fun (p : ℕ) ↦ p) n.primeFactorsList) = n
⊢ ∏ p ∈ n.primeFactors, p = n
have rw₂ : n.primeFactorsList.prod = n
Tactic: rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList,
    List.map_id', Nat.prod_primeFactorsList hn.ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : Squarefree n
rw : ∏ p ∈ n.primeFactorsList.toFinset, p = n
rw₁ : List.prod (List.map (fun (p : ℕ) ↦ p) n.primeFactorsList) = n
rw₂ : n.primeFactorsList.prod = n
⊢ ∏ p ∈ n.primeFactors, p = n
have rw₃ : n = n
Tactic: rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList,
    List.map_id', Nat.prod_primeFactorsList hn.ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
⊢ primeFactors (∏ p ∈ s, p) = s
have hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
Tactic: have hn : ∏ p ∈ s, p ≠ 0 := prod_ne_zero_iff.2 fun p hp ↦ (hs _ hp).ne_zero
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
⊢ primeFactors (∏ p ∈ s, p) = s
have h : ∀ (p : ℕ), p ∈ primeFactors (∏ p ∈ s, p) ↔ p ∈ s
Tactic: ext p
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
p : ℕ
⊢ p ∈ primeFactors (∏ p ∈ s, p) ↔ p ∈ s
have h : (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s
Tactic: rw [mem_primeFactors_of_ne_zero hn, and_congr_right (fun hp ↦ hp.prime.dvd_finsetProd_iff _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : Ne (α := ℕ) (∏ p ∈ s, p) 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s
have h : (Prime p ∧ ∃ a ∈ s, p ∣ a) → p ∈ s
Tactic: refine ⟨?_, fun hp ↦ ⟨hs _ hp, _, hp, dvd_rfl⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors
have h : ∀ (p : ℕ), p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors
Tactic: ext p
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (hypothesis)
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors
have this : m / m.gcd n ≠ 0
Tactic: have : m / m.gcd n ≠ 0 := by simp [gcd_ne_zero_right hn, gcd_le_left _ hm.ne_zero.bot_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors
have h : Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
Tactic: simp only [mem_primeFactors, ne_eq, this, not_false_eq_true, and_true, not_and, mem_sdiff,
    hm.ne_zero, hn, dvd_div_iff_mul_dvd (gcd_dvd_left _ _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
have h : ∀ (hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)), (m.gcd n).Coprime p
Tactic: refine ⟨fun hp ↦ ⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, fun _ hpn ↦ hp.1.not_isUnit <| hm _ <|
    (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩, fun hp ↦
      ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
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)
⊢ (m.gcd n).Coprime p
have h : ¬p ∣ m.gcd n
Tactic: rw [coprime_comm, hp.1.1.coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a
have refine : n = HMul.hMul (α := ℕ) (∏ a ∈ n.primeFactors \ t, a) (∏ 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) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = HMul.hMul (α := ℕ) (∏ a ∈ n.primeFactors \ t, a) (∏ a ∈ t, a)
have rw : n = ∏ x ∈ n.primeFactors, x
Tactic: rw [Finset.prod_sdiff ht, prod_primeFactors_of_squarefree hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Squarefree (goal)
Goal:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
rw : n = ∏ x ∈ n.primeFactors, x
⊢ n = HMul.hMul (α := ℕ) (∏ a ∈ n.primeFactors \ t, a) (∏ a ∈ t, a)
have rw₁ : n = n
Tactic: rw [Finset.prod_sdiff ht, prod_primeFactors_of_squarefree hn]
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a : ℕ
ha : a ≤ a.pred
⊢ IsMin a
have zero : ∀ (ha : 0 ≤ pred 0), IsMin (α := ℕ) 0
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a : ℕ
ha : a ≤ a.pred
zero : ∀ (ha : 0 ≤ pred 0), IsMin (α := ℕ) 0
⊢ IsMin a
have succ : ∀ (n : ℕ) (ha : n + 1 ≤ (n + 1).pred), IsMin (n + 1)
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a < b
⊢ a ≤ b.pred
have zero : ∀ (h : a < 0), a ≤ pred 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a < b
zero : ∀ (h : a < 0), a ≤ pred 0
⊢ a ≤ b.pred
have succ : ∀ (n : ℕ) (h : a < n + 1), a ≤ (n + 1).pred
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
a n : ℕ
⊢ pred^[n + 1] a = a - (n + 1)
have rw : (pred ∘ pred^[n]) a = (a - n).pred
Tactic: rw [Function.iterate_succ', sub_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a ≤ b
⊢ Order.succ^[b - a] a = b
have rw : succ^[b - a] a = b
Tactic: rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a ≤ b
rw : succ^[b - a] a = b
⊢ Order.succ^[b - a] a = b
have rw₁ : a + (b - a) = b
Tactic: rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a ≤ b
rw : succ^[b - a] a = b
rw₁ : a + (b - a) = b
⊢ Order.succ^[b - a] a = b
have rw₂ : b = b
Tactic: rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a ≤ b
⊢ Order.pred^[b - a] b = a
have rw : pred^[b - a] b = a
Tactic: rw [pred_eq_pred, Nat.pred_iterate, tsub_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a ≤ b
rw : pred^[b - a] b = a
⊢ Order.pred^[b - a] b = a
have rw₁ : b - (b - a) = a
Tactic: rw [pred_eq_pred, Nat.pred_iterate, tsub_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Data.Nat.SuccPred (goal)
Goal:
m n a b : ℕ
h : a ≤ b
rw : pred^[b - a] b = a
rw₁ : b - (b - a) = a
⊢ Order.pred^[b - a] b = a
have rw₂ : a = a
Tactic: rw [pred_eq_pred, Nat.pred_iterate, tsub_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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 := ⋯ }
⊢ φ n = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
have rw : #({a ∈ range n | n.Coprime a}) = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ φ n = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
have rw₁ : #({a ∈ range n | n.Coprime a}) = Nat.card ↥({x ∈ range n | n.Coprime x})
Tactic: rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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})
⊢ φ n = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
have rw₂ : #({a ∈ range n | n.Coprime a}) = Fintype.card ↥({x ∈ range n | n.Coprime x})
Tactic: rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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})
⊢ φ n = Nat.card (↑{m : ℕ | m < n ∧ n.Coprime m} : Type)
have rw₃ : #({a ∈ range n | n.Coprime a}) = #({x ∈ range n | n.Coprime x})
Tactic: rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
⊢ (n + 1).gcd (1 % (n + 1)) = 1
have rw : (1 % (n + 1)).gcd (n + 1) = 1
Tactic: rw [gcd_comm, ← gcd_rec, gcd_one_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
rw : (1 % (n + 1)).gcd (n + 1) = 1
⊢ (n + 1).gcd (1 % (n + 1)) = 1
have rw₁ : (n + 1).gcd 1 = 1
Tactic: rw [gcd_comm, ← gcd_rec, gcd_one_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
rw : (1 % (n + 1)).gcd (n + 1) = 1
rw₁ : (n + 1).gcd 1 = 1
⊢ (n + 1).gcd (1 % (n + 1)) = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [gcd_comm, ← gcd_rec, gcd_one_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a n : ℕ
⊢ #({x ∈ Ico n (n + a) | a.Coprime x}) = φ a
have pp : Function.Periodic (β := Prop) (fun (x : ℕ) ↦ a.Coprime x) a
Tactic: rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
| #({x ∈ Ico k (k + n) | a.Coprime x})
have rw : #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x})
Tactic: rw [← Nat.mod_add_div n a]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + n) | a.Coprime x}) ≤ φ a * (n / a + 1)
have conv_lhs : #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x}) ≤ φ a * (n / a + 1)
Tactic: conv_lhs => rw [← Nat.mod_add_div n a]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ φ a * HAdd.hAdd (α := ℕ) 0 1
have zero : #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x}) * HAdd.hAdd (α := ℕ) 0 1
Tactic: rw [← filter_coprime_Ico_eq_totient a k]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x}) * HAdd.hAdd (α := ℕ) 0 1
have zero : #({x ∈ Ico k (k + n % a) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x})
Tactic: simp only [add_zero, mul_one, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + n % a) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x})
have zero : n % a ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x}) ≤ φ a * (n / a + 1)
have 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)
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 => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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))) | a.Coprime x}) ≤ φ a * i + φ a + φ a
have 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
Tactic: simp_rw [← add_assoc] at ih ⊢
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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) | 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})
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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) ∪ 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
have 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})
Tactic: rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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}) + φ a ≤ φ a * i + φ a + φ a
have grw : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * (i + 1) + φ a
Tactic: 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 ∈ 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
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * i + φ a + φ a
have grw₁ : φ a * (i + 1) + φ a ≤ φ a * (i + 1) + φ a
Tactic: 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 ∈ 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
have Ico : #({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: 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]