awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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 = 1
hu :
  u =
    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
have hvu₁ : v * (↑u.cast : ZMod (Nat.card G)) = 1
Tactic: rw [← u.intCast_zmod_cast] at hu hvu
Cleared hypotheses: hvu, hu
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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 = 1
hu :
  u =
    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₁ : v * (↑u.cast : ZMod (Nat.card G)) = 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have 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))
Tactic: rw [← u.intCast_zmod_cast] at hu hvu
Cleared hypotheses: hvu, hu
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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))
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ (k : K) (q : G), k • q * q⁻¹ = g
have hvu₁ : 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
Cleared hypotheses: hvu, hu
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
have neg : ∀ (p : G), k • HPow.hPow (β := ℤ) p v.cast * (HPow.hPow (β := ℤ) p v.cast)⁻¹ = HPow.hPow (β := ℤ) p 1
Tactic: refine Or.inr fun p ↦ zpow_one p ▸ ⟨k, p ^ (v.cast : ℤ), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ k • HPow.hPow (β := ℤ) p v.cast * (HPow.hPow (β := ℤ) p v.cast)⁻¹ = HPow.hPow (β := ℤ) p 1
have neg : HMul.hMul (α := ℤ) v.cast u.cast ≡ 1 [ZMOD (↑(orderOf p) : ℤ)]
Tactic: rw [h (p ^ v.cast) k u.cast hu.symm, ← zpow_mul, zpow_eq_zpow_iff_modEq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
have refine_1 : ∀ (h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1), ⁅K, P⁆ = ⊥
Tactic: refine (smul_mul_inv_trivial_or_surjective hP hPK).imp (fun h ↦ ?_) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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⁆ = ⊥
⊢ ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P
have refine_2 : ∀ (h : ∀ (g : ↥P), ∃ (k : ↥K) (q : ↥P), k • q * q⁻¹ = g), ⁅K, P⁆ = P
Tactic: refine (smul_mul_inv_trivial_or_surjective hP hPK).imp (fun h ↦ ?_) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ ⁅K, P⁆ = ⊥
have refine_1 : ∀ g₁ ∈ K, ∀ g₂ ∈ P, Membership.mem (γ := Subgroup G) ⊥ ⁅g₁, g₂⁆
Tactic: rw [eq_bot_iff, Subgroup.commutator_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ ⁅K, P⁆ = P
have refine_2 : (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆
Tactic: rw [le_antisymm_iff, Subgroup.commutator_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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⁆
have refine_2 : ∀ (g : G) (hg : g ∈ P), g ∈ ⁅K, P⁆
Tactic: refine ⟨fun k hk g hg ↦ P.mul_mem ((hKP hk g).mp hg) (P.inv_mem hg), fun g hg ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ g ∈ ⁅K, P⁆
have refine_2 : ∀ (k : ↥K) (q : ↥P) (hkq : k • q * q⁻¹ = Subtype.mk (p := fun (x : G) ↦ x ∈ P) g hg), g ∈ ⁅K, P⁆
Tactic: obtain ⟨k, q, hkq⟩ := h ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ g ∈ ⁅K, P⁆
have refine_2 : (↑(k • q * q⁻¹) : G) ∈ ⁅K, P⁆
Tactic: rw [← Subtype.coe_mk g hg, ← hkq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ (↑P : Subgroup G) ≤ Subgroup.center G ∨ (↑P : Subgroup G) ≤ commutator G
have obtain : ∀ (K : Subgroup G) (hK : K.IsComplement' (↑P : Subgroup 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
have refine_1 : ∀ (h : ⁅K, (↑P : Subgroup G)⁆ = ⊥), (↑P : Subgroup G) ≤ Subgroup.center G
Tactic: refine (commutator_eq_bot_or_commutator_eq_self P hK).imp (fun h ↦ ?_) (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ (↑P : Subgroup G) ≤ Subgroup.center G ∨ (↑P : Subgroup G) ≤ commutator G
have refine_2 : ∀ (h : ⁅K, (↑P : Subgroup G)⁆ = (↑P : Subgroup G)), (↑P : Subgroup G) ≤ commutator G
Tactic: refine (commutator_eq_bot_or_commutator_eq_self P hK).imp (fun h ↦ ?_) (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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) ≤ Subgroup.center G
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
⊢ (↑P : Subgroup G) ≤ Subgroup.center G
have refine_1 : ∀ (h : LE.le (α := Subgroup G) ⊤ (Subgroup.centralizer (↑(↑P : Subgroup G) : Set G))),
  (↑P : Subgroup G) ≤ Subgroup.center G
Tactic: rwa [hK.sup_eq_top, top_le_iff, Subgroup.centralizer_eq_top_iff_subset] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ (↑P : Subgroup G) ≤ Subgroup.center G
have refine_1₁ : ∀ (h : Eq (α := Subgroup G) (Subgroup.centralizer (↑(↑P : Subgroup G) : Set G)) ⊤),
  (↑P : Subgroup G) ≤ Subgroup.center G
Tactic: rwa [hK.sup_eq_top, top_le_iff, Subgroup.centralizer_eq_top_iff_subset] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ (↑P : Subgroup G) ≤ Subgroup.center G
have refine_1₂ : ∀ (h : (↑(↑P : Subgroup G) : Set G) ⊆ (↑(Subgroup.center G) : Set G)), (↑P : Subgroup G) ≤ Subgroup.center G
Tactic: rwa [hK.sup_eq_top, top_le_iff, Subgroup.centralizer_eq_top_iff_subset] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
⊢ (↑P : Subgroup G) ≤ commutator G
have refine_2 : ⁅K, (↑P : Subgroup G)⁆ ≤ Bracket.bracket (L := Subgroup G) ⊤ ⊤
Tactic: rw [← h, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) ∨
    (↑P : Subgroup G) ≤ commutator G
have this : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
Tactic: have : Q.Normal := P.normal_in_normalizer
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) ∨
    (↑P : Subgroup G) ≤ commutator G
have this₁ : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
Tactic: have : IsCyclic Q :=
    isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe P.le_normalizer).symm.surjective
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) ∨
    (↑P : Subgroup G) ≤ commutator G
have refine_1 : ∀ (h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ Subgroup.center ↥(Subgroup.normalizer (↑P : Set G))),
  LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
Tactic: refine (le_center_or_le_commutator Q).imp (fun h ↦ ?_) (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
refine_1 :
  ∀ (h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ Subgroup.center ↥(Subgroup.normalizer (↑P : Set G))),
    LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) ∨
    (↑P : Subgroup G) ≤ commutator G
have refine_2 : ∀ (h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ commutator ↥(Subgroup.normalizer (↑P : Set G))),
  (↑P : Subgroup G) ≤ commutator G
Tactic: refine (le_center_or_le_commutator Q).imp (fun h ↦ ?_) (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ Subgroup.center ↥(Subgroup.normalizer (↑P : Set G))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
have h₁ : Subgroup.normalizer (↑P : Set G) ≤
  Subgroup.map (Subgroup.subtype (Subgroup.normalizer (↑P : Set G)))
    (Subgroup.centralizer
      (↑(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) : Set ↥(Subgroup.normalizer (↑P : Set G))))
Tactic: rw [← SetLike.coe_subset_coe, ← Subgroup.centralizer_eq_top_iff_subset, eq_top_iff,
      ← Subgroup.map_subtype_le_map_subtype, ← MonoidHom.range_eq_map,
      (Subgroup.normalizer (P : Set G)).range_subtype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h :
  Subgroup.normalizer (↑P : Set G) ≤
    Subgroup.map (Subgroup.subtype (Subgroup.normalizer (↑P : Set G)))
      (Subgroup.centralizer
        (↑(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) : Set ↥(Subgroup.normalizer (↑P : Set G))))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
have h₁ : LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G))
  (Subgroup.centralizer
    ((⇑(Subgroup.subtype (Subgroup.normalizer (↑P : Set G))) : (a : ↥(Subgroup.normalizer (↑P : Set G))) → G) ''
      (↑(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) : Set ↥(Subgroup.normalizer (↑P : Set G)))))
Tactic: replace h := h.trans (Subgroup.map_centralizer_le_centralizer_image _ _)
Cleared hypotheses: h