awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact isCyclic_of_surjective _ (f.subgroupMap_surjective Q)

Premises used: Sylow.toSubgroup, isCyclic_of_surjective, MonoidHom.subgroupMap_surjective
-- 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 : Finite G
inst_4 : IsZGroup G
H : Subgroup G
inst_5 : H.Normal
⊢ IsZGroup.{u_1} (G ⧸ H)

Tactic:
of_surjective (QuotientGroup.mk'_surjective H)

Premises used: QuotientGroup.mk'_surjective, IsZGroup.of_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
⊢ Nat.Prime p

Tactic:
have hp : p.Prime := Nat.minFac_prime Finite.one_lt_card.ne'
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
⊢ Fact (Nat.Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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
⊢ IsCyclic.{u_1} ↥(↑P : Subgroup G)

Tactic:
have hP := isZGroup p hp P
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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) ⊤

Tactic:
lt_of_le_of_lt (Abelianization.commutator_subset_ker f) ?_

Premises used: lt_of_le_of_lt, Abelianization.commutator_subset_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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 ⋯
refine : f.ker < ⊤
⊢ LT.lt (α := Subgroup G) (commutator G) ⊤

Tactic:
refine lt_of_le_of_lt (Abelianization.commutator_subset_ker f) ?_

Premises used: lt_of_le_of_lt, Abelianization.commutator_subset_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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 ⋯
⊢ (↑P : Subgroup G) ≠ ⊥

Tactic:
have h := P.ne_bot_of_dvd_card (Nat.card G).minFac_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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) ≠ ⊥
contrapose : ∀ (h : ¬f.ker < ⊤), (↑P : Subgroup G) = ⊥
⊢ f.ker < ⊤

Tactic:
contrapose h
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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 < ⊤
rw : f.ker.IsComplement' (↑P : Subgroup G)
⊢ (↑P : Subgroup G) = ⊥

