awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
hx : orderOf (G := QuaternionGroup 1) (xa 0) = Nat.card (QuaternionGroup 1)
x : QuaternionGroup 1
⊢ IsCyclic (QuaternionGroup 1)

Tactic:
apply isCyclic_of_orderOf_eq_card

Premises used: isCyclic_of_orderOf_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
hx : orderOf (G := QuaternionGroup 1) (xa 0) = 4
⊢ orderOf (G := QuaternionGroup 1) (xa 0) = Nat.card (QuaternionGroup 1)

Tactic:
rw [Nat.card_eq_fintype_card, card, mul_one]

Premises used: QuaternionGroup.card, mul_one, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
⊢ orderOf (G := QuaternionGroup 1) (xa 0) = 4

Tactic:
orderOf_xa 0

Premises used: QuaternionGroup.orderOf_xa, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
⊢ orderOf (G := QuaternionGroup 1) (xa 0) = 4

Tactic:
exact orderOf_xa 0

Premises used: QuaternionGroup.orderOf_xa, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inl : orderOf (G := QuaternionGroup 0) (a 1) = HMul.hMul (α := ℕ) 2 0
inr : ∀ (hn : NeZero n), orderOf (G := QuaternionGroup n) (a 1) = 2 * n
⊢ orderOf (G := QuaternionGroup n) (a 1) = 2 * n

Tactic:
rcases eq_zero_or_neZero n with rfl | hn

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
inl : ∀ (n : ℕ), 0 < n → HPow.hPow (α := QuaternionGroup 0) (QuaternionGroup.a 1) n ≠ 1
⊢ orderOf (G := QuaternionGroup 0) (a 1) = HMul.hMul (α := ℕ) 2 0

Tactic:
simp_rw [mul_zero, orderOf_eq_zero_iff']

Premises used: MulZeroClass.mul_zero, orderOf_eq_zero_iff'
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
h : 0 < n
inl : Ne (α := QuaternionGroup 0) (a (↑n : ZMod (2 * 0))) (a 0)
⊢ HPow.hPow (α := QuaternionGroup 0) (a 1) n ≠ 1

Tactic:
rw [one_def, a_one_pow]

Premises used: QuaternionGroup.one_def, QuaternionGroup.a_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
h : 0 < n
inl : ¬Eq (α := ZMod (HMul.hMul (α := ℕ) 2 0)) (↑n : ZMod (2 * 0)) 0
⊢ Ne (α := QuaternionGroup 0) (a (↑n : ZMod (2 * 0))) (a 0)

Tactic:
apply mt a.inj

Premises used: mt, QuaternionGroup.a.inj
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
h : 0 < n
⊢ CharZero (ZMod (HMul.hMul (α := ℕ) 2 0))

Tactic:
haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
h : 0 < n
this : CharZero (ZMod (HMul.hMul (α := ℕ) 2 0))
⊢ ¬Eq (α := ZMod (HMul.hMul (α := ℕ) 2 0)) (↑n : ZMod (2 * 0)) 0

Tactic:
simpa using h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
inr : ¬orderOf (G := QuaternionGroup n) (a 1) < 2 * n
⊢ orderOf (G := QuaternionGroup n) (a 1) = 2 * n

Tactic:
apply (Nat.le_of_dvd
    (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left

Premises used: QuaternionGroup.a_one_pow_n, orderOf_dvd_of_pow_eq_one, LE.le.lt_or_eq, Or.resolve_left, NeZero.pos, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := QuaternionGroup n) (a 1) < 2 * n
⊢ HPow.hPow (α := QuaternionGroup n) (a 1) (orderOf (G := QuaternionGroup n) (a 1)) = 1

Tactic:
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := QuaternionGroup n) (a 1) < 2 * n
h1 : HPow.hPow (α := QuaternionGroup n) (a 1) (orderOf (G := QuaternionGroup n) (a 1)) = 1
⊢ Eq (α := QuaternionGroup n) (a (↑(orderOf (G := QuaternionGroup n) (a 1)) : ZMod (2 * n))) 1

Tactic:
rw [a_one_pow] at h1

Premises used: QuaternionGroup.a_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := QuaternionGroup n) (a 1) < 2 * n
h1 : Eq (α := QuaternionGroup n) (a (↑(orderOf (G := QuaternionGroup n) (a 1)) : ZMod (2 * n))) 1
⊢ Eq (α := ZMod (2 * n)) (↑(orderOf (G := QuaternionGroup n) (a 1)) : ZMod (2 * n)) 0

Tactic:
injection h1 with h2
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := QuaternionGroup n) (a 1) < 2 * n
h2 : Eq (α := ZMod (2 * n)) (↑(orderOf (G := QuaternionGroup n) (a 1)) : ZMod (2 * n)) 0
⊢ orderOf (G := QuaternionGroup n) (a 1) = 0

Tactic:
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2

Premises used: Nat.mod_eq_of_lt, ZMod.val_natCast, ZMod.val_eq_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := QuaternionGroup n) (a 1) < 2 * n
h2 : orderOf (G := QuaternionGroup n) (a 1) = 0
⊢ False

Tactic:
absurd h2.symm (orderOf_pos _).ne

Premises used: absurd, Eq.symm, orderOf_pos, LT.lt.ne
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := QuaternionGroup n) (a 1) < 2 * n
h2 : orderOf (G := QuaternionGroup n) (a 1) = 0
⊢ False

Tactic:
exact absurd h2.symm (orderOf_pos _).ne

Premises used: absurd, Eq.symm, orderOf_pos, LT.lt.ne
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
rw : orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n)))
| orderOf (a i)

Tactic:
rw [← ZMod.natCast_zmod_val i]

Premises used: ZMod.natCast_zmod_val
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
conv_lhs : orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n))) = 2 * n / (2 * n).gcd i.val
⊢ orderOf (a i) = 2 * n / (2 * n).gcd i.val

Tactic:
conv_lhs => rw [← ZMod.natCast_zmod_val i]

Premises used: ZMod.natCast_zmod_val
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
rw : orderOf (HPow.hPow (α := QuaternionGroup n) (a 1) i.val) = 2 * n / (2 * n).gcd i.val
rw₁ :
  orderOf (G := QuaternionGroup n) (a 1) / (orderOf (G := QuaternionGroup n) (a 1)).gcd i.val =
    2 * n / (2 * n).gcd i.val
rw₂ rw₃ : 2 * n / (2 * n).gcd i.val = 2 * n / (2 * n).gcd i.val
⊢ orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n))) = 2 * n / (2 * n).gcd i.val

Tactic:
rw [← a_one_pow, orderOf_pow, orderOf_a_one]

Premises used: QuaternionGroup.orderOf_a_one, orderOf_pow, QuaternionGroup.a_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
rw : Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) (HMul.hMul (α := ℕ) 2 2)
⊢ Monoid.exponent (QuaternionGroup n) = 2 * @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]

Premises used: lcm_mul_left, OfNat.ofNat, normalize_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inl : Monoid.exponent (QuaternionGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ (HMul.hMul (α := ℕ) 2 0) 4
inr : ∀ (hn : NeZero n), Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
⊢ Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4

Tactic:
rcases eq_zero_or_neZero n with rfl | hn

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
⊢ Monoid.exponent (QuaternionGroup 0) = 0

Tactic:
Monoid.exponent_eq_zero_of_order_zero orderOf_a_one

Premises used: QuaternionGroup.orderOf_a_one, Monoid.exponent_eq_zero_of_order_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
⊢ Monoid.exponent (QuaternionGroup 0) = 0

Tactic:
exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one

Premises used: Monoid.exponent_eq_zero_of_order_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
inr : Monoid.exponent (QuaternionGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
inr₁ : @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
⊢ Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4

Tactic:
apply Nat.dvd_antisymm

Premises used: Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
inr : ∀ (g : QuaternionGroup n), g ^ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 = 1
⊢ Monoid.exponent (QuaternionGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4

Tactic:
apply Monoid.exponent_dvd_of_forall_pow_eq_one

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
inr : 2 * n / (2 * n).gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
⊢ a m ^ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]

Premises used: QuaternionGroup.orderOf_a, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n / (2 * n).gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4

Tactic:
Nat.dvd_trans ⟨gcd (2 * n) m.val, ?_⟩ (dvd_lcm_left (2 * n) 4)

Premises used: HMul.hMul, Nat.dvd_trans, dvd_lcm_left, GCDMonoid.gcd, Exists.intro, OfNat.ofNat, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
inr : 2 * n = 2 * n / (2 * n).gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ (2 * n) m.val
⊢ 2 * n / (2 * n).gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4

Tactic:
refine Nat.dvd_trans ⟨gcd (2 * n) m.val, ?_⟩ (dvd_lcm_left (2 * n) 4)

Premises used: HMul.hMul, Nat.dvd_trans, dvd_lcm_left, GCDMonoid.gcd, Exists.intro, OfNat.ofNat, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n = 2 * n / (2 * n).gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ (2 * n) m.val

Tactic:
(Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel, HMul.hMul, OfNat.ofNat, Eq.symm, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n = 2 * n / (2 * n).gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ (2 * n) m.val

Tactic:
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm

Premises used: Nat.gcd_dvd_left, Nat.div_mul_cancel, HMul.hMul, OfNat.ofNat, Eq.symm, ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
inr : 4 ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
⊢ xa m ^ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]

Premises used: QuaternionGroup.orderOf_xa, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 4 ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4

Tactic:
dvd_lcm_right (2 * n) 4

Premises used: HMul.hMul, dvd_lcm_right, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 4 ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4

Tactic:
exact dvd_lcm_right (2 * n) 4

Premises used: HMul.hMul, dvd_lcm_right, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
inr : 2 * n ∣ Monoid.exponent (QuaternionGroup n)
inr₁ : 4 ∣ Monoid.exponent (QuaternionGroup n)
⊢ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
apply lcm_dvd

Premises used: lcm_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
⊢ orderOf (G := QuaternionGroup n) (a 1) ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
Monoid.order_dvd_exponent (a 1)

Premises used: Monoid.order_dvd_exponent, QuaternionGroup.a, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : 2 * n = orderOf (G := QuaternionGroup n) (a 1)
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
convert! Monoid.order_dvd_exponent (a 1)

Premises used: Monoid.order_dvd_exponent, QuaternionGroup.a, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
⊢ 2 * n = orderOf (G := QuaternionGroup n) (a 1)

Tactic:
orderOf_a_one.symm

Premises used: QuaternionGroup.orderOf_a_one, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
⊢ 2 * n = orderOf (G := QuaternionGroup n) (a 1)

Tactic:
exact orderOf_a_one.symm

Premises used: QuaternionGroup.orderOf_a_one, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
⊢ orderOf (G := QuaternionGroup n) (xa 0) ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))

