awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : AddGroup G
g : G
h :
  ∀ (x : ℤ),
    Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))
        x ↔
      Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
⊢ Eq (α := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))
    (zmultiples (↑(addOrderOf g) : ℤ))

Tactic:
ext
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : AddGroup G
g : G
x : ℤ
h :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x
h₁ :
  Eq (α := G) ((((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G) x : G) (0 : G) ↔
    ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₂ : x • g = 0 ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₃ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HSMul.hSMul (β := ℤ) k (↑(addOrderOf g) : ℤ) = x
h₄ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), HMul.hMul (α := ℤ) (↑(addOrderOf g) : ℤ) (↑k : ℤ) = x
h₅ : (↑(addOrderOf g) : ℤ) ∣ x ↔ ∃ (k : ℤ), (↑(addOrderOf g) : ℤ) * k = x
h₆ : (∃ (c : ℤ), x = (↑(addOrderOf g) : ℤ) * c) ↔ ∃ (k : ℤ), (↑(addOrderOf g) : ℤ) * k = x
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) x ↔
    Membership.mem (γ := AddSubgroup ℤ) (zmultiples (↑(addOrderOf g) : ℤ)) x

Tactic:
simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]

Premises used: dvd_def, AddSubgroup.mem_zmultiples_iff, eq_comm, addOrderOf_dvd_iff_zsmul_eq_zero, zmultiplesHom_apply, Int.cast_id, zsmul_eq_mul', AddMonoidHom.mem_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Group G
g : G
⊢ Eq (α := Subgroup (Multiplicative ℤ))
    (MonoidHom.ker.{0, u_2} (M := G) ((zpowersHom G : (a : G) → Multiplicative ℤ →* G) g) : Subgroup (Multiplicative ℤ))
    (zpowers ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(orderOf g) : ℤ)) : Subgroup (Multiplicative ℤ))

Tactic:
congr_arg AddSubgroup.toSubgroup <| zmultiplesHom_ker_eq (Additive.ofMul g)

Premises used: MonoidHom.mker, Set.Mem, Additive, setOf, zmultiplesHom_ker_eq, Additive.ofMul, congr_arg, Multiplicative, MonoidHom.ker, orderOf, AddSubgroup.toSubgroup, Submonoid.comap, Set.preimage, Subgroup.zpowers, Set.singleton, Set.range, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : AddGroup G
g : G
hg : ∀ (x : G), Membership.mem (γ := AddSubgroup G) (zmultiples g) x
n : ℕ
hn : Nat.card G = n
rw : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(addOrderOf g) : ℤ))
rw₁ : Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ)) (zmultiples (↑(Nat.card.{u_2} ↥(zmultiples g)) : ℤ))
rw₂ : Eq (α := AddSubgroup ℤ) (zmultiples (↑(Nat.card G) : ℤ)) (zmultiples (↑(Nat.card.{u_2} ↥(zmultiples g)) : ℤ))
rw₃ rw₄ : Eq (α := AddSubgroup ℤ) (zmultiples (↑(Nat.card G) : ℤ)) (zmultiples (↑(Nat.card G) : ℤ))
⊢ Eq (α := AddSubgroup ℤ) (zmultiples (↑n : ℤ))
    (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g))

Tactic:
rw [zmultiplesHom_ker_eq, ← Nat.card_zmultiples, ← hn,
      Nat.card_congr (Equiv.subtypeUnivEquiv hg)]

Premises used: Nat.card_zmultiples, Equiv.subtypeUnivEquiv, zmultiplesHom_ker_eq, Nat.card_congr
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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 : ℤ
change : HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g
⊢ (zmodAddEquivOfGenerator hg hn : (a : ZMod n) → G) (↑i : ZMod n) = i • g

Tactic:
change (ZMod.cast (i : ZMod n) : ℤ) • g = i • g

Premises used: Int.cast, ZMod.cast
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
rw₁₁ rw₁₂ : Eq.{u_2 + 1} (α := G) 0 0
⊢ HSMul.hSMul (α := ℤ) (ZMod.cast (n := n) (↑i : ZMod n)) g = i • g

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]

