awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n
have refine_1 : ∀ (n : ℕ),
  ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) =
    ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑1 : ℝ) (↑n : ℝ)))
        fun (t : ℝ) ↦
        HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t)
          (∑ k ∈ Icc 0 ⌊t⌋₊, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
Tactic: refine Summable.congr_atTop (summable_mul_of_bigO_atTop_aux (fun n ↦ if n = 0 then 0 else c n) 1
    h_bdd (by rwa [Nat.cast_one]) (fun n ↦ ?_) hg₁ hg₂) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
refine_1 :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f (↑k : ℝ)‖ * norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) =
      ‖f (↑n : ℝ)‖ * ∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑1 : ℝ) (↑n : ℝ)))
          fun (t : ℝ) ↦
          HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t)
            (∑ k ∈ Icc 0 ⌊t⌋₊, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ f (↑n : ℝ) * c n
have refine_2 : EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ f (↑n : ℝ) * (fun (n : ℕ) ↦ if n = 0 then 0 else c n) n)
  fun (n : ℕ) ↦ f (↑n : ℝ) * c n
Tactic: refine Summable.congr_atTop (summable_mul_of_bigO_atTop_aux (fun n ↦ if n = 0 then 0 else c n) 1
    h_bdd (by rwa [Nat.cast_one]) (fun n ↦ ?_) hg₁ hg₂) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 1) t → DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (X := ℝ) (ε := ℝ) (deriv fun (t : ℝ) ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ k ∈ Icc 1 n, ‖c k‖) (∑ k ∈ Icc 0 n, norm.{u_1} (E := 𝕜) ((fun (n : ℕ) ↦ if n = 0 then 0 else c n) k))
h_bdd :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f (↑n : ℝ)‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖)
    fun (x : ℕ) ↦ 1
hg₁ :
  Asymptotics.IsBigO (E := ℝ) atTop
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ) (deriv (fun (t : ℝ) ↦ ‖f t‖) t) (∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖)) g
⊢ EventuallyEq.{0, u_1} (β := 𝕜) atTop (fun (n : ℕ) ↦ f (↑n : ℝ) * (fun (n : ℕ) ↦ if n = 0 then 0 else c n) n)
    fun (n : ℕ) ↦ f (↑n : ℝ) * c n
have h₁ : ∀ (k : ℕ) (hk : k ≠ 0), (f (↑k : ℝ) * if k = 0 then 0 else c k) = f (↑k : ℝ) * c k
Tactic: filter_upwards [eventually_ne_atTop 0] with k hk
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (λ : (a : ℕ) → ℕ) n = exponent (ZMod n)ˣ
have zero : ∀ (hn : Ne (α := ℕ) 0 0), (λ : (a : ℕ) → ℕ) 0 = exponent (ZMod 0)ˣ
Tactic: cases n with | zero => contradiction | succ n =>
  change Nat.find _ = _
  grind [exponent, ExponentExists.of_finite]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), (λ : (a : ℕ) → ℕ) 0 = exponent (ZMod 0)ˣ
⊢ (λ : (a : ℕ) → ℕ) n = exponent (ZMod n)ˣ
have succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), (λ : (a : ℕ) → ℕ) (n + 1) = exponent (ZMod (n + 1))ˣ
Tactic: cases n with | zero => contradiction | succ n =>
  change Nat.find _ = _
  grind [exponent, ExponentExists.of_finite]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