Premises used: Monoid.order_dvd_exponent, QuaternionGroup.xa, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
h : 4 = orderOf (G := QuaternionGroup n) (xa 0)
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
convert! Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))

Premises used: Monoid.order_dvd_exponent, QuaternionGroup.xa, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
⊢ 4 = orderOf (G := QuaternionGroup n) (xa 0)

Tactic:
(orderOf_xa 0).symm

Premises used: QuaternionGroup.orderOf_xa, OfNat.ofNat, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
hn : NeZero n
⊢ 4 = orderOf (G := QuaternionGroup n) (xa 0)

Tactic:
exact (orderOf_xa 0).symm

Premises used: QuaternionGroup.orderOf_xa, OfNat.ofNat, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : IsCyclic G
⊢ IsZGroup G

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, IsZGroup.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : IsZGroup G
p : ℕ
inst_4 : Fact (Nat.Prime p)
P : Sylow p G
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
isZGroup p Fact.out P

Premises used: IsZGroup.isZGroup, Fact.out
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsZGroup G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
obtain : ∀ (Q : Sylow p G) (hQ : P ≤ (↑Q : Subgroup G)), IsCyclic.{u_1} ↥P
⊢ IsCyclic.{u_1} ↥P

Tactic:
obtain ⟨Q, hQ⟩ := hP.exists_le_sylow

Premises used: IsPGroup.exists_le_sylow
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsZGroup G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
Q : Sylow p G
hQ : P ≤ (↑Q : Subgroup G)
⊢ IsCyclic.{u_1} ↥P

Tactic:
Subgroup.isCyclic_of_le hQ

Premises used: Subgroup.isCyclic_of_le
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : IsZGroup G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
Q : Sylow p G
hQ : P ≤ (↑Q : Subgroup G)
⊢ IsCyclic.{u_1} ↥P

Tactic:
exact Subgroup.isCyclic_of_le hQ

Premises used: Subgroup.isCyclic_of_le
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
⊢ Finite G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero hG.ne_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
this : Finite G
⊢ IsZGroup G

Tactic:
⟨fun p hp P ↦ ?_⟩

Premises used: IsZGroup.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
this : Finite G
refine : ∀ (p : ℕ) (hp : Nat.Prime p) (P : Sylow p G), IsCyclic.{u_1} ↥(↑P : Subgroup G)
⊢ IsZGroup G