Tactic:
rw [← Subgroup.isComplement'_top_left, ← (not_lt_top_iff.mp h)]

Premises used: Subgroup.isComplement'_top_left, not_lt_top_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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 < ⊤
⊢ f.ker.IsComplement' (↑P : Subgroup G)

Tactic:
hP.isComplement' rfl

Premises used: IsCyclic.isComplement', Set.Mem, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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 < ⊤
⊢ f.ker.IsComplement' (↑P : Subgroup G)

Tactic:
exact hP.isComplement' rfl

Premises used: IsCyclic.isComplement', rfl
-- 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 : Finite G
inst_4 : IsZGroup G
rw : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable G

Tactic:
rw [isSolvable_iff_commutator_lt]

Premises used: isSolvable_iff_commutator_lt
-- 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 : Finite G
inst_4 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
⊢ Nontrivial.{u_1} ↥H

Tactic:
rw [← H.nontrivial_iff_ne_bot] at h

Premises used: Subgroup.nontrivial_iff_ne_bot
-- 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 : Finite G
inst_4 : IsZGroup G
H : Subgroup G
h : Nontrivial.{u_1} ↥H
rw : LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤
⊢ ⁅H, H⁆ < H

Tactic:
rw [← H.range_subtype, MonoidHom.range_eq_map, ← Subgroup.map_commutator,
    Subgroup.map_subtype_lt_map_subtype]

Premises used: MonoidHom.range_eq_map, Subgroup.map_subtype_lt_map_subtype, Subgroup.range_subtype, Subgroup.map_commutator
-- 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 : Finite G
inst_4 : IsZGroup G
H : Subgroup G
h : Nontrivial.{u_1} ↥H
⊢ LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤

Tactic:
commutator_lt H

Premises used: Membership.mem, Subtype, IsZGroup.commutator_lt
-- 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 : Finite G
inst_4 : IsZGroup G
H : Subgroup G
h : Nontrivial.{u_1} ↥H
⊢ LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤

Tactic:
exact commutator_lt H

Premises used: Membership.mem, Subtype, IsZGroup.commutator_lt
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
⊢ Monoid.exponent G = Nat.card G

Tactic:
dvd_antisymm Group.exponent_dvd_nat_card ?_

Premises used: dvd_antisymm, Group.exponent_dvd_nat_card
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
refine : Nat.card G ∣ Monoid.exponent G
⊢ Monoid.exponent G = Nat.card G

Tactic:
refine dvd_antisymm Group.exponent_dvd_nat_card ?_

Premises used: dvd_antisymm, Group.exponent_dvd_nat_card
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
rw :
  ∀ (p : ℕ),
    Nat.Prime p →
      LE.le (α := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
        (((Monoid.exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Nat.card G ∣ Monoid.exponent G

Tactic:
rw [← Nat.factorization_prime_le_iff_dvd Nat.card_pos.ne' Monoid.exponent_ne_zero_of_finite]

Premises used: Nat.card_pos, LT.lt.ne', Nat.factorization_prime_le_iff_dvd, Monoid.exponent_ne_zero_of_finite
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ Fact (Nat.Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
rw : Monoid.exponent.{u_1} ↥(↑P : Subgroup G) ∣ Monoid.exponent G
⊢ LE.le (α := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
    (((Monoid.exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [← hp.pow_dvd_iff_le_factorization Monoid.exponent_ne_zero_of_finite,
      ← P.card_eq_multiplicity, ← (isZGroup p hp P).exponent_eq_card]

Premises used: Sylow.card_eq_multiplicity, IsCyclic.exponent_eq_card, Monoid.exponent_ne_zero_of_finite, Nat.Prime.pow_dvd_iff_le_factorization
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ Monoid.exponent.{u_1} ↥(↑P : Subgroup G) ∣ Monoid.exponent G

Tactic:
Monoid.exponent_dvd_of_monoidHom P.1.subtype P.1.subtype_injective

Premises used: Sylow.toSubgroup, Subgroup.subtype, Subgroup.subtype_injective, Monoid.exponent_dvd_of_monoidHom
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ Monoid.exponent.{u_1} ↥(↑P : Subgroup G) ∣ Monoid.exponent G

Tactic:
exact Monoid.exponent_dvd_of_monoidHom P.1.subtype P.1.subtype_injective

Premises used: Sylow.toSubgroup, Subgroup.subtype, Subgroup.subtype_injective, Monoid.exponent_dvd_of_monoidHom
-- 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 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
⊢ ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))

Tactic:
have (p : { x // x ∈ (Nat.card G).primeFactors }) : Fact p.1.Prime :=
    ⟨Nat.prime_of_mem_primeFactors p.2⟩
-- 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 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
obtain : ∀ (ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G), IsCyclic G
⊢ IsCyclic G

Tactic:
obtain ⟨ϕ⟩ := ((Group.isNilpotent_of_finite_tfae (G := G)).out 0 4).mp hG

Premises used: Group.isNilpotent_of_finite_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- 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 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
g h : G
rw :
  Eq (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (g * h) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
rw₁ :
  HMul.hMul (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (β :=
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) g :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) h :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) =
    (ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g)
rw₂ :
  HMul.hMul (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (β :=
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) h :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) g :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) =
    (ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g)
rw₃ rw₄ :
  Eq (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
⊢ g * h = h * g

Tactic:
rw [← ϕ.symm.injective.eq_iff, map_mul, mul_comm, ← map_mul]

Premises used: Function.Injective.eq_iff, map_mul, mul_comm, MulEquiv.symm, MulEquiv.injective
-- 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 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
x : CommGroup G := { toGroup := inst, mul_comm := ⋯ }
⊢ IsCyclic G

Tactic:
IsCyclic.of_exponent_eq_card (exponent_eq_card G)

Premises used: IsCyclic.of_exponent_eq_card, IsZGroup.exponent_eq_card
-- 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 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
x : CommGroup G := { toGroup := inst, mul_comm := ⋯ }
⊢ IsCyclic G

Tactic:
exact IsCyclic.of_exponent_eq_card (exponent_eq_card G)

Premises used: IsCyclic.of_exponent_eq_card, IsZGroup.exponent_eq_card
-- 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 : Finite G
inst_4 : IsZGroup G
⊢ IsCyclic.{u_1} (Abelianization G)

Tactic:
let _ : IsZGroup (Abelianization G) := inferInstanceAs (IsZGroup (G ⧸ commutator G))
  inferInstance

Premises used: inferInstance, _private.0.IsZGroup.isCyclic_abelianization._proof_1
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
ind : ∀ (H : Subgroup G) (hH : ∀ y < H, IsCyclic.{u_1} ↥⁅y, y⁆), IsCyclic.{u_1} ↥⁅H, H⁆
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup G) ⊤ ⊤)

Tactic:
induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH

Premises used: WellFoundedLT.induction, Top.top
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic.{u_1} ↥⁅y, y⁆
ind : ∀ (hH : ∀ y < ⊥, IsCyclic.{u_1} ↥⁅y, y⁆), IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup G) ⊥ ⊥)
ind₁ : ∀ (h : H ≠ ⊥), IsCyclic.{u_1} ↥⁅H, H⁆
⊢ IsCyclic.{u_1} ↥⁅H, H⁆

Tactic:
rcases eq_or_ne H ⊥ with rfl | h

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
hH : ∀ y < ⊥, IsCyclic.{u_1} ↥⁅y, y⁆
ind : IsCyclic.{u_1} ↥⊥
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup G) ⊥ ⊥)

Tactic:
rw [Subgroup.commutator_bot_left]

Premises used: Subgroup.commutator_bot_left
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
hH : ∀ y < ⊥, IsCyclic.{u_1} ↥⁅y, y⁆
⊢ IsCyclic.{u_1} ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic.{u_1} ↥⁅y, y⁆
h : H ≠ ⊥
⊢ IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆

Tactic:
specialize hH ⁅H, H⁆ (IsSolvable.commutator_lt_of_ne_bot h)

Premises used: IsSolvable.commutator_lt_of_ne_bot, Bracket.bracket
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
f : ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) ≃*
  ↥(Subgroup.map H.subtype (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))) :=
  Subgroup.equivMapOfInjective (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) H.subtype ⋯
rw :
  ∀ (f : ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) ≃* ↥⁅⁅H, H⁆, ⁅H, H⁆⁆),
    IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))

