awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : Eq (α := QuaternionGroup n) (a (↑n : ZMod (2 * n))) 1
⊢ False
have h' : Eq (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) 0
Tactic: injection h with h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : Eq (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) 0
⊢ False
have h'₁ : ZMod.val (n := 2 * n) (↑n : ZMod (2 * n)) = ZMod.val (n := 2 * n) 0
Tactic: apply_fun ZMod.val at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ZMod.val (n := 2 * n) (↑n : ZMod (2 * n)) = ZMod.val (n := 2 * n) 0
⊢ False
have h'₁ : ZMod.val (n := 2 * n) (↑n : ZMod (2 * n)) / n = ZMod.val (n := 2 * n) 0 / n
Tactic: apply_fun (· / n) at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
⊢ IsCyclic (QuaternionGroup 1)
have hx : orderOf (G := QuaternionGroup 1) (xa 0) = Nat.card (QuaternionGroup 1)
Tactic: apply isCyclic_of_orderOf_eq_card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
hx : orderOf (G := QuaternionGroup 1) (xa 0) = Nat.card (QuaternionGroup 1)
⊢ IsCyclic (QuaternionGroup 1)
have x : QuaternionGroup 1
Tactic: apply isCyclic_of_orderOf_eq_card
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
⊢ orderOf (G := QuaternionGroup 1) (xa 0) = Nat.card (QuaternionGroup 1)
have hx : orderOf (G := QuaternionGroup 1) (xa 0) = 4
Tactic: rw [Nat.card_eq_fintype_card, card, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
⊢ orderOf (G := QuaternionGroup n) (a 1) = 2 * n
have inl : orderOf (G := QuaternionGroup 0) (a 1) = HMul.hMul (α := ℕ) 2 0
Tactic: rcases eq_zero_or_neZero n with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inl : orderOf (G := QuaternionGroup 0) (a 1) = HMul.hMul (α := ℕ) 2 0
⊢ orderOf (G := QuaternionGroup n) (a 1) = 2 * n
have inr : ∀ (hn : NeZero n), orderOf (G := QuaternionGroup n) (a 1) = 2 * n
Tactic: rcases eq_zero_or_neZero n with rfl | hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
⊢ orderOf (G := QuaternionGroup 0) (a 1) = HMul.hMul (α := ℕ) 2 0
have inl : ∀ (n : ℕ), 0 < n → HPow.hPow (α := QuaternionGroup 0) (QuaternionGroup.a 1) n ≠ 1
Tactic: simp_rw [mul_zero, orderOf_eq_zero_iff']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
h : 0 < n
⊢ HPow.hPow (α := QuaternionGroup 0) (a 1) n ≠ 1
have inl : Ne (α := QuaternionGroup 0) (a (↑n : ZMod (2 * 0))) (a 0)
Tactic: rw [one_def, a_one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
h : 0 < n
⊢ Ne (α := QuaternionGroup 0) (a (↑n : ZMod (2 * 0))) (a 0)
have inl : ¬Eq (α := ZMod (HMul.hMul (α := ℕ) 2 0)) (↑n : ZMod (2 * 0)) 0
Tactic: apply mt a.inj
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
h : 0 < n
⊢ ¬Eq (α := ZMod (HMul.hMul (α := ℕ) 2 0)) (↑n : ZMod (2 * 0)) 0
have this : CharZero (ZMod (HMul.hMul (α := ℕ) 2 0))
Tactic: haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ orderOf (G := QuaternionGroup n) (a 1) = 2 * n
have inr : ¬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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := QuaternionGroup n) (a 1) < 2 * n
⊢ False
have h1 : 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 _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
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
⊢ False
have h1₁ : Eq (α := QuaternionGroup n) (a (↑(orderOf (G := QuaternionGroup n) (a 1)) : ZMod (2 * n))) 1
Tactic: rw [a_one_pow] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
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
⊢ False
have h2 : Eq (α := ZMod (2 * n)) (↑(orderOf (G := QuaternionGroup n) (a 1)) : ZMod (2 * n)) 0
Tactic: injection h1 with h2
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (hypothesis)
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
⊢ False
have h2₁ : orderOf (G := QuaternionGroup n) (a 1) = 0
Tactic: rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
| orderOf (a i)
have rw : orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n)))
Tactic: rw [← ZMod.natCast_zmod_val i]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a i) = 2 * n / (2 * n).gcd i.val
have conv_lhs : orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n))) = 2 * n / (2 * n).gcd i.val
Tactic: conv_lhs => rw [← ZMod.natCast_zmod_val i]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
⊢ orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n))) = 2 * n / (2 * n).gcd i.val
have rw : orderOf (HPow.hPow (α := QuaternionGroup n) (a 1) i.val) = 2 * n / (2 * n).gcd i.val
Tactic: rw [← a_one_pow, orderOf_pow, orderOf_a_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
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
⊢ orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n))) = 2 * n / (2 * n).gcd i.val
have rw₁ : orderOf (G := QuaternionGroup n) (a 1) / (orderOf (G := QuaternionGroup n) (a 1)).gcd i.val = 2 * n / (2 * n).gcd i.val
Tactic: rw [← a_one_pow, orderOf_pow, orderOf_a_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
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
⊢ orderOf (G := QuaternionGroup n) (a (↑i.val : ZMod (2 * n))) = 2 * n / (2 * n).gcd i.val
have rw₂ : 2 * n / (2 * n).gcd i.val = 2 * n / (2 * n).gcd i.val
Tactic: rw [← a_one_pow, orderOf_pow, orderOf_a_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = 2 * @lcm _ Nat.instCommMonoidWithZero _ n 2
have rw : Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) (HMul.hMul (α := ℕ) 2 2)
Tactic: rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
have inl : Monoid.exponent (QuaternionGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ (HMul.hMul (α := ℕ) 2 0) 4
Tactic: rcases eq_zero_or_neZero n with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
inl : Monoid.exponent (QuaternionGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ (HMul.hMul (α := ℕ) 2 0) 4
⊢ Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
have inr : ∀ (hn : NeZero n), Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
Tactic: rcases eq_zero_or_neZero n with rfl | hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
have inr : Monoid.exponent (QuaternionGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
inr : Monoid.exponent (QuaternionGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
⊢ Monoid.exponent (QuaternionGroup n) = @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
have inr₁ : @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
have inr : ∀ (g : QuaternionGroup n), g ^ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 = 1
Tactic: apply Monoid.exponent_dvd_of_forall_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 = 1
have inr : 2 * n / (2 * n).gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n / (2 * n).gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
have inr : 2 * n = 2 * n / (2 * n).gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ (2 * n) m.val
Tactic: refine Nat.dvd_trans ⟨gcd (2 * n) m.val, ?_⟩ (dvd_lcm_left (2 * n) 4)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 = 1
have inr : 4 ∣ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
have inr : 2 * n ∣ Monoid.exponent (QuaternionGroup n)
Tactic: apply lcm_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
inr : 2 * n ∣ Monoid.exponent (QuaternionGroup n)
⊢ @lcm _ Nat.instCommMonoidWithZero _ (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
have inr₁ : 4 ∣ Monoid.exponent (QuaternionGroup n)
Tactic: apply lcm_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)
have h : 2 * n = orderOf (G := QuaternionGroup n) (a 1)
Tactic: convert! Monoid.order_dvd_exponent (a 1)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Quaternion (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)
have h : 4 = orderOf (G := QuaternionGroup n) (xa 0)
Tactic: convert! Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ IsCyclic.{u_1} ↥P
have obtain : ∀ (Q : Sylow p G) (hQ : P ≤ (↑Q : Subgroup G)), IsCyclic.{u_1} ↥P
Tactic: obtain ⟨Q, hQ⟩ := hP.exists_le_sylow
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
⊢ IsZGroup G
have this : Finite G
Tactic: have : Finite G := Nat.finite_of_card_ne_zero hG.ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
hG : Squarefree (Nat.card G)
this : Finite G
⊢ IsZGroup G
have refine : ∀ (p : ℕ) (hp : Nat.Prime p) (P : Sylow p G), IsCyclic.{u_1} ↥(↑P : Subgroup G)
Tactic: refine ⟨fun p hp P ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)
have this₁ : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)
have obtain : ∀ (k : ℕ) (hk : Nat.card.{u_1} ↥(↑P : Subgroup G) = p ^ k), IsCyclic.{u_1} ↥(↑P : Subgroup G)
Tactic: obtain ⟨k, hk⟩ := P.2.exists_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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')
⊢ IsZGroup G
have 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)
Tactic: rw [isZGroup_iff] at hG' ⊢
Cleared hypotheses: hG', hf
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)
have obtain : ∀ (Q : Sylow p G') (hQ : Subgroup.comap f (↑Q : Subgroup G') = (↑P : Subgroup G)), IsCyclic.{u_1} ↥(↑P : Subgroup G)
Tactic: obtain ⟨Q, hQ⟩ := P.exists_comap_eq_of_injective hf
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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_1} ↥(↑P : Subgroup G)
have hG'₁ : IsCyclic.{u_2} ↥(↑Q : Subgroup G')
Tactic: specialize hG' p hp Q
Cleared hypotheses: hG'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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')
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)
have h : Subgroup.map f (↑P : Subgroup G) ≤ (↑Q : Subgroup G')
Tactic: have h : Subgroup.map f P ≤ Q := hQ ▸ Subgroup.map_comap_le f ↑Q
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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_1} ↥(↑P : Subgroup G)
have this : IsCyclic.{u_2} ↥(Subgroup.map f (↑P : Subgroup G))
Tactic: have := isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe h).surjective
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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')
⊢ IsZGroup G'
have 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')
Tactic: rw [isZGroup_iff] at hG ⊢
Cleared hypotheses: hG, hf
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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'
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have this : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have obtain : ∀ (Q : Sylow p G), IsCyclic.{u_2} ↥(↑(Sylow.mapSurjective hf Q) : Subgroup G')
Tactic: obtain ⟨Q, rfl⟩ := Sylow.mapSurjective_surjective hf p P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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_2} ↥(↑(Sylow.mapSurjective hf Q) : Subgroup G')
have hG₁ : IsCyclic.{u_1} ↥(↑Q : Subgroup G)
Tactic: specialize hG p hp Q
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
inst_3 : Nontrivial G
p : ℕ := (Nat.card G).minFac
⊢ LT.lt (α := Subgroup G) (commutator G) ⊤
have hp : Nat.Prime p
Tactic: have hp : p.Prime := Nat.minFac_prime Finite.one_lt_card.ne'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
inst_3 : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
⊢ LT.lt (α := Subgroup G) (commutator G) ⊤
have this : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
inst_3 : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ LT.lt (α := Subgroup G) (commutator G) ⊤
have hP : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Tactic: have hP := isZGroup p hp P
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
inst_3 : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic.{u_1} ↥(↑P : Subgroup G)
f : G →* ↥(↑P : Subgroup G) := MonoidHom.transferSylow P ⋯
⊢ LT.lt (α := Subgroup G) (commutator G) ⊤
have refine : f.ker < ⊤
Tactic: refine lt_of_le_of_lt (Abelianization.commutator_subset_ker f) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
inst_3 : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic.{u_1} ↥(↑P : Subgroup G)
f : G →* ↥(↑P : Subgroup G) := MonoidHom.transferSylow P ⋯
⊢ f.ker < ⊤
have h : (↑P : Subgroup G) ≠ ⊥
Tactic: have h := P.ne_bot_of_dvd_card (Nat.card G).minFac_dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
inst_3 : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic.{u_1} ↥(↑P : Subgroup G)
f : G →* ↥(↑P : Subgroup G) := MonoidHom.transferSylow P ⋯
h : (↑P : Subgroup G) ≠ ⊥
⊢ f.ker < ⊤
have contrapose : ∀ (h : ¬f.ker < ⊤), (↑P : Subgroup G) = ⊥
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
inst_3 : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic.{u_1} ↥(↑P : Subgroup G)
f : G →* ↥(↑P : Subgroup G) := MonoidHom.transferSylow P ⋯
h : ¬f.ker < ⊤
⊢ (↑P : Subgroup G) = ⊥
have rw : f.ker.IsComplement' (↑P : Subgroup G)
Tactic: rw [← Subgroup.isComplement'_top_left, ← (not_lt_top_iff.mp h)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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 : Finite G
inst_4 : IsZGroup G
⊢ IsSolvable G
have rw : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
Tactic: rw [isSolvable_iff_commutator_lt]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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 : Finite G
inst_4 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
⊢ ⁅H, H⁆ < H
have h₁ : Nontrivial.{u_1} ↥H
Tactic: rw [← H.nontrivial_iff_ne_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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 : Finite G
inst_4 : IsZGroup G
H : Subgroup G
h : Nontrivial.{u_1} ↥H
⊢ ⁅H, H⁆ < H
have rw : LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤
Tactic: rw [← H.range_subtype, MonoidHom.range_eq_map, ← Subgroup.map_commutator,
    Subgroup.map_subtype_lt_map_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
⊢ Monoid.exponent G = Nat.card G
have refine : Nat.card G ∣ Monoid.exponent G
Tactic: refine dvd_antisymm Group.exponent_dvd_nat_card ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
⊢ Nat.card G ∣ Monoid.exponent G
have rw : ∀ (p : ℕ),
  Nat.Prime p →
    LE.le (α := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
      (((Monoid.exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← Nat.factorization_prime_le_iff_dvd Nat.card_pos.ne' Monoid.exponent_ne_zero_of_finite]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ LE.le (α := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
    (((Monoid.exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have this : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp