awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₅ : (i - (i - (↑n : ℤ) * (i / (↑n : ℤ)))) • g = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
rw₅ : (i - (i - (↑n : ℤ) * (i / (↑n : ℤ)))) • g = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₆ : ((↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
rw₅ : (i - (i - (↑n : ℤ) * (i / (↑n : ℤ)))) • g = 0
rw₆ : ((↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₇ : (i / (↑n : ℤ)) • HSMul.hSMul (α := ℤ) (↑n : ℤ) g = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
rw₅ : (i - (i - (↑n : ℤ) * (i / (↑n : ℤ)))) • g = 0
rw₆ : ((↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₇ : (i / (↑n : ℤ)) • HSMul.hSMul (α := ℤ) (↑n : ℤ) g = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₈ : (i / (↑n : ℤ)) • n • g = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
rw₅ : (i - (i - (↑n : ℤ) * (i / (↑n : ℤ)))) • g = 0
rw₆ : ((↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₇ : (i / (↑n : ℤ)) • HSMul.hSMul (α := ℤ) (↑n : ℤ) g = 0
rw₈ : (i / (↑n : ℤ)) • n • g = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₉ : (i / (↑(Nat.card G) : ℤ)) • Nat.card G • g = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
rw₅ : (i - (i - (↑n : ℤ) * (i / (↑n : ℤ)))) • g = 0
rw₆ : ((↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₇ : (i / (↑n : ℤ)) • HSMul.hSMul (α := ℤ) (↑n : ℤ) g = 0
rw₈ : (i / (↑n : ℤ)) • n • g = 0
rw₉ : (i / (↑(Nat.card G) : ℤ)) • Nat.card G • g = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₁₀ : HSMul.hSMul (β := G) (i / (↑(Nat.card G) : ℤ)) 0 = 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : (i % (↑n : ℤ)) • g = i • g
rw₁ : (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = i • g
rw₂ : i • g = (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g
rw₃ : i • g - (i - (↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₄ : i • g + -((i - (↑n : ℤ) * (i / (↑n : ℤ))) • g) = 0
rw₅ : (i - (i - (↑n : ℤ) * (i / (↑n : ℤ)))) • g = 0
rw₆ : ((↑n : ℤ) * (i / (↑n : ℤ))) • g = 0
rw₇ : (i / (↑n : ℤ)) • HSMul.hSMul (α := ℤ) (↑n : ℤ) g = 0
rw₈ : (i / (↑n : ℤ)) • n • g = 0
rw₉ : (i / (↑(Nat.card G) : ℤ)) • Nat.card G • g = 0
rw₁₀ : HSMul.hSMul (β := G) (i / (↑(Nat.card G) : ℤ)) 0 = 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
have rw₁₁ : Eq.{u_2 + 1} (α := G) 0 0
Tactic: rw [ZMod.coe_intCast, Int.emod_def, eq_comm, ← sub_eq_zero, sub_eq_add_neg, ← sub_zsmul,
    Int.sub_sub_self, mul_zsmul', natCast_zsmul, ← hn, card_nsmul_eq_zero', zsmul_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ Eq (α := ZMod n) (((zmodAddEquivOfGenerator hg hn).symm : (a : G) → ZMod n) (i • g) : ZMod n) ((↑i : ZMod n) : ZMod n)
have rw : i • g = (zmodAddEquivOfGenerator hg hn : (a : ZMod n) → G) (↑i : ZMod n)
Tactic: rw [AddEquiv.symm_apply_eq, zmodAddEquivOfGenerator_apply_intCast]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
rw : i • g = (zmodAddEquivOfGenerator hg hn : (a : ZMod n) → G) (↑i : ZMod n)
⊢ Eq (α := ZMod n) (((zmodAddEquivOfGenerator hg hn).symm : (a : G) → ZMod n) (i • g) : ZMod n) ((↑i : ZMod n) : ZMod n)
have rw₁ : i • g = i • g
Tactic: rw [AddEquiv.symm_apply_eq, zmodAddEquivOfGenerator_apply_intCast]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
⊢ ∃ (p : ℕ), Nat.Prime p ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod p)
have obtain : ∀ (g : G) (hg : Eq (α := Subgroup G) (zpowers g) ⊤),
  ∃ (p : ℕ), Nat.Prime p ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod p)
Tactic: obtain ⟨g, hg⟩ := isCyclic_iff_exists_zpowers_eq_top.mp (inferInstance : IsCyclic G)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ ∃ (p : ℕ), Nat.Prime p ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod p)
have h : Nat.Prime (orderOf g) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (orderOf g))
Tactic: use orderOf g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Nat.Prime (orderOf g) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (orderOf g))
have h : Nat.Prime (Nat.card G) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))
Tactic: rw [orderOf_eq_card_of_zpowers_eq_top hg]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Nat.Prime (Nat.card G) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))
have h : Nat.Prime (Nat.card G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
h : Nat.Prime (Nat.card G)
⊢ Nat.Prime (Nat.card G) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))
have h₁ : Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst : Group G
inst_1 : Group G'
inst_2 : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
⊢ G ≃* G'
have hGcyc : IsCyclic G
Tactic: have hGcyc := isCyclic_of_prime_card hG
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst : Group G
inst_1 : Group G'
inst_2 : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
hGcyc : IsCyclic G
⊢ G ≃* G'
have hHcyc : IsCyclic G'
Tactic: have hHcyc := isCyclic_of_prime_card hH
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst : Group G
inst_1 : Group G'
inst_2 : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
hGcyc : IsCyclic G
hHcyc : IsCyclic G'
⊢ G ≃* G'
have hcard : Nat.card G = Nat.card G'
Tactic: apply mulEquivOfCyclicCardEq
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : Infinite G
inst_1 : Group G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Function.Bijective (α := Multiplicative ℤ) (β := G)
    (⇑((zpowersHom G : (a : G) → Multiplicative ℤ →* G) g : Multiplicative ℤ →* G) : (a : Multiplicative ℤ) → G)
have refine : Eq (α := Subgroup (Multiplicative ℤ))
  (MonoidHom.ker.{0, u_2} (M := G) ((zpowersHom G : (a : G) → Multiplicative ℤ →* G) g)) ⊥
Tactic: refine ⟨(MonoidHom.ker_eq_bot_iff _).mp ?_, MonoidHom.range_eq_top.mp hg⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : Infinite G
inst_1 : CommGroup G
inst_2 : PartialOrder G
inst_3 : IsOrderedMonoid G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
hg1 : 1 < g
x y : Multiplicative ℤ
hxy : x < y
⊢ LT.lt (α := G) ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) x : G)
    ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) y : G)
have simp : HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ) <
  HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ)
