awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
u v : ZMod (Nat.card G)
hvu : v * (↑u.cast : ZMod (Nat.card G)) = 1
hu :
  (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
⊢ HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(Nat.card G) : ℤ)]

Tactic:
rw [← v.intCast_zmod_cast, ← Int.cast_mul, ← Int.cast_one, ZMod.intCast_eq_intCast_iff] at hvu

Premises used: ZMod.intCast_eq_intCast_iff, Int.cast_mul, ZMod.intCast_zmod_cast, Int.cast_one
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
u v : ZMod (Nat.card G)
hvu : v * (↑u.cast : ZMod (Nat.card G)) = 1
hu :
  (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
hvu₁ : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(Nat.card G) : ℤ)]
⊢ (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))

Tactic:
rw [← v.intCast_zmod_cast, ← Int.cast_mul, ← Int.cast_one, ZMod.intCast_eq_intCast_iff] at hvu

Premises used: ZMod.intCast_eq_intCast_iff, Int.cast_mul, ZMod.intCast_zmod_cast, Int.cast_one
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
u v : ZMod (Nat.card G)
hvu : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(Nat.card G) : ℤ)]
hu :
  (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g

Tactic:
Or.inr fun p ↦ zpow_one p ▸ ⟨k, p ^ (v.cast : ℤ), ?_⟩

Premises used: ZMod.cast, Eq.rec, zpow_one, HPow.hPow, Exists.intro, Or.inr
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
u v : ZMod (Nat.card G)
hvu : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(Nat.card G) : ℤ)]
hu :
  (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
neg : ∀ (p : G), k • HPow.hPow (β := ℤ) p v.cast * (HPow.hPow (β := ℤ) p v.cast)⁻¹ = HPow.hPow (β := ℤ) p 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g

Tactic:
refine Or.inr fun p ↦ zpow_one p ▸ ⟨k, p ^ (v.cast : ℤ), ?_⟩

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
u v : ZMod (Nat.card G)
hvu : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(Nat.card G) : ℤ)]
hu :
  (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
neg : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(orderOf p) : ℤ)]
⊢ k • HPow.hPow (β := ℤ) p v.cast * (HPow.hPow (β := ℤ) p v.cast)⁻¹ = HPow.hPow (β := ℤ) p 1

Tactic:
rw [h (p ^ v.cast) k u.cast hu.symm, ← zpow_mul, zpow_eq_zpow_iff_modEq]

Premises used: ZMod.cast, zpow_mul, HPow.hPow, zpow_eq_zpow_iff_modEq, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
u v : ZMod (Nat.card G)
hvu : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(Nat.card G) : ℤ)]
hu :
  (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
⊢ HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(orderOf p) : ℤ)]

Tactic:
hvu.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard p))

Premises used: Iff.mpr, orderOf_dvd_natCard, Int.ModEq.of_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p_1 : ℕ
inst_1 : Fact (Nat.Prime p_1)
inst_2 : IsCyclic G
K : Type u_4
inst_3 : Group K
inst_4 : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h :
  ∀ (g : G) (k : K) (n : ℤ)
    (h :
      HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) =
        (↑n : ZMod (Nat.card G))),
    k • g * g⁻¹ = g ^ n
hG :
  ∀ (k : K),
    Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)) ∨
      IsUnit
        (HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
          ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G)))
k : K
hk : ¬Eq (α := ZMod (Nat.card G)) ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
u v : ZMod (Nat.card G)
hvu : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(Nat.card G) : ℤ)]
hu :
  (↑u.cast : ZMod (Nat.card G)) =
    HSub.hSub (α := ZMod (Nat.card G)) (β := ZMod (Nat.card G))
      ((ϕ : (a : K) → ZMod (Nat.card G)) k : ZMod (Nat.card G)) (1 : ZMod (Nat.card G))
p : G
⊢ HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(orderOf p) : ℤ)]

Tactic:
exact hvu.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard p))

Premises used: Iff.mpr, orderOf_dvd_natCard, Int.ModEq.of_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
⊢ ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P

Tactic:
(smul_mul_inv_trivial_or_surjective hP hPK).imp (fun h ↦ ?_) fun h ↦ ?_

Premises used: IsPGroup.smul_mul_inv_trivial_or_surjective, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
refine_1 : ∀ (h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1), ⁅K, P⁆ = ⊥
refine_2 : ∀ (h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g), ⁅K, P⁆ = P
⊢ ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P

Tactic:
refine (smul_mul_inv_trivial_or_surjective hP hPK).imp (fun h ↦ ?_) fun h ↦ ?_