a : (ZMod n)ˣ
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) n : ℕ) = 1
have zero : ∀ (a : (ZMod 0)ˣ), HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) 0 : ℕ) = 1
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
a : (ZMod n)ˣ
zero : ∀ (a : (ZMod 0)ˣ), HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) 0 : ℕ) = 1
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) n : ℕ) = 1
have succ : ∀ (n : ℕ) (a : (ZMod (n + 1))ˣ), HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ) = 1
Tactic: cases n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a : (ZMod 0)ˣ
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) 0 : ℕ) = 1
have zero : HPow.hPow (β := ℕ) a 0 = 1
Tactic: rw [map_zero, pow_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a : (ZMod 0)ˣ
zero : HPow.hPow (β := ℕ) a 0 = 1
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) 0 : ℕ) = 1
have zero₁ : Eq (α := (ZMod 0)ˣ) 1 1
Tactic: rw [map_zero, pow_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
a : (ZMod (n + 1))ˣ
⊢ HPow.hPow (β := ℕ) a ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ) = 1
have succ : a ^ exponent (ZMod (n + 1))ˣ = 1
Tactic: rw [carmichael_eq_exponent']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
⊢ (λ : (a : ℕ) → ℕ) n ∣ φ n
have zero : (λ : (a : ℕ) → ℕ) 0 ∣ φ 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
zero : (λ : (a : ℕ) → ℕ) 0 ∣ φ 0
⊢ (λ : (a : ℕ) → ℕ) n ∣ φ n
have succ : ∀ (n : ℕ), (λ : (a : ℕ) → ℕ) (n + 1) ∣ φ (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
⊢ (λ : (a : ℕ) → ℕ) (n + 1) ∣ φ (n + 1)
have succ : exponent (ZMod (n + 1))ˣ ∣ Fintype.card (ZMod (n + 1))ˣ
Tactic: rw [← ZMod.card_units_eq_totient, carmichael_eq_exponent']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a b : ℕ
h : a ∣ b
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) b : ℕ)
have zero : ∀ (h : a ∣ 0), Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) 0 : ℕ)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a b : ℕ
h : a ∣ b
zero : ∀ (h : a ∣ 0), Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) 0 : ℕ)
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) b : ℕ)
have succ : ∀ (n : ℕ) (h : a ∣ n + 1), Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a n : ℕ
h : a ∣ n + 1
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (n + 1) : ℕ)
have succ : exponent (ZMod a)ˣ ∣ exponent (ZMod (n + 1))ˣ
Tactic: rw [carmichael_eq_exponent <| ne_zero_of_dvd_ne_zero (by lia) h, carmichael_eq_exponent']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a b : ℕ
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
have pos : ∀ (h₀ : a = 0 ∨ b = 0), (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
Tactic: by_cases! h₀ : a = 0 ∨ b = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a b : ℕ
pos : ∀ (h₀ : a = 0 ∨ b = 0), (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
have neg : ∀ (h₀ : a ≠ 0 ∧ b ≠ 0), (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
Tactic: by_cases! h₀ : a = 0 ∨ b = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
have neg : (λ : (a : ℕ) → ℕ) (a.lcm b) ∣ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
Tactic: apply dvd_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
neg : (λ : (a : ℕ) → ℕ) (a.lcm b) ∣ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
have neg₁ : Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b) ∣ (λ : (a : ℕ) → ℕ) (a.lcm b)
Tactic: apply dvd_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) ∣ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)
have neg : exponent (ZMod (a.lcm b))ˣ ∣ exponent (ZMod a × ZMod b)ˣ
Tactic: rw [carmichael_eq_exponent h₀.left, carmichael_eq_exponent h₀.right,
      carmichael_eq_exponent <| lcm_ne_zero h₀.left h₀.right, ← lcm_eq_nat_lcm <| exponent _,
      ← exponent_prod, ← exponent_eq_of_mulEquiv .prodUnits]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (hypothesis)
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b) ∣ (λ : (a : ℕ) → ℕ) (a.lcm b)
have ha : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
Tactic: have ha := carmichael_dvd <| Nat.dvd_lcm_left a b
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (hypothesis)
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
ha : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
⊢ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b) ∣ (λ : (a : ℕ) → ℕ) (a.lcm b)
have hb : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) b : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
Tactic: have hb := carmichael_dvd <| Nat.dvd_lcm_right a b
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
have refine_1 : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
Tactic: refine s.induction ?_ fun a s ha ih ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
refine_1 : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
have refine_2 : ∀ (a : α) (s : Finset α) (ha : a ∉ s)
  (ih : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)),
  Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) ((insert a s).lcm f) : ℕ) ((insert a s).lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
Tactic: refine s.induction ?_ fun a s ha ih ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
α : Type u_2
s_1 : Finset α
f : α → ℕ
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) ((insert a s).lcm f) : ℕ) ((insert a s).lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
have refine_2 : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (@GCDMonoid.lcm _ instCommMonoidWithZero _ (f a) (s.lcm f)) : ℕ)
  (@GCDMonoid.lcm _ instCommMonoidWithZero _ (((⇑λ : (a : ℕ) → ℕ) ∘ f) a) ((λ : (a : ℕ) → ℕ) (s.lcm f)) : ℕ)
Tactic: rw [Finset.lcm_insert, Finset.lcm_insert, ← ih]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
have refine_1 : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
Tactic: classical
  refine s.induction ?_ fun a s ha ih ↦ ?_
  · exact carmichael_eq_exponent' 1 |>.trans exp_eq_one_of_subsingleton
  rw [Finset.lcm_insert, Finset.lcm_insert, ← ih]
  exact carmichael_lcm ..
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
refine_1 : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
have refine_2 : ∀ (a : α) (s : Finset α) (ha : a ∉ s)
  (ih : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)),
  Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) ((insert a s).lcm f) : ℕ) ((insert a s).lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
Tactic: classical
  refine s.induction ?_ fun a s ha ih ↦ ?_
  · exact carmichael_eq_exponent' 1 |>.trans exp_eq_one_of_subsingleton
  rw [Finset.lcm_insert, Finset.lcm_insert, ← ih]
  exact carmichael_lcm ..
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
refine_1 : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
refine_2 refine_2₁ :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ih : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)),
    Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) ((insert a s).lcm f) : ℕ) ((insert a s).lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
have refine_2₂ : ∀ (a : α) (s : Finset α) (ha : a ∉ s)
  (ih : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)),
  Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (@GCDMonoid.lcm _ instCommMonoidWithZero _ (f a) (s.lcm f)) : ℕ)
    (@GCDMonoid.lcm _ instCommMonoidWithZero _ (((⇑λ : (a : ℕ) → ℕ) ∘ f) a) ((λ : (a : ℕ) → ℕ) (s.lcm f)) : ℕ)
