awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card.{u} ↥H' = p ^ m
⊢ Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'

Tactic:
simpa only [pow_succ', H'card] using And.intro hmk hkm

Premises used: And.intro, pow_succ'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ Nat.card G
⊢ p ^ n ∣ (↑P : Subgroup G).index * Nat.card.{u} ↥(↑P : Subgroup G)

Tactic:
rw [← index_mul_card P.1] at hdvd

Premises used: Sylow.toSubgroup, Subgroup.index_mul_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ (↑P : Subgroup G).index * Nat.card.{u} ↥(↑P : Subgroup G)
⊢ p ^ n ∣ Nat.card.{u} ↥(↑P : Subgroup G)

Tactic:
(hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm.dvd_of_dvd_mul_left hdvd

Premises used: Nat.Coprime.symm, Sylow.not_dvd_index, Nat.Coprime.dvd_of_dvd_mul_left, Fact.out, Nat.Prime.coprime_pow_of_not_dvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ (↑P : Subgroup G).index * Nat.card.{u} ↥(↑P : Subgroup G)
⊢ p ^ n ∣ Nat.card.{u} ↥(↑P : Subgroup G)

Tactic:
exact (hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm.dvd_of_dvd_mul_left hdvd

Premises used: Nat.Coprime.symm, Sylow.not_dvd_index, Nat.Coprime.dvd_of_dvd_mul_left, Fact.out, Nat.Prime.coprime_pow_of_not_dvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ HPow.hPow (β := ℕ) p 1 ∣ Nat.card G

Tactic:
rw [← pow_one p] at hdvd

Premises used: pow_one
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Sylow p G
hdvd : HPow.hPow (β := ℕ) p 1 ∣ Nat.card G
⊢ HPow.hPow (β := ℕ) p 1 ∣ Nat.card.{u} ↥(↑P : Subgroup G)

Tactic:
have key := P.pow_dvd_card_of_pow_dvd_card hdvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Sylow p G
hdvd : HPow.hPow (β := ℕ) p 1 ∣ Nat.card G
key : HPow.hPow (β := ℕ) p 1 ∣ Nat.card.{u} ↥(↑P : Subgroup G)
rwa rwa₁ rwa₂ rwa₃ : ∀ (key : p ∣ Nat.card.{u} ↥(↑P : Subgroup G)), p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
⊢ p ∣ Nat.card.{u} ↥(↑P : Subgroup G)

Tactic:
rwa [pow_one] at key

Premises used: pow_one
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
⊢ (Nat.card.{u} ↥(↑P : Subgroup G)).Coprime (↑P : Subgroup G).index

Tactic:
let ⟨_n, hn⟩ := IsPGroup.iff_card.mp P.2
  hn.symm ▸ (hp.1.coprime_pow_of_not_dvd P.not_dvd_index).symm

Premises used: Sylow.isPGroup', Sylow.toSubgroup, Nat.Coprime, Nat.Coprime.symm, IsPGroup.iff_card, Sylow.not_dvd_index, Membership.mem, Eq.rec, Subtype, Nat.card, _private.0.Sylow.card_coprime_index.match_1, Subgroup.index, Iff.mp, Eq.symm, Fact.out, Nat.Prime.coprime_pow_of_not_dvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ (↑P : Subgroup G) ≠ ⊥

Tactic:
fun h => hp.out.not_dvd_one ?_

Premises used: Nat.Prime.not_dvd_one, Not, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
refine : ∀ (h : (↑P : Subgroup G) = ⊥), p ∣ 1
⊢ (↑P : Subgroup G) ≠ ⊥

Tactic:
refine fun h => hp.out.not_dvd_one ?_

Premises used: Nat.Prime.not_dvd_one, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : (↑P : Subgroup G) = ⊥
⊢ p ∣ Nat.card.{u} ↥(↑P : Subgroup G)

Tactic:
have key : p ∣ Nat.card P := P.dvd_card_of_dvd_card hdvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : (↑P : Subgroup G) = ⊥
key : p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
rwa : ∀ (key : p ∣ Nat.card.{u} ↥⊥), p ∣ 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (key : p ∣ 1), p ∣ 1
⊢ p ∣ 1

Tactic:
rwa [h, card_bot] at key

Premises used: Subgroup.card_bot
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
obtain :
  ∀ (n : ℕ) (heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n),
    Nat.card.{u} ↥(↑P : Subgroup G) = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Nat.card.{u} ↥(↑P : Subgroup G) = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
obtain ⟨n, heq : Nat.card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'

Premises used: Sylow.isPGroup', Sylow.toSubgroup, IsPGroup.iff_card, Membership.mem, Subtype, Nat.card, Iff.mp
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n
⊢ Nat.card.{u} ↥(↑P : Subgroup G) = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
Nat.dvd_antisymm ?_ (P.pow_dvd_card_of_pow_dvd_card (Nat.ordProj_dvd _ p))

Premises used: Nat.ordProj_dvd, Sylow.pow_dvd_card_of_pow_dvd_card, Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n
refine : Nat.card.{u} ↥(↑P : Subgroup G) ∣ HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Nat.card.{u} ↥(↑P : Subgroup G) = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
refine Nat.dvd_antisymm ?_ (P.pow_dvd_card_of_pow_dvd_card (Nat.ordProj_dvd _ p))

Premises used: Nat.ordProj_dvd, Sylow.pow_dvd_card_of_pow_dvd_card, Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n
rw : Nat.card.{u} ↥(↑P : Subgroup G) ∣ Nat.card G
⊢ Nat.card.{u} ↥(↑P : Subgroup G) ∣ HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [heq, ← hp.out.pow_dvd_iff_dvd_ordProj (show Nat.card G ≠ 0 from Nat.card_pos.ne'), ← heq]

Premises used: Nat.card_pos, LT.lt.ne', Nat.Prime.pow_dvd_iff_dvd_ordProj, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n
⊢ Nat.card.{u} ↥(↑P : Subgroup G) ∣ Nat.card G

Tactic:
P.1.card_subgroup_dvd_card

Premises used: Sylow.toSubgroup, Subgroup.card_subgroup_dvd_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n
⊢ Nat.card.{u} ↥(↑P : Subgroup G) ∣ Nat.card G

Tactic:
exact P.1.card_subgroup_dvd_card

Premises used: Sylow.toSubgroup, Subgroup.card_subgroup_dvd_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
refine : ∀ (Q : Sylow p G), Q = default
⊢ Unique (Sylow p G)

Tactic:
refine { uniq := fun Q ↦ ?_ }
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
obtain : ∀ (x : G) (h1 : x • P = Q), Q = default
⊢ Q = default

Tactic:
obtain ⟨x, h1⟩ := exists_smul_eq G P Q

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
x : G
h1 : x • P = Q
obtain : ∀ (x : G) (h2 : x • P = default), Q = default
⊢ Q = default

Tactic:
obtain ⟨x, h2⟩ := exists_smul_eq G P default

Premises used: Inhabited.default, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
x_1 : G
h1 : x_1 • P = Q
x : G
h2 : x • P = default
rw : ∀ (h1 : P = Q) (x : G) (h2 : P = default), Q = default
⊢ Q = default

Tactic:
rw [smul_eq_of_normal] at h1 h2

Premises used: Sylow.smul_eq_of_normal
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
x_1 : G
h1 : P = Q
x : G
h2 rw : P = default
rw₁ rw₂ : P = P
⊢ Q = default

Tactic:
rw [← h1, ← h2]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
⊢ (↑P : Subgroup G).Characteristic

Tactic:
Subgroup.characteristic_iff_map_eq.mpr fun ϕ ↦ ?_

Premises used: Iff.mpr, Subgroup.characteristic_iff_map_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
refine : ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
⊢ (↑P : Subgroup G).Characteristic

Tactic:
refine Subgroup.characteristic_iff_map_eq.mpr fun ϕ ↦ ?_

Premises used: Iff.mpr, Subgroup.characteristic_iff_map_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
⊢ ϕ • (↑P : Subgroup G) =
    Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)

Tactic:
have h := Subgroup.pointwise_smul_def (a := ϕ) (P : Subgroup G)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h :
  ϕ • (↑P : Subgroup G) =
    Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)
rwa :
  ∀
    (h :
      (↑(ϕ • P) : Subgroup G) =
        Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)),
    Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
rwa₁ :
  ∀
    (h :
      (↑P : Subgroup G) =
        Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)),
    Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (h :
      Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G) =
        (↑P : Subgroup G)),
    Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
