awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
neg : exponent (ZMod (a.lcm b))ˣ ∣ exponent (ZMod a × ZMod b)ˣ
⊢ (λ : (a : ℕ) → ℕ) (a.lcm b) ∣ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) 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]

Premises used: Nat.lcm_ne_zero, Monoid.exponent_eq_of_mulEquiv, And.right, Monoid.exponent_prod, And.left, lcm_eq_nat_lcm, ArithmeticFunction.carmichael_eq_exponent, Monoid.exponent, MulEquiv.prodUnits
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ exponent (ZMod (a.lcm b))ˣ ∣ exponent (ZMod a × ZMod b)ˣ

Tactic:
exponent_dvd_of_monoidHom _ <| Units.map_injective <| ZMod.castHom_injective _

Premises used: Units.map_injective, Monoid.exponent_dvd_of_monoidHom, ZMod.castHom_injective
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ exponent (ZMod (a.lcm b))ˣ ∣ exponent (ZMod a × ZMod b)ˣ

Tactic:
exact exponent_dvd_of_monoidHom _ <| Units.map_injective <| ZMod.castHom_injective _

Premises used: Units.map_injective, Monoid.exponent_dvd_of_monoidHom, ZMod.castHom_injective
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)

Tactic:
have ha := carmichael_dvd <| Nat.dvd_lcm_left a b
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
ha : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
⊢ Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) b : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)

Tactic:
have hb := carmichael_dvd <| Nat.dvd_lcm_right a b
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
ha : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
hb : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) b : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
⊢ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b) ∣ (λ : (a : ℕ) → ℕ) (a.lcm b)

Tactic:
Nat.lcm_dvd ha hb

Premises used: Nat.lcm_dvd
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
ha : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) a : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
hb : Dvd.dvd (α := ℕ) ((λ : (a : ℕ) → ℕ) b : ℕ) ((λ : (a : ℕ) → ℕ) (a.lcm b) : ℕ)
⊢ Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b) ∣ (λ : (a : ℕ) → ℕ) (a.lcm b)

Tactic:
exact Nat.lcm_dvd ha hb

Premises used: Nat.lcm_dvd
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
a b : ℕ
h : a.Coprime b
⊢ (λ : (a : ℕ) → ℕ) (a * b) = Nat.lcm ((λ : (a : ℕ) → ℕ) a) ((λ : (a : ℕ) → ℕ) b)

Tactic:
h.lcm_eq_mul ▸ carmichael_lcm ..

Premises used: Eq.rec, Nat.Coprime.lcm_eq_mul, ArithmeticFunction.carmichael_lcm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)

Tactic:
s.induction ?_ fun a s ha ih ↦ ?_

Premises used: Finset.induction
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
refine_1 : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
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) : ℕ)

Tactic:
refine s.induction ?_ fun a s ha ih ↦ ?_
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)

Tactic:
carmichael_eq_exponent' 1 |>.trans exp_eq_one_of_subsingleton

Premises used: Multiset.foldr, Finset.fold, Monoid.exp_eq_one_of_subsingleton, ArithmeticFunction.carmichael_eq_exponent', Finset.lcm, OfNat.ofNat, List.foldr, Multiset.fold, Eq.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (Finset.lcm ∅ f) : ℕ) (Finset.lcm ∅ ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)

Tactic:
exact carmichael_eq_exponent' 1 |>.trans exp_eq_one_of_subsingleton

Premises used: Monoid.exp_eq_one_of_subsingleton, ArithmeticFunction.carmichael_eq_exponent', OfNat.ofNat, Eq.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
α : Type u_2
s_1 : Finset α
f : α → ℕ
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)
refine_2 :
  Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (@GCDMonoid.lcm _ instCommMonoidWithZero _ (f a) (s.lcm f)) : ℕ)
    (@GCDMonoid.lcm _ instCommMonoidWithZero _ (((⇑λ : (a : ℕ) → ℕ) ∘ f) a) ((λ : (a : ℕ) → ℕ) (s.lcm f)) : ℕ)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) ((insert a s).lcm f) : ℕ) ((insert a s).lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)

Tactic:
rw [Finset.lcm_insert, Finset.lcm_insert, ← ih]