Premises used: IsPGroup.smul_mul_inv_trivial_or_surjective, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
refine_1 : ∀ g₁ ∈ K, ∀ g₂ ∈ P, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆
⊢ ⁅K, P⁆ = ⊥

Tactic:
rw [eq_bot_iff, Subgroup.commutator_le]

Premises used: Subgroup.commutator_le, eq_bot_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ∀ g₁ ∈ K, ∀ g₂ ∈ P, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆

Tactic:
fun k hk g hg ↦ Subtype.ext_iff.mp (h ⟨g, hg⟩ ⟨k, hk⟩)

Premises used: Set.Mem, setOf, Subtype.ext_iff, Subtype.mk, Set.singleton, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ∀ g₁ ∈ K, ∀ g₂ ∈ P, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆

Tactic:
exact fun k hk g hg ↦ Subtype.ext_iff.mp (h ⟨g, hg⟩ ⟨k, hk⟩)

Premises used: Subtype.ext_iff, Subtype.mk, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g
refine_2 : (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆
⊢ ⁅K, P⁆ = P

Tactic:
rw [le_antisymm_iff, Subgroup.commutator_le]

Premises used: Subgroup.commutator_le, le_antisymm_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g
⊢ (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆

Tactic:
⟨fun k hk g hg ↦ P.mul_mem ((hKP hk g).mp hg) (P.inv_mem hg), fun g hg ↦ ?_⟩

Premises used: Subgroup.inv_mem, And.intro, Iff.mp, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g
refine_2 : ∀ (g : G) (hg : g ∈ P), g ∈ ⁅K, P⁆
⊢ (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆

Tactic:
refine ⟨fun k hk g hg ↦ P.mul_mem ((hKP hk g).mp hg) (P.inv_mem hg), fun g hg ↦ ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g
g : G
hg : g ∈ P
refine_2 : ∀ (k : ↥K) (q : ↥P) (hkq : k • q * q⁻¹ = Subtype.mk (p := fun (x : G) ↦ x ∈ P) g hg), g ∈ ⁅K, P⁆
⊢ g ∈ ⁅K, P⁆

Tactic:
obtain ⟨k, q, hkq⟩ := h ⟨g, hg⟩

Premises used: Subtype.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g
g : G
hg : g ∈ P
k : ↥K
q : ↥P
hkq : k • q * q⁻¹ = Subtype.mk (p := fun (x : G) ↦ x ∈ P) g hg
refine_2 : (↑(k • q * q⁻¹) : G) ∈ ⁅K, P⁆
⊢ g ∈ ⁅K, P⁆

Tactic:
rw [← Subtype.coe_mk g hg, ← hkq]

Premises used: Subtype.coe_mk
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g
g : G
hg : g ∈ P
k : ↥K
q : ↥P
hkq : k • q * q⁻¹ = Subtype.mk (p := fun (x : G) ↦ x ∈ P) g hg
⊢ (↑(k • q * q⁻¹) : G) ∈ ⁅K, P⁆

Tactic:
Subgroup.commutator_mem_commutator k.2 q.2

Premises used: Set.Mem, Subgroup.commutator_mem_commutator, Subtype.property
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P K : Subgroup G
inst_2 : IsCyclic.{u_1} ↥P
hP : IsPGroup.{u_1} p ↥P
hKP : K ≤ Subgroup.normalizer (↑P : Set G)
hPK : (Nat.card.{u_1} ↥P).Coprime (Nat.card.{u_1} ↥K)
x : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g
g : G
hg : g ∈ P
k : ↥K
q : ↥P
hkq : k • q * q⁻¹ = Subtype.mk (p := fun (x : G) ↦ x ∈ P) g hg
⊢ (↑(k • q * q⁻¹) : G) ∈ ⁅K, P⁆

Tactic:
exact Subgroup.commutator_mem_commutator k.2 q.2

Premises used: Subgroup.commutator_mem_commutator, Subtype.property
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
h : K.IsComplement' (↑P : Subgroup G)
⊢ ⁅K, (↑P : Subgroup G)⁆ = ⊥ ∨ ⁅K, (↑P : Subgroup G)⁆ = (↑P : Subgroup G)

Tactic:
P.2.commutator_eq_bot_or_commutator_eq_self (P.normalizer_eq_top ▸ le_top)
    (h.index_eq_card ▸ P.card_coprime_index)

Premises used: Sylow.isPGroup', Sylow.toSubgroup, Subgroup.IsComplement'.index_eq_card, Eq.rec, Subgroup.normalizer_eq_top, IsPGroup.commutator_eq_bot_or_commutator_eq_self, le_top, Eq.symm, Sylow.card_coprime_index
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
obtain :
  ∀ (K : Subgroup G) (hK : K.IsComplement' (↑P : Subgroup G)),
    (↑P : Subgroup G) ≤ Subgroup.center G ∨ (↑P : Subgroup G) ≤ commutator G
⊢ (↑P : Subgroup G) ≤ Subgroup.center G ∨ (↑P : Subgroup G) ≤ commutator G

Tactic:
obtain ⟨K, hK⟩ := Subgroup.exists_left_complement'_of_coprime P.card_coprime_index

Premises used: Subgroup.exists_left_complement'_of_coprime, Sylow.card_coprime_index
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
hK : K.IsComplement' (↑P : Subgroup G)
⊢ (↑P : Subgroup G) ≤ Subgroup.center G ∨ (↑P : Subgroup G) ≤ commutator G

Tactic:
(commutator_eq_bot_or_commutator_eq_self P hK).imp (fun h ↦ ?_) (fun h ↦ ?_)

Premises used: Sylow.commutator_eq_bot_or_commutator_eq_self, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
hK : K.IsComplement' (↑P : Subgroup G)
refine_1 : ∀ (h : ⁅K, (↑P : Subgroup G)⁆ = ⊥), (↑P : Subgroup G) ≤ Subgroup.center G
refine_2 : ∀ (h : ⁅K, (↑P : Subgroup G)⁆ = (↑P : Subgroup G)), (↑P : Subgroup G) ≤ commutator G
⊢ (↑P : Subgroup G) ≤ Subgroup.center G ∨ (↑P : Subgroup G) ≤ commutator G

Tactic:
refine (commutator_eq_bot_or_commutator_eq_self P hK).imp (fun h ↦ ?_) (fun h ↦ ?_)

Premises used: Sylow.commutator_eq_bot_or_commutator_eq_self, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
hK : K.IsComplement' (↑P : Subgroup G)
h : ⁅K, (↑P : Subgroup G)⁆ = ⊥
⊢ K ⊔ (↑P : Subgroup G) ≤ Subgroup.centralizer (↑(↑P : Subgroup G) : Set G)

Tactic:
replace h := sup_le (Subgroup.commutator_eq_bot_iff_le_centralizer.mp h) P.le_centralizer
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
hK : K.IsComplement' (↑P : Subgroup G)
h : K ⊔ (↑P : Subgroup G) ≤ Subgroup.centralizer (↑(↑P : Subgroup G) : Set G)
refine_1 :
  ∀ (h : LE.le (α := Subgroup G) ⊤ (Subgroup.centralizer (↑(↑P : Subgroup G) : Set G))),
    (↑P : Subgroup G) ≤ Subgroup.center G
refine_1₁ :
  ∀ (h : Eq (α := Subgroup G) (Subgroup.centralizer (↑(↑P : Subgroup G) : Set G)) ⊤),
    (↑P : Subgroup G) ≤ Subgroup.center G
refine_1₂ refine_1₃ refine_1₄ refine_1₅ :
  ∀ (h : (↑(↑P : Subgroup G) : Set G) ⊆ (↑(Subgroup.center G) : Set G)), (↑P : Subgroup G) ≤ Subgroup.center G
⊢ (↑P : Subgroup G) ≤ Subgroup.center G

Tactic:
rwa [hK.sup_eq_top, top_le_iff, Subgroup.centralizer_eq_top_iff_subset] at h

Premises used: Subgroup.centralizer_eq_top_iff_subset, top_le_iff, Subgroup.IsComplement'.sup_eq_top
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
hK : K.IsComplement' (↑P : Subgroup G)
h : ⁅K, (↑P : Subgroup G)⁆ = (↑P : Subgroup G)
refine_2 : ⁅K, (↑P : Subgroup G)⁆ ≤ Bracket.bracket (L := Subgroup G) ⊤ ⊤
⊢ (↑P : Subgroup G) ≤ commutator G

Tactic:
rw [← h, commutator_def]

Premises used: commutator_def
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
hK : K.IsComplement' (↑P : Subgroup G)
h : ⁅K, (↑P : Subgroup G)⁆ = (↑P : Subgroup G)
⊢ ⁅K, (↑P : Subgroup G)⁆ ≤ Bracket.bracket (L := Subgroup G) ⊤ ⊤

Tactic:
Subgroup.commutator_mono le_top le_top

Premises used: Subgroup.commutator_mono, le_top