Premises used: sub_eq_zero, zsmul_zero, sub_eq_add_neg, Int.sub_sub_self, card_nsmul_eq_zero', eq_comm, sub_zsmul, mul_zsmul', ZMod.coe_intCast, Int.emod_def, natCast_zsmul
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)
rw₁ rw₂ : i • g = i • g
⊢ Eq (α := ZMod n) (((zmodAddEquivOfGenerator hg hn).symm : (a : G) → ZMod n) (i • g) : ZMod n) ((↑i : ZMod n) : ZMod n)

Tactic:
rw [AddEquiv.symm_apply_eq, zmodAddEquivOfGenerator_apply_intCast]

Premises used: zmodAddEquivOfGenerator_apply_intCast, AddEquiv.symm_apply_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ (zmodAddEquivOfGenerator hg hn : (a : ZMod n) → G) 1 = g

Tactic:
simpa using zmodAddEquivOfGenerator_apply_intCast hg hn 1

Premises used: zmodAddEquivOfGenerator_apply_intCast, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ Eq (α := ZMod n) (((zmodAddEquivOfGenerator hg hn).symm : (a : G) → ZMod n) g : ZMod n) (1 : ZMod n)

Tactic:
simpa using zmodAddEquivOfGenerator_symm_apply_zsmul hg hn 1

Premises used: zmodAddEquivOfGenerator_symm_apply_zsmul, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
obtain :
  ∀ (g : G) (hg : Eq (α := Subgroup G) (zpowers g) ⊤),
    ∃ (p : ℕ), Nat.Prime p ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod p)
⊢ ∃ (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)

Premises used: isCyclic_iff_exists_zpowers_eq_top, inferInstance, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
h : Nat.Prime (orderOf g) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (orderOf g))
⊢ ∃ (p : ℕ), Nat.Prime p ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod p)

Tactic:
use orderOf g

Premises used: orderOf
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))
⊢ Nat.Prime (orderOf g) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (orderOf g))

Tactic:
rw [orderOf_eq_card_of_zpowers_eq_top hg]

Premises used: orderOf_eq_card_of_zpowers_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)
h₁ : Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))
⊢ Nat.Prime (Nat.card G) ∧ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))

Tactic:
constructor
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)

Tactic:
IsSimpleGroup.prime_card

Premises used: IsSimpleGroup.prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)

Tactic:
exact IsSimpleGroup.prime_card

Premises used: IsSimpleGroup.prime_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))

Tactic:
⟨(zmodAddCyclicAddEquiv (G := Additive G) inferInstance).symm⟩

Premises used: inferInstance, zmodAddCyclicAddEquiv, Nonempty.intro, AddEquiv.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : IsSimpleGroup G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Nonempty.{max 1 (u_2 + 1)} (Additive G ≃+ ZMod (Nat.card G))

Tactic:
exact ⟨(zmodAddCyclicAddEquiv (G := Additive G) inferInstance).symm⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (zmodMulEquivOfGenerator hg hn : (a : Multiplicative (ZMod n)) → G)
      ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) (↑i : ZMod n)) =
    g ^ i

Tactic:
zmodAddEquivOfGenerator_apply_intCast (G := Additive G) hg hn i

Premises used: Quotient.liftOn', AddCon.liftOn, Additive, zmodAddEquivOfGenerator_apply_intCast
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ Eq (α := Multiplicative (ZMod n))
    (((zmodMulEquivOfGenerator hg hn).symm : (a : G) → Multiplicative (ZMod n)) (g ^ i) : Multiplicative (ZMod n))
    ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) (↑i : ZMod n) : Multiplicative (ZMod n))

Tactic:
zmodAddEquivOfGenerator_symm_apply_zsmul (G := Additive G) hg hn i

Premises used: zmodAddEquivOfGenerator_symm_apply_zsmul, Quotient.liftOn', AddCon.liftOn, ZMod, Multiplicative
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
n : ℕ
hn : Nat.card G = n
⊢ (zmodMulEquivOfGenerator hg hn : (a : Multiplicative (ZMod n)) → G)
      ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) 1) =
    g