⊢ Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)

Tactic:
rwa [← pointwise_smul_def, Subsingleton.elim (ϕ • P) P, eq_comm] at h

Premises used: Sylow.pointwise_smul_def, eq_comm, HSMul.hSMul, Subsingleton.elim
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
⊢ (↑P : Subgroup G).Normal

Tactic:
Subgroup.normal_of_characteristic _

Premises used: Subgroup.normal_of_characteristic
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
have : ∀ (x : Unique (Sylow p G)), (↑P : Subgroup G).Characteristic
⊢ (↑P : Subgroup G).Characteristic

Tactic:
have _ := unique_of_normal P h
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
x : Unique (Sylow p G)
⊢ (↑P : Subgroup G).Characteristic

Tactic:
characteristic_of_subsingleton _

Premises used: Sylow.characteristic_of_subsingleton
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
x : Unique (Sylow p G)
⊢ (↑P : Subgroup G).Characteristic

Tactic:
exact characteristic_of_subsingleton _

Premises used: Sylow.characteristic_of_subsingleton
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
⊢ ∀
    (hn :
      Normal (normalizer (↑(P.subtype ⋯) : Set ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))))),
    (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))).Normal

Tactic:
have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
this :
  ∀
    (hn :
      Normal (normalizer (↑(P.subtype ⋯) : Set ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))))),
    (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))).Normal