Tactic: classical
  refine s.induction ?_ fun a s ha ih ↦ ?_
  · exact carmichael_eq_exponent' 1 |>.trans exp_eq_one_of_subsingleton
  rw [Finset.lcm_insert, Finset.lcm_insert, ← ih]
  exact carmichael_lcm ..
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) n : ℕ)
    (n.primeFactors.lcm fun (p : ℕ) ↦ (λ : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) :
      ℕ)
have nth_rw : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) : ℕ)
  (n.primeFactors.lcm fun (p : ℕ) ↦ (λ : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) :
    ℕ)
Tactic: nth_rw 1 [← n.prod_factorization_pow_eq_self <| NeZero.ne _]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≤ 2
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = φ (HPow.hPow (α := ℕ) 2 n)
have rw : exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
Tactic: rw [carmichael_eq_exponent', ← ZMod.card_units_eq_totient, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≤ 2
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
have rw : φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: rw [carmichael_two_pow_of_le_two_eq_totient hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≤ 2
⊢ φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
have 0 : ∀ (hn : LE.le (α := ℕ) 0 2), φ (HPow.hPow (α := ℕ) (β := ℕ) 2 0) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 0 1)
Tactic: interval_cases n
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≤ 2
0 : ∀ (hn : LE.le (α := ℕ) 0 2), φ (HPow.hPow (α := ℕ) (β := ℕ) 2 0) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 0 1)
⊢ φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
have 1 : ∀ (hn : LE.le (α := ℕ) 1 2), φ (HPow.hPow (α := ℕ) (β := ℕ) 2 1) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 1 1)
Tactic: interval_cases n
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≤ 2
0 : ∀ (hn : LE.le (α := ℕ) 0 2), φ (HPow.hPow (α := ℕ) (β := ℕ) 2 0) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 0 1)
1 : ∀ (hn : LE.le (α := ℕ) 1 2), φ (HPow.hPow (α := ℕ) (β := ℕ) 2 1) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 1 1)
⊢ φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
have 2 : ∀ (hn : LE.le (α := ℕ) 2 2), φ (HPow.hPow (α := ℕ) (β := ℕ) 2 2) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 2 1)
Tactic: interval_cases n
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
have pos : ∀ (hn' : n ≤ 2), (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
Tactic: by_cases hn' : n ≤ 2
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
pos : ∀ (hn' : n ≤ 2), (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
have neg : ∀ (hn' : ¬n ≤ 2), (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
Tactic: by_cases hn' : n ≤ 2
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
have neg : exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)
Tactic: refine carmichael_eq_exponent' _ |>.trans <| dvd_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
neg : exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
have neg₁ : HPow.hPow (α := ℕ) 2 (n - 2) ∣ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
Tactic: refine carmichael_eq_exponent' _ |>.trans <| dvd_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
have rw : Fintype.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia,
        Nat.add_one_sub_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
rw : Fintype.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
have rw₁ : φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia,
        Nat.add_one_sub_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
rw : Fintype.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
rw₁ : φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
have rw₂ : HPow.hPow (α := ℕ) 2 (n - 1) * HSub.hSub (α := ℕ) 2 1 = HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia,
        Nat.add_one_sub_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
rw : Fintype.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
rw₁ : φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
rw₂ : HPow.hPow (α := ℕ) 2 (n - 1) * HSub.hSub (α := ℕ) 2 1 = HPow.hPow (α := ℕ) 2 (n - 1)
rw₃ : HPow.hPow (α := ℕ) 2 (n - 1) * 1 = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
have rw₄ : HPow.hPow (α := ℕ) 2 (n - 1) = HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia,
        Nat.add_one_sub_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (hypothesis)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)
have hcard : Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: have hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1) := by
      rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia,
        Nat.add_one_sub_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)
have neg : ∀ (k : ℕ) (hk : k ≤ n - 1) (h : exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 k),
  exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)
Tactic: have ⟨k, hk, h⟩ := dvd_prime_pow prime_two |>.mp <| hcard ▸ Group.exponent_dvd_nat_card
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (hypothesis)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
k : ℕ
hk : k ≤ n - 1
h : exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 k
⊢ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)
have this : ¬exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
Tactic: have := IsCyclic.iff_exponent_eq_card.not.mp <| ZMod.isCyclic_units_two_pow_iff n |>.not.mpr hn'
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ HPow.hPow (α := ℕ) 2 (n - 2) ∣ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
have neg : orderOf five ∣ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
Tactic: rw [← ZMod.orderOf_five (n - 2), show n - 2 + 2 = n by lia,
      show (5 : ZMod (2 ^ n)) = five by rfl, orderOf_units]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Carmichael (goal)
Goal:
n : ℕ
hn : 3 ≤ n
⊢ HMul.hMul (α := ℕ) (β := ℕ) (2 : ℕ) ((λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) : ℕ) = φ (HPow.hPow (α := ℕ) 2 n)
have rw : HPow.hPow (α := ℕ) 2 (n - 2).succ = HPow.hPow (α := ℕ) 2 (n - 1) * HSub.hSub (α := ℕ) 2 1
Tactic: rw [carmichael_two_pow_of_ne_two, ← pow_succ', totient_prime_pow prime_two]