Tactic:
zmodAddEquivOfGenerator_apply_one (G := Additive G) hg hn

Premises used: Quotient.liftOn', AddCon.liftOn, Additive, zmodAddEquivOfGenerator_apply_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Group G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x
n : ℕ
hn : Nat.card G = n
⊢ Eq (α := Multiplicative (ZMod n))
    (((zmodMulEquivOfGenerator hg hn).symm : (a : G) → Multiplicative (ZMod n)) g : Multiplicative (ZMod n))
    ((Multiplicative.ofAdd : (a : ZMod n) → Multiplicative (ZMod n)) 1 : Multiplicative (ZMod n))

Tactic:
zmodAddEquivOfGenerator_symm_apply_generator (G := Additive G) hg hn

Premises used: Quotient.liftOn', AddCon.liftOn, ZMod, Multiplicative, zmodAddEquivOfGenerator_symm_apply_generator
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ IsCyclic G

Tactic:
have hGcyc := isCyclic_of_prime_card hG
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ IsCyclic G'

Tactic:
have hHcyc := isCyclic_of_prime_card hH
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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'
hcard : Nat.card G = Nat.card G'
⊢ G ≃* G'

Tactic:
apply mulEquivOfCyclicCardEq

Premises used: mulEquivOfCyclicCardEq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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'
⊢ Nat.card G = Nat.card G'

Tactic:
hG.trans hH.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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'
⊢ Nat.card G = Nat.card G'

Tactic:
exact hG.trans hH.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)

Tactic:
⟨(MonoidHom.ker_eq_bot_iff _).mp ?_, MonoidHom.range_eq_top.mp hg⟩

Premises used: MonoidHom.range_eq_top, And.intro, MonoidHom.ker_eq_bot_iff, Iff.mp, Function.Bijective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : Group G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
refine :
  Eq (α := Subgroup (Multiplicative ℤ))
    (MonoidHom.ker.{0, u_2} (M := G) ((zpowersHom G : (a : G) → Multiplicative ℤ →* G) g)) ⊥
⊢ Function.Bijective (α := Multiplicative ℤ) (β := G)
    (⇑((zpowersHom G : (a : G) → Multiplicative ℤ →* G) g : Multiplicative ℤ →* G) : (a : Multiplicative ℤ) → G)

Tactic:
refine ⟨(MonoidHom.ker_eq_bot_iff _).mp ?_, MonoidHom.range_eq_top.mp hg⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : Group G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Eq (α := Subgroup (Multiplicative ℤ))
    (MonoidHom.ker.{0, u_2} (M := G) ((zpowersHom G : (a : G) → Multiplicative ℤ →* G) g)) ⊥

Tactic:
simp [zpowersHom_ker_eq, ← infinite_zpowers, hg, Set.infinite_univ]

Premises used: infinite_zpowers, Set.infinite_univ, zpowersHom_ker_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : Group G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
⊢ Eq (α := Multiplicative ℤ) (((intEquivOfZPowersEqTop g hg).symm : (a : G) → Multiplicative ℤ) g : Multiplicative ℤ)
    ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ)

Tactic:
simp [MulEquiv.symm_apply_eq]

Premises used: MulEquiv.symm_apply_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : Group G
g : G
hg : Eq (α := Subgroup G) (zpowers g) ⊤
k : ℤ
⊢ Eq (α := Multiplicative ℤ)
    (((intEquivOfZPowersEqTop g hg).symm : (a : G) → Multiplicative ℤ) (g ^ k) : Multiplicative ℤ)
    ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) k : Multiplicative ℤ)

Tactic:
simp [← ofAdd_zsmul]

Premises used: ofAdd_zsmul
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
simp :
  HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ) <
    HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ)
⊢ LT.lt (α := G) ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) x : G)
    ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) y : G)

Tactic:
simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]

Premises used: zpowersHom_apply, intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ) <
    HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ)

Tactic:
zpow_lt_zpow_right hg1 hxy

Premises used: zpow_lt_zpow_right
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ) <
    HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ)

Tactic:
exact zpow_lt_zpow_right hg1 hxy

Premises used: zpow_lt_zpow_right
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
simp :
  HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ) <
    HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ)