Tactic:
rw [Subgroup.map_commutator, Subgroup.map_subtype_commutator] at f

Premises used: Subgroup.map_commutator, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
f : ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) ≃* ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))

Tactic:
isCyclic_of_surjective f.symm f.symm.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective, MulEquiv.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
f : ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) ≃* ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))

Tactic:
exact isCyclic_of_surjective f.symm f.symm.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective, MulEquiv.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))

Tactic:
replace hH : IsCyclic (⁅commutator H, commutator H⁆ : Subgroup H) := by
      let f := Subgroup.equivMapOfInjective ⁅commutator H, commutator H⁆ _ H.subtype_injective
      rw [Subgroup.map_commutator, Subgroup.map_subtype_commutator] at f
      exact isCyclic_of_surjective f.symm f.symm.surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
this : IsCyclic.{u_1} ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥(Subgroup.map H.subtype (commutator ↥H)) :=
  Subgroup.equivMapOfInjective (commutator ↥H) H.subtype ⋯
rw : ∀ (f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆), IsCyclic.{u_1} ↥⁅H, H⁆
⊢ IsCyclic.{u_1} ↥⁅H, H⁆

Tactic:
rw [Subgroup.map_subtype_commutator] at f

Premises used: Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
this : IsCyclic.{u_1} ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆
⊢ IsCyclic.{u_1} ↥⁅H, H⁆

Tactic:
isCyclic_of_surjective f f.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
this : IsCyclic.{u_1} ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆
⊢ IsCyclic.{u_1} ↥⁅H, H⁆

Tactic:
exact isCyclic_of_surjective f f.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
ind : IsCyclic.{u_1} ↥(commutator ↥H)
⊢ IsCyclic.{u_1} ↥⁅H, H⁆

Tactic:
suffices IsCyclic (commutator H) by
      let f := Subgroup.equivMapOfInjective (commutator H) _ H.subtype_injective
      rw [Subgroup.map_subtype_commutator] at f
      exact isCyclic_of_surjective f f.surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h_1 : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
h : LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (commutator ↥(commutator ↥H)) (Subgroup.center ↥(commutator ↥H))
⊢ LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (MonoidHom.ker Abelianization.of) (Subgroup.center ↥(commutator ↥H))

Tactic:
rw [← Abelianization.ker_of (commutator H)] at h

Premises used: Membership.mem, Subtype, commutator, Abelianization.ker_of
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h_1 : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
h : LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (MonoidHom.ker Abelianization.of) (Subgroup.center ↥(commutator ↥H))
x : CommGroup ↥(commutator ↥H) := commGroupOfCyclicCenterQuotient Abelianization.of h
⊢ IsCyclic.{u_1} ↥(commutator ↥H)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
ind : LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (commutator ↥(commutator ↥H)) (Subgroup.center ↥(commutator ↥H))
⊢ IsCyclic.{u_1} ↥(commutator ↥H)

Tactic:
suffices h : commutator (commutator H) ≤ Subgroup.center (commutator H) by
      rw [← Abelianization.ker_of (commutator H)] at h
      let _ := commGroupOfCyclicCenterQuotient Abelianization.of h
      infer_instance