Premises used: Finset.lcm_insert
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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 : ℕ) → ℕ) (@GCDMonoid.lcm _ instCommMonoidWithZero _ (f a) (s.lcm f)) : ℕ)
    (@GCDMonoid.lcm _ instCommMonoidWithZero _ (((⇑λ : (a : ℕ) → ℕ) ∘ f) a) ((λ : (a : ℕ) → ℕ) (s.lcm f)) : ℕ)

Tactic:
carmichael_lcm ..

Premises used: ArithmeticFunction.carmichael_lcm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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 : ℕ) → ℕ) (@GCDMonoid.lcm _ instCommMonoidWithZero _ (f a) (s.lcm f)) : ℕ)
    (@GCDMonoid.lcm _ instCommMonoidWithZero _ (((⇑λ : (a : ℕ) → ℕ) ∘ f) a) ((λ : (a : ℕ) → ℕ) (s.lcm f)) : ℕ)

Tactic:
exact carmichael_lcm ..

Premises used: ArithmeticFunction.carmichael_lcm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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) : ℕ)
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)) : ℕ)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.lcm f) : ℕ) (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 ..

Premises used: Monoid.exp_eq_one_of_subsingleton, ArithmeticFunction.carmichael_eq_exponent', Finset.lcm_insert, OfNat.ofNat, ArithmeticFunction.carmichael_lcm, Eq.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : (↑s : Set α).Pairwise (Function.onFun Coprime f)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (s.prod f) : ℕ) (s.lcm ((⇑λ : (a : ℕ) → ℕ) ∘ f) : ℕ)

Tactic:
s.lcm_eq_prod h ▸ carmichael_finset_lcm ..

Premises used: Eq.rec, Finset.lcm_eq_prod, ArithmeticFunction.carmichael_finset_lcm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
inst : NeZero n
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 : ℕ)) :
      ℕ)
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) n : ℕ)
    (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 _]

Premises used: Nat.prod_factorization_pow_eq_self, NeZero.ne
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) : ℕ)
    (n.primeFactors.lcm fun (p : ℕ) ↦ (λ : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) :
      ℕ)

Tactic:
carmichael_finsetProd pairwise_coprime_pow_primeFactors_factorization.set_of_subtype

Premises used: Multiset.toFinset, ArithmeticFunction.carmichael_finsetProd, List.toFinset, Pairwise.set_of_subtype, Nat.primeFactors, Finsupp.prod
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := ℕ) ((λ : (a : ℕ) → ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) : ℕ)
    (n.primeFactors.lcm fun (p : ℕ) ↦ (λ : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) :
      ℕ)

Tactic:
exact carmichael_finsetProd pairwise_coprime_pow_primeFactors_factorization.set_of_subtype

Premises used: ArithmeticFunction.carmichael_finsetProd, Pairwise.set_of_subtype
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≤ 2
rw : exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = φ (HPow.hPow (α := ℕ) 2 n)

Tactic:
rw [carmichael_eq_exponent', ← ZMod.card_units_eq_totient, Fintype.card_eq_nat_card]

Premises used: ZMod.card_units_eq_totient, ArithmeticFunction.carmichael_eq_exponent', Fintype.card_eq_nat_card
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≤ 2
⊢ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ

Tactic:
IsCyclic.iff_exponent_eq_card.mp <| ZMod.isCyclic_units_two_pow_iff n |>.mpr hn

Premises used: Iff.mpr, IsCyclic.iff_exponent_eq_card, Iff.mp, ZMod.isCyclic_units_two_pow_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≤ 2
⊢ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ

Tactic:
exact IsCyclic.iff_exponent_eq_card.mp <| ZMod.isCyclic_units_two_pow_iff n |>.mpr hn

Premises used: Iff.mpr, IsCyclic.iff_exponent_eq_card, Iff.mp, ZMod.isCyclic_units_two_pow_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≤ 2
rw : φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
rw [carmichael_two_pow_of_le_two_eq_totient hn]

Premises used: ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totient
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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)
2 : ∀ (hn : LE.le (α := ℕ) 2 2), φ (HPow.hPow (α := ℕ) (β := ℕ) 2 2) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 2 1)
⊢ φ (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
interval_cases n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : LE.le (α := ℕ) 0 2
⊢ φ (HPow.hPow (α := ℕ) (β := ℕ) 2 0) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 0 1)

Tactic:
decide
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : LE.le (α := ℕ) 1 2
⊢ φ (HPow.hPow (α := ℕ) (β := ℕ) 2 1) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 1 1)

Tactic:
decide
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : LE.le (α := ℕ) 2 2
⊢ φ (HPow.hPow (α := ℕ) (β := ℕ) 2 2) = HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 2 1)

Tactic:
decide
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
pos : ∀ (hn' : n ≤ 2), (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
neg : ∀ (hn' : ¬n ≤ 2), (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)

Tactic:
by_cases hn' : n ≤ 2
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : n ≤ 2
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)

Tactic:
grind [carmichael_two_pow_of_le_two]

Premises used: ArithmeticFunction.carmichael_two_pow_of_le_two
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)

Tactic:
carmichael_eq_exponent' _ |>.trans <| dvd_antisymm ?_ ?_

Premises used: dvd_antisymm, ArithmeticFunction.carmichael_eq_exponent', Eq.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
neg : exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)
neg₁ : HPow.hPow (α := ℕ) 2 (n - 2) ∣ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
⊢ (λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) = HPow.hPow (α := ℕ) 2 (n - 2)

Tactic:
refine carmichael_eq_exponent' _ |>.trans <| dvd_antisymm ?_ ?_

Premises used: dvd_antisymm, ArithmeticFunction.carmichael_eq_exponent', Eq.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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)
rw₄ rw₅ : HPow.hPow (α := ℕ) 2 (n - 1) = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ Nat.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]

Premises used: Nat.add_one_sub_one, Nat.totient_prime_pow, ZMod.card_units_eq_totient, Nat.prime_two, mul_one, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 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]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = HPow.hPow (α := ℕ) 2 (n - 1)
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)
⊢ 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
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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))ˣ = 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'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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
this : ¬exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
⊢ k ≤ n - 2

Tactic:
grind
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
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
this : ¬exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ = Nat.card (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
⊢ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ ∣ HPow.hPow (α := ℕ) 2 (n - 2)

Tactic:
exact h ▸ Nat.pow_dvd_pow 2 (by grind)
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ n - 2 + 2 = n

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ 5 = (↑five : ZMod (2 ^ n))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ := ZMod.unitOfCoprime 5 ⋯
neg : orderOf five ∣ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ
⊢ HPow.hPow (α := ℕ) 2 (n - 2) ∣ 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]

Premises used: orderOf_units, HSub.hSub, ZMod.orderOf_five, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ orderOf five ∣ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ

Tactic:
order_dvd_exponent five

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ orderOf five ∣ exponent (ZMod (HPow.hPow (α := ℕ) 2 n))ˣ

Tactic:
exact order_dvd_exponent five

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : 3 ≤ n
rw : HPow.hPow (α := ℕ) 2 (n - 2).succ = HPow.hPow (α := ℕ) 2 (n - 1) * HSub.hSub (α := ℕ) 2 1
rw₁ : 0 < n
rw₂ : n ≠ 2
⊢ HMul.hMul (α := ℕ) (β := ℕ) (2 : ℕ) ((λ : (a : ℕ) → ℕ) (HPow.hPow (α := ℕ) 2 n) : ℕ) = φ (HPow.hPow (α := ℕ) 2 n)