Tactic: simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : Infinite G
inst_1 : CommGroup G
inst_2 : PartialOrder G
inst_3 : IsOrderedMonoid G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
hg1 : g < 1
x y : Multiplicative ℤ
hxy : x < y
⊢ LT.lt (α := G) ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) y : G)
    ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) x : G)
have simp : HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ) <
  HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ)
Tactic: simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : Infinite G
inst_1 : AddGroup G
g : G
hg : Eq (α := AddSubgroup G) (zmultiples g) ⊤
⊢ Function.Bijective (α := ℤ) (β := G) (⇑((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G)
have refine : Eq (α := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) ⊥
Tactic: refine ⟨(AddMonoidHom.ker_eq_bot_iff _).mp ?_, AddMonoidHom.range_eq_top.mp hg⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
h : IsCyclic G
⊢ Nat.card.{u_2} (MulAut G) = (Nat.card G).totient
have this : NeZero (Nat.card G)
Tactic: have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
h : IsCyclic G
this : NeZero (Nat.card G)
⊢ Nat.card.{u_2} (MulAut G) = (Nat.card G).totient
have rw : Nat.card.{u_2} (MulAut G) = Nat.card (ZMod (Nat.card G))ˣ
Tactic: rw [← ZMod.card_units_eq_totient, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have obtain : ∀ (g : G) (h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤),
  Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
Tactic: obtain ⟨g, h⟩ := isCyclic_iff_exists_zpowers_eq_top.mp hG
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
g : G
h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw : Nat.card.{u_2} ↥(Subgroup.map (G := G) (powMonoidHom d) ⊤) = Nat.card G / (Nat.card G).gcd d
Tactic: rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
g : G
h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
rw : Nat.card.{u_2} ↥(Subgroup.map (G := G) (powMonoidHom d) ⊤) = Nat.card G / (Nat.card G).gcd d
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw₁ : Nat.card.{u_2} ↥(Subgroup.map (powMonoidHom d) (Subgroup.zpowers g)) = Nat.card G / (Nat.card G).gcd d
Tactic: rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
g : G
h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
rw : Nat.card.{u_2} ↥(Subgroup.map (G := G) (powMonoidHom d) ⊤) = Nat.card G / (Nat.card G).gcd d
rw₁ : Nat.card.{u_2} ↥(Subgroup.map (powMonoidHom d) (Subgroup.zpowers g)) = Nat.card G / (Nat.card G).gcd d
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw₂ : Nat.card.{u_2} ↥(Subgroup.zpowers (((powMonoidHom d : G →* G) : (a : G) → G) g) : Subgroup G) =
  Nat.card G / (Nat.card G).gcd d
Tactic: rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
g : G
h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
rw : Nat.card.{u_2} ↥(Subgroup.map (G := G) (powMonoidHom d) ⊤) = Nat.card G / (Nat.card G).gcd d
rw₁ : Nat.card.{u_2} ↥(Subgroup.map (powMonoidHom d) (Subgroup.zpowers g)) = Nat.card G / (Nat.card G).gcd d
rw₂ :
  Nat.card.{u_2} ↥(Subgroup.zpowers (((powMonoidHom d : G →* G) : (a : G) → G) g) : Subgroup G) =
    Nat.card G / (Nat.card G).gcd d
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw₃ : orderOf (G := G) (((powMonoidHom d : G →* G) : (a : G) → G) g : G) = Nat.card G / (Nat.card G).gcd d
Tactic: rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
g : G
h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
rw : Nat.card.{u_2} ↥(Subgroup.map (G := G) (powMonoidHom d) ⊤) = Nat.card G / (Nat.card G).gcd d
rw₁ : Nat.card.{u_2} ↥(Subgroup.map (powMonoidHom d) (Subgroup.zpowers g)) = Nat.card G / (Nat.card G).gcd d
rw₂ :
  Nat.card.{u_2} ↥(Subgroup.zpowers (((powMonoidHom d : G →* G) : (a : G) → G) g) : Subgroup G) =
    Nat.card G / (Nat.card G).gcd d
rw₃ : orderOf (G := G) (((powMonoidHom d : G →* G) : (a : G) → G) g : G) = Nat.card G / (Nat.card G).gcd d
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw₄ : orderOf (g ^ d) = Nat.card G / (Nat.card G).gcd d
Tactic: rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
g : G
h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
rw : Nat.card.{u_2} ↥(Subgroup.map (G := G) (powMonoidHom d) ⊤) = Nat.card G / (Nat.card G).gcd d
rw₁ : Nat.card.{u_2} ↥(Subgroup.map (powMonoidHom d) (Subgroup.zpowers g)) = Nat.card G / (Nat.card G).gcd d
rw₂ :
  Nat.card.{u_2} ↥(Subgroup.zpowers (((powMonoidHom d : G →* G) : (a : G) → G) g) : Subgroup G) =
    Nat.card G / (Nat.card G).gcd d
rw₃ : orderOf (G := G) (((powMonoidHom d : G →* G) : (a : G) → G) g : G) = Nat.card G / (Nat.card G).gcd d
rw₄ : orderOf (g ^ d) = Nat.card G / (Nat.card G).gcd d
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw₅ : orderOf g / (orderOf g).gcd d = Nat.card G / (Nat.card G).gcd d
Tactic: rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
g : G
h : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
rw : Nat.card.{u_2} ↥(Subgroup.map (G := G) (powMonoidHom d) ⊤) = Nat.card G / (Nat.card G).gcd d
rw₁ : Nat.card.{u_2} ↥(Subgroup.map (powMonoidHom d) (Subgroup.zpowers g)) = Nat.card G / (Nat.card G).gcd d
rw₂ :
  Nat.card.{u_2} ↥(Subgroup.zpowers (((powMonoidHom d : G →* G) : (a : G) → G) g) : Subgroup G) =
    Nat.card G / (Nat.card G).gcd d
rw₃ : orderOf (G := G) (((powMonoidHom d : G →* G) : (a : G) → G) g : G) = Nat.card G / (Nat.card G).gcd d
rw₄ : orderOf (g ^ d) = Nat.card G / (Nat.card G).gcd d
rw₅ : orderOf g / (orderOf g).gcd d = Nat.card G / (Nat.card G).gcd d
⊢ Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw₆ : Nat.card G / (Nat.card G).gcd d = Nat.card G / (Nat.card G).gcd d
Tactic: rw [MonoidHom.range_eq_map, ← h, MonoidHom.map_zpowers, Nat.card_zpowers, powMonoidHom_apply,
    orderOf_pow, orderOf_eq_card_of_zpowers_eq_top h]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
⊢ Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw : Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
Tactic: rw [Subgroup.index_ker, card_powMonoidHom_range]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
rw : Nat.card.{u_2} ↥(MonoidHom.range (G := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
⊢ Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) = Nat.card G / (Nat.card G).gcd d
have rw₁ : Nat.card G / (Nat.card G).gcd d = Nat.card G / (Nat.card G).gcd d
Tactic: rw [Subgroup.index_ker, card_powMonoidHom_range]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := G) (powMonoidHom d)) = (Nat.card G).gcd d
have h : Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) ≠ 0
Tactic: have h : (powMonoidHom d : G →* G).ker.index ≠ 0 := Subgroup.index_ne_zero_of_finite
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
h : Subgroup.index.{u_2} (G := G) (MonoidHom.ker (M := G) (powMonoidHom d)) ≠ 0
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := G) (powMonoidHom d)) = (Nat.card G).gcd d
have rw : (Nat.card G).gcd d ∣ Nat.card G
Tactic: rw [← mul_left_inj' h, Subgroup.card_mul_index, index_powMonoidHom_ker, Nat.mul_div_cancel']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
⊢ Subgroup.index.{u_2} (G := G) (MonoidHom.range (G := G) (powMonoidHom d)) = (Nat.card G).gcd d
have rw : Nat.card.{u_2} ↥(MonoidHom.ker (M := G) (powMonoidHom d)) = (Nat.card G).gcd d
Tactic: rw [Subgroup.index_range, card_powMonoidHom_ker]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsCyclic G
inst_2 : Finite G
d : ℕ
rw : Nat.card.{u_2} ↥(MonoidHom.ker (M := G) (powMonoidHom d)) = (Nat.card G).gcd d
⊢ Subgroup.index.{u_2} (G := G) (MonoidHom.range (G := G) (powMonoidHom d)) = (Nat.card G).gcd d
have rw₁ : (Nat.card G).gcd d = (Nat.card G).gcd d
Tactic: rw [Subgroup.index_range, card_powMonoidHom_ker]