⊢ LT.lt (α := G) ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) y : G)
    ((intEquivOfZPowersEqTop g hg : (a : Multiplicative ℤ) → G) x : G)

Tactic:
simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]

Premises used: zpowersHom_apply, intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ) <
    HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ)

Tactic:
zpow_right_strictAnti hg1 hxy

Premises used: zpow_right_strictAnti
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
⊢ HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) y : ℤ) <
    HPow.hPow (β := ℤ) g ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x : ℤ)

Tactic:
exact zpow_right_strictAnti hg1 hxy

Premises used: zpow_right_strictAnti
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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)

Tactic:
⟨(AddMonoidHom.ker_eq_bot_iff _).mp ?_, AddMonoidHom.range_eq_top.mp hg⟩

Premises used: AddMonoidHom.ker_eq_bot_iff, AddMonoidHom.range_eq_top, And.intro, Iff.mp, Function.Bijective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : AddGroup G
g : G
hg : Eq (α := AddSubgroup G) (zmultiples g) ⊤
refine : Eq (α := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) ⊥
⊢ Function.Bijective (α := ℤ) (β := G) (⇑((zmultiplesHom G : (a : G) → ℤ →+ G) g : ℤ →+ G) : (a : ℤ) → G)

Tactic:
refine ⟨(AddMonoidHom.ker_eq_bot_iff _).mp ?_, AddMonoidHom.range_eq_top.mp hg⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : AddGroup G
g : G
hg : Eq (α := AddSubgroup G) (zmultiples g) ⊤
⊢ Eq (α := AddSubgroup ℤ) (AddMonoidHom.ker.{0, u_2} (M := G) ((zmultiplesHom G : (a : G) → ℤ →+ G) g)) ⊥

Tactic:
simp [zmultiplesHom_ker_eq, ← infinite_zmultiples, hg, Set.infinite_univ]

Premises used: zmultiplesHom_ker_eq, infinite_zmultiples, Set.infinite_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : AddGroup G
g : G
hg : Eq (α := AddSubgroup G) (zmultiples g) ⊤
⊢ Eq (α := ℤ) (((intEquivOfZMultiplesEqTop g hg).symm : (a : G) → ℤ) g : ℤ) (1 : ℤ)

Tactic:
simp [AddEquiv.symm_apply_eq]

Premises used: AddEquiv.symm_apply_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Infinite G
inst_1 : AddGroup G
g : G
hg : Eq (α := AddSubgroup G) (zmultiples g) ⊤
k : ℤ
⊢ ((intEquivOfZMultiplesEqTop g hg).symm : (a : G) → ℤ) (k • g) = k

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
h : IsCyclic G
⊢ NeZero (Nat.card G)

Tactic:
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : Group G
inst_1 : Finite G
h : IsCyclic G
this : NeZero (Nat.card G)
rw : Nat.card.{u_2} (MulAut G) = Nat.card (ZMod (Nat.card G))ˣ
⊢ Nat.card.{u_2} (MulAut G) = (Nat.card G).totient

Tactic:
rw [← ZMod.card_units_eq_totient, ← Nat.card_eq_fintype_card]

Premises used: ZMod.card_units_eq_totient, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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 (ZMod (Nat.card G))ˣ

Tactic:
Nat.card_congr (mulAutMulEquiv G)

Premises used: IsCyclic.mulAutMulEquiv, Nat.card_congr, EquivLike.toEquiv
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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 (ZMod (Nat.card G))ˣ

Tactic:
exact Nat.card_congr (mulAutMulEquiv G)

Premises used: Nat.card_congr
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
G : Type u_2
inst : CommGroup G
hG : IsCyclic G
inst_1 : Finite G
d : ℕ
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
⊢ 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

Premises used: isCyclic_iff_exists_zpowers_eq_top, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
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
rw₆ rw₇ : Nat.card G / (Nat.card 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

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]

Premises used: MonoidHom.range_eq_map, orderOf_pow, Nat.card_zpowers, orderOf_eq_card_of_zpowers_eq_top, MonoidHom.map_zpowers, powMonoidHom_apply