Tactic:
refine ⟨fun p hp P ↦ ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
this : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
⊢ Fact (Nat.Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
this_1 : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
obtain : ∀ (k : ℕ) (hk : Nat.card.{u_1} ↥(↑P : Subgroup G) = p ^ k), IsCyclic.{u_1} ↥(↑P : Subgroup G)
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
obtain ⟨k, hk⟩ := P.2.exists_card_eq

Premises used: Sylow.isPGroup', IsPGroup.exists_card_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
this_1 : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
k : ℕ
hk : Nat.card.{u_1} ↥(↑P : Subgroup G) = p ^ k
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
isCyclic_of_card_dvd_prime ((hk ▸ hG.pow_dvd_of_pow_dvd) P.card_subgroup_dvd_card)

Premises used: isCyclic_of_card_dvd_prime
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
this_1 : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
k : ℕ
hk : Nat.card.{u_1} ↥(↑P : Subgroup G) = p ^ k
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
exact isCyclic_of_card_dvd_prime ((hk ▸ hG.pow_dvd_of_pow_dvd) P.card_subgroup_dvd_card)

Premises used: isCyclic_of_card_dvd_prime
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hG' : IsZGroup G'
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw :
  ∀ (hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic.{u_2} ↥(↑P : Subgroup G'))
    (hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')) (p : ℕ),
    Nat.Prime p → ∀ (P : Sylow p G), IsCyclic.{u_1} ↥(↑P : Subgroup G)
⊢ IsZGroup G

Tactic:
rw [isZGroup_iff] at hG' ⊢

Premises used: isZGroup_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic.{u_2} ↥(↑P : Subgroup G')
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G
obtain :
  ∀ (Q : Sylow p G') (hQ : Subgroup.comap f (↑Q : Subgroup G') = (↑P : Subgroup G)), IsCyclic.{u_1} ↥(↑P : Subgroup G)
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
obtain ⟨Q, hQ⟩ := P.exists_comap_eq_of_injective hf

Premises used: Sylow.exists_comap_eq_of_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic.{u_2} ↥(↑P : Subgroup G')
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f (↑Q : Subgroup G') = (↑P : Subgroup G)
⊢ IsCyclic.{u_2} ↥(↑Q : Subgroup G')

Tactic:
specialize hG' p hp Q
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f (↑Q : Subgroup G') = (↑P : Subgroup G)
hG' : IsCyclic.{u_2} ↥(↑Q : Subgroup G')
⊢ Subgroup.map f (↑P : Subgroup G) ≤ (↑Q : Subgroup G')

Tactic:
have h : Subgroup.map f P ≤ Q := hQ ▸ Subgroup.map_comap_le f ↑Q
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f (↑Q : Subgroup G') = (↑P : Subgroup G)
hG' : IsCyclic.{u_2} ↥(↑Q : Subgroup G')
h : Subgroup.map f (↑P : Subgroup G) ≤ (↑Q : Subgroup G')
⊢ IsCyclic.{u_2} ↥(Subgroup.map f (↑P : Subgroup G))

Tactic:
have := isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe h).surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f (↑Q : Subgroup G') = (↑P : Subgroup G)
hG' : IsCyclic.{u_2} ↥(↑Q : Subgroup G')
h : Subgroup.map f (↑P : Subgroup G) ≤ (↑Q : Subgroup G')
this : IsCyclic.{u_2} ↥(Subgroup.map f (↑P : Subgroup G))
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
isCyclic_of_surjective _ (Subgroup.equivMapOfInjective P f hf).symm.surjective

Premises used: isCyclic_of_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f (↑Q : Subgroup G') = (↑P : Subgroup G)
hG' : IsCyclic.{u_2} ↥(↑Q : Subgroup G')
h : Subgroup.map f (↑P : Subgroup G) ≤ (↑Q : Subgroup G')
this : IsCyclic.{u_2} ↥(Subgroup.map f (↑P : Subgroup G))
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
exact isCyclic_of_surjective _ (Subgroup.equivMapOfInjective P f hf).symm.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective, MulEquiv.symm, Subgroup.equivMapOfInjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : IsZGroup G
H : Subgroup G
⊢ IsZGroup.{u_1} ↥H

Tactic:
of_injective H.subtype_injective

Premises used: Subgroup.subtype_injective, IsZGroup.of_injective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : Finite G
hG : IsZGroup G
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw :
  ∀ (hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic.{u_1} ↥(↑P : Subgroup G))
    (hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')) (p : ℕ),
    Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic.{u_2} ↥(↑P : Subgroup G')
⊢ IsZGroup G'

Tactic:
rw [isZGroup_iff] at hG ⊢

Premises used: isZGroup_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic.{u_1} ↥(↑P : Subgroup G)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
⊢ Fact (Nat.Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic.{u_1} ↥(↑P : Subgroup G)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
obtain : ∀ (Q : Sylow p G), IsCyclic.{u_2} ↥(↑(Sylow.mapSurjective hf Q) : Subgroup G')
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')

Tactic:
obtain ⟨Q, rfl⟩ := Sylow.mapSurjective_surjective hf p P

Premises used: Sylow.mapSurjective_surjective, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic.{u_1} ↥(↑P : Subgroup G)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
Q : Sylow p G
⊢ IsCyclic.{u_1} ↥(↑Q : Subgroup G)

Tactic:
specialize hG p hp Q
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : Finite G
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
Q : Sylow p G
hG : IsCyclic.{u_1} ↥(↑Q : Subgroup G)
⊢ IsCyclic.{u_2} ↥(↑(Sylow.mapSurjective hf Q) : Subgroup G')

Tactic:
isCyclic_of_surjective _ (f.subgroupMap_surjective Q)

Premises used: Sylow.toSubgroup, isCyclic_of_surjective, MonoidHom.subgroupMap_surjective