Tactic:
rw [carmichael_two_pow_of_ne_two, ← pow_succ', totient_prime_pow prime_two]

Premises used: Nat.pow_succ', Nat.totient_prime_pow, Nat.prime_two, ArithmeticFunction.carmichael_two_pow_of_ne_two
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : 3 ≤ n
⊢ HPow.hPow (α := ℕ) 2 (n - 2).succ = HPow.hPow (α := ℕ) 2 (n - 1) * HSub.hSub (α := ℕ) 2 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : 3 ≤ n
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
⊢ NeZero p

Tactic:
have : NeZero p := ⟨hp.ne_zero⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
this : NeZero p
rw : exponent (ZMod (p ^ n))ˣ = Nat.card (ZMod (p ^ n))ˣ
⊢ (λ : (a : ℕ) → ℕ) (p ^ n) = φ (p ^ n)

Tactic:
rw [carmichael_eq_exponent', ← ZMod.card_units_eq_totient, Fintype.card_eq_nat_card]

Premises used: ZMod.card_units_eq_totient, ArithmeticFunction.carmichael_eq_exponent', Fintype.card_eq_nat_card
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
this : NeZero p
⊢ exponent (ZMod (p ^ n))ˣ = Nat.card (ZMod (p ^ n))ˣ

Tactic:
IsCyclic.iff_exponent_eq_card.mp <| ZMod.isCyclic_units_of_prime_pow p hp hp₂ n

Premises used: ZMod.isCyclic_units_of_prime_pow, IsCyclic.iff_exponent_eq_card, Iff.mp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael
Goal:
p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
this : NeZero p
⊢ exponent (ZMod (p ^ n))ˣ = Nat.card (ZMod (p ^ n))ˣ

Tactic:
exact IsCyclic.iff_exponent_eq_card.mp <| ZMod.isCyclic_units_of_prime_pow p hp hp₂ n

Premises used: ZMod.isCyclic_units_of_prime_pow, IsCyclic.iff_exponent_eq_card, Iff.mp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
f : ArithmeticFunction R
⊢ f.toFun = (⇑f : (a : ℕ) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
f : ℕ → R
hf : f 0 = 0
⊢ (⇑{ toFun := f, map_zero' := hf : ZeroHom ℕ R } : (a : ℕ) → R) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
f : ArithmeticFunction R
⊢ Eq (α := R) ((f : (a : ℕ) → R) 0 : R) (0 : R)

Tactic:
ZeroHom.map_zero' f

Premises used: ZeroHom.map_zero'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
f g : ArithmeticFunction R
⊢ Eq (α := (a : ℕ) → R) (⇑f : (a : ℕ) → R) (⇑g : (a : ℕ) → R) ↔ f = g

Tactic:
DFunLike.coe_fn_eq

Premises used: DFunLike.coe_fn_eq
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
h :
  ∀ (f : (a : ℕ) → R),
    Membership.mem (γ := Set ((a : ℕ) → R))
        (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))) f ↔
      Membership.mem (γ := Set ((a : ℕ) → R)) {f : (a : ℕ) → R | f 0 = 0} f
⊢ Eq.{u_1 + 1} (α := Set ((a : ℕ) → R)) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
    {f : (a : ℕ) → R | f 0 = 0}

Tactic:
ext f
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
f : ArithmeticFunction R
⊢ Membership.mem (γ := Set ((a : ℕ) → R)) {f : (a : ℕ) → R | f 0 = 0} (⇑f : (a : ℕ) → R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
f : (a : ℕ) → R
⊢ Membership.mem (γ := Set ((a : ℕ) → R)) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
      f ↔
    Membership.mem (γ := Set ((a : ℕ) → R)) {f : (a : ℕ) → R | f 0 = 0} f

Tactic:
exact ⟨by rintro ⟨f, rfl⟩; simp, fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
x : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((0 : (a : ℕ) → R) x : R) (0 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
f g : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((f : (a : ℕ) → R) x : R) ((g : (a : ℕ) → R) x : R)
⊢ f = g

Tactic:
ZeroHom.ext h

Premises used: ZeroHom.ext, ArithmeticFunction
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
x : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((1 : (a : ℕ) → R) x : R) (if x = 1 then 1 else 0 : R)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
⊢ Eq.{u_1 + 1} (α := R) ((1 : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
x : ℕ
h : x ≠ 1
⊢ Eq.{u_1 + 1} (α := R) ((1 : (a : ℕ) → R) x : R) (0 : R)

Tactic:
if_neg h

Premises used: if_neg, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
f : ArithmeticFunction ℕ
⊢ Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ ((↑((f : (a : ℕ) → ℕ) n) : R) : R)) 0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
f : ArithmeticFunction ℕ
⊢ (↑f : ArithmeticFunction ℕ) = f

Tactic:
ext fun _ => cast_id _

Premises used: ArithmeticFunction.ext, Nat.cast_id, ArithmeticFunction.natToArithmeticFunction, ArithmeticFunction.instFunLikeNat._aux_1