⊢ ∀
    (hn :
      Normal (G := ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))
        (subgroupOf (normalizer (↑(↑P : Subgroup G) : Set G))
          (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))),
    LE.le (α := Subgroup G) (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))
      (normalizer (↑(↑P : Subgroup G) : Set G))

Tactic:
rw [← (P.subtype _).coe_coe, coe_subtype,
    normal_subgroupOf_iff_le_normalizer (le_normalizer.trans le_normalizer),
    ← subgroupOf_normalizer_eq (le_normalizer.trans le_normalizer)] at this

Premises used: Subgroup.subgroupOf_normalizer_eq, Subgroup.le_normalizer, Subgroup.normal_subgroupOf_iff_le_normalizer, Sylow.coe_coe, Sylow.coe_subtype, LE.le.trans, Sylow.subtype
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
this :
  ∀
    (hn :
      Normal (G := ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))
        (subgroupOf (normalizer (↑(↑P : Subgroup G) : Set G))
          (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))),
    LE.le (α := Subgroup G) (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))
      (normalizer (↑(↑P : Subgroup G) : Set G))
⊢ Eq (α := Subgroup G) (normalizer (↑(normalizer (↑P : Set G)) : Set G)) (normalizer (↑P : Set G))

Tactic:
le_antisymm (this normal_in_normalizer) le_normalizer

Premises used: Subgroup.le_normalizer, le_antisymm, Subgroup.normal_in_normalizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
this :
  ∀
    (hn :
      Normal (G := ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))
        (subgroupOf (normalizer (↑(↑P : Subgroup G) : Set G))
          (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))),
    LE.le (α := Subgroup G) (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))
      (normalizer (↑(↑P : Subgroup G) : Set G))
⊢ Eq (α := Subgroup G) (normalizer (↑(normalizer (↑P : Set G)) : Set G)) (normalizer (↑P : Set G))

Tactic:
exact le_antisymm (this normal_in_normalizer) le_normalizer

Premises used: Subgroup.le_normalizer, le_antisymm, Subgroup.normal_in_normalizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
inl :
  ∀ (heq : Eq (α := Subgroup G) (normalizer (↑P : Set G)) ⊤),
    Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
inr :
  ∀ (K : Subgroup G) (hK : IsCoatom K) (hNK : normalizer (↑P : Set G) ≤ K),
    Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤

Tactic:
rcases eq_top_or_exists_le_coatom (normalizer (P : Set G))
        with (heq | ⟨K, hK, hNK⟩)

Premises used: IsCoatomic.eq_top_or_exists_le_coatom, Subgroup.normalizer, SetLike.coe
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
heq : Eq (α := Subgroup G) (normalizer (↑P : Set G)) ⊤
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤

Tactic:
heq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
heq : Eq (α := Subgroup G) (normalizer (↑P : Set G)) ⊤
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤

Tactic:
exact heq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
⊢ K.Normal

Tactic:
haveI := hnc _ hK
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
⊢ (↑P : Subgroup G) ≤ K

Tactic:
have hPK : P ≤ K := le_trans le_normalizer hNK
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
hPK : (↑P : Subgroup G) ≤ K
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤

Tactic:
(hK.1 ?_).elim

Premises used: False.elim, And.left
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
hPK : (↑P : Subgroup G) ≤ K
inr : K = ⊤
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤

Tactic:
refine (hK.1 ?_).elim

Premises used: False.elim, And.left
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
hPK : (↑P : Subgroup G) ≤ K
inr : normalizer (↑P : Set G) ⊔ K = ⊤
inr₁ inr₂ : Eq.{u + 1} (α := Subgroup G) ⊤ ⊤
⊢ K = ⊤

Tactic:
rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]

Premises used: Sylow.normalizer_sup_eq_top', sup_of_le_right
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
hnc : NormalizerCondition G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
⊢ (↑P : Subgroup G).Normal

Tactic:
normalizer_eq_top_iff.mp <|
    normalizerCondition_iff_only_full_group_self_normalizing.mp hnc _ <| normalizer_normalizer _

Premises used: Sylow.normalizer_normalizer, normalizerCondition_iff_only_full_group_self_normalizing, Subgroup.normalizer_eq_top_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
have : (this : Fintype G) → ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
⊢ ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G

Tactic:
have := Fintype.ofFinite G
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this : Fintype G
set :
  let ps := (Nat.card G).primeFactors;
  ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
⊢ ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G

Tactic:
set ps := (Nat.card G).primeFactors

Premises used: Nat.card, Nat.primeFactors
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
have : (this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)) → ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G

Tactic:
have : ∀ p, Fintype (P p) := fun p ↦ Fintype.ofFinite (P p)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
⊢ Fact (Nat.Prime p₁)

Tactic:
haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
⊢ Fact (Nat.Prime p₂)

Tactic:
haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ p₁ ≠ p₂

Tactic:
simpa using hne
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ p₁ ≠ p₂

Tactic:
have hne' : p₁ ≠ p₂ := by simpa using hne