awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h2 : (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h : ↥(centralizer (↑(zpowers x) : Set G))
hh : (((↑h : G) * g) • P).subtype ⋯ = P.subtype h1
rw : g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * (↑h : G) * g
rw₁ : g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * (↑h : G) * x * g
rw₂ : g⁻¹ * x * g = g⁻¹ * (↑h : G)⁻¹ * (↑h : G) * x * g
rw₃ rw₄ : g⁻¹ * x * g = g⁻¹ * x * g
⊢ g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * ((↑h : G) * g)

Tactic:
rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]

Premises used: mul_assoc, Subgroup.mem_zpowers, Commute.right_comm, Subtype.prop, mul_inv_rev, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
_hP : IsMulCommutative.{u_1} ↥(↑P : Subgroup G)
x g : G
hx : x ∈ P
hy : g⁻¹ * x * g ∈ P
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
P.conj_eq_normalizer_conj_of_mem_centralizer x g
    (P.le_centralizer hx) (P.le_centralizer hy)

Premises used: Sylow.toSubgroup, Subgroup.le_centralizer, Sylow.conj_eq_normalizer_conj_of_mem_centralizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
rw rw₁ :
  HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G)) ≃
    HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G))
⊢ HasQuotient.Quotient G (B := Subgroup G) (stabilizer G P) ≃
    HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G))

Tactic:
rw [P.stabilizer_eq_normalizer]

Premises used: Sylow.stabilizer_eq_normalizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G)))

Tactic:
Finite.of_equiv (Sylow p G) P.equivQuotientNormalizer

Premises used: Sylow.equivQuotientNormalizer, Finite.of_equiv, Sylow
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
⊢ Nat.card.{u_1} (Sylow p G) = Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G)))

Tactic:
Nat.card_congr P.equivQuotientNormalizer

Premises used: Sylow.equivQuotientNormalizer, Nat.card_congr
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
⊢ Nat.card.{u_1} (Sylow p G) = index (normalizer (↑P : Set G))

Tactic:
P.card_eq_card_quotient_normalizer

Premises used: Subgroup.index, Sylow.card_eq_card_quotient_normalizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
⊢ Nat.card.{u_1} (Sylow p G) ∣ (↑P : Subgroup G).index

Tactic:
((congr_arg _ P.card_eq_index_normalizer).mp dvd_rfl).trans
    (index_dvd_of_le le_normalizer)

Premises used: Eq.mp, Subgroup.le_normalizer, congr_arg, dvd_rfl, Subgroup.index_dvd_of_le, Sylow.card_eq_index_normalizer, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h : p ∣ (↑P : Subgroup G).index
⊢ p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))

Tactic:
rw [P.index_eq_card] at h

Premises used: Sylow.toSubgroup, Subgroup.index_eq_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
obtain : ∀ (x : G ⧸ (↑P : Subgroup G)) (hx : orderOf x = p), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card' (G := G ⧸ (P : Subgroup G)) p h

Premises used: exists_prime_orderOf_dvd_card'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
⊢ IsPGroup.{u_1} p ↥(zpowers x)

Tactic:
have h := IsPGroup.of_card (((Nat.card_zpowers x).trans hx).trans (pow_one p).symm)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hϕ : IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' (↑P : Subgroup G)))
⊢ IsPGroup.{u_1} p ↥Q

Tactic:
apply h.comap_of_ker_isPGroup

Premises used: IsPGroup.comap_of_ker_isPGroup
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hϕ : IsPGroup.{u_1} p ↥(↑P : Subgroup G)
⊢ IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' (↑P : Subgroup G)))

Tactic:
rw [QuotientGroup.ker_mk']

Premises used: QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ IsPGroup.{u_1} p ↥(↑P : Subgroup G)

Tactic:
P.2

Premises used: Sylow.isPGroup'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ IsPGroup.{u_1} p ↥(↑P : Subgroup G)

Tactic:
exact P.2

Premises used: Sylow.isPGroup'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ IsPGroup.{u_1} p ↥Q

Tactic:
have hQ : IsPGroup p Q := by
    apply h.comap_of_ker_isPGroup
    rw [QuotientGroup.ker_mk']
    exact P.2
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hQ : IsPGroup.{u_1} p ↥Q
⊢ ¬x = 1

Tactic:
replace hp := mt orderOf_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hQ : IsPGroup.{u_1} p ↥Q
hp : ¬x = 1
⊢ (↑P : Subgroup G) < comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)

Tactic:
rw [← zpowers_eq_bot, ← Ne, ← bot_lt_iff_ne_bot, ←
    comap_lt_comap_of_surjective (QuotientGroup.mk'_surjective _), MonoidHom.comap_bot,
    QuotientGroup.ker_mk'] at hp

Premises used: MonoidHom.comap_bot, Subgroup.comap_lt_comap_of_surjective, bot_lt_iff_ne_bot, Ne, Subgroup.zpowers_eq_bot, QuotientGroup.mk'_surjective, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hQ : IsPGroup.{u_1} p ↥Q
hp : (↑P : Subgroup G) < comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ False

Tactic:
hp.ne' (P.3 hQ hp.le)

Premises used: LT.lt.le, Sylow.is_maximal', LT.lt.ne'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hQ : IsPGroup.{u_1} p ↥Q
hp : (↑P : Subgroup G) < comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ False

Tactic:
exact hp.ne' (P.3 hQ hp.le)

Premises used: LT.lt.le, Sylow.is_maximal', LT.lt.ne'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
rw : ¬p ∣ (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) * Nat.card.{u_1} (Sylow p G)
⊢ ¬p ∣ (↑P : Subgroup G).index

Tactic:
rw [← relIndex_mul_index le_normalizer, P.coe_coe, ← card_eq_index_normalizer]

Premises used: Subgroup.relIndex_mul_index, Subgroup.le_normalizer, Sylow.coe_coe, Sylow.card_eq_index_normalizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
⊢ (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal

Tactic:
haveI : (P.subtype le_normalizer).Normal :=
    Subgroup.normal_in_normalizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
this : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal
⊢ (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).FiniteIndex

Tactic:
haveI : (P.subtype le_normalizer).FiniteIndex := ⟨hP⟩
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
this_1 : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal
this : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).FiniteIndex
⊢ ¬p ∣ (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).index

Tactic:
replace hP := not_dvd_index_aux (P.subtype le_normalizer)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
this_1 : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal
this : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).FiniteIndex
hP : ¬p ∣ (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).index
⊢ ¬p ∣ (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) * Nat.card.{u_1} (Sylow p G)

Tactic:
hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)

Premises used: Nat.Prime.not_dvd_mul, not_dvd_card_sylow, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
this_1 : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal
this : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).FiniteIndex
hP : ¬p ∣ (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).index
⊢ ¬p ∣ (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) * Nat.card.{u_1} (Sylow p G)

Tactic:
exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)

Premises used: Nat.Prime.not_dvd_mul, not_dvd_card_sylow, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ Finite.{u_1 + 1} (Sylow p G)

Tactic:
have := P.finite_of_finiteIndex
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
this : Finite.{u_1 + 1} (Sylow p G)
⊢ ¬p ∣ (↑P : Subgroup G).index

Tactic:
P.not_dvd_index' Nat.card_pos.ne'

Premises used: Sylow.not_dvd_index', Nat.card_pos, LT.lt.ne'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
this : Finite.{u_1 + 1} (Sylow p G)
⊢ ¬p ∣ (↑P : Subgroup G).index

Tactic:
exact P.not_dvd_index' Nat.card_pos.ne'

Premises used: Sylow.not_dvd_index', Nat.card_pos, LT.lt.ne'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
inst_3 : Fact (Nat.Prime p)
P : Sylow p G
⊢ (↑(mapSurjective hf P) : Subgroup G') = map f (↑P : Subgroup G)

Tactic:
rfl

Premises used: Subgroup.map, rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
⊢ Finite G'

Tactic:
have : Finite G' := Finite.of_surjective f hf
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
⊢ map f Q ≤ (↑P : Subgroup G')

Tactic:
have hPQ : Q.map f ≤ P := Subgroup.map_le_iff_le_comap.mpr (Subgroup.map_subtype_le Q₀.1)
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
⊢ IsPGroup.{u_1} p ↥Q

Tactic:
have hpQ : IsPGroup p Q := Q₀.2.map (P.comap f).subtype
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
rw : ¬p ∣ (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G'))).index * (↑P : Subgroup G').index
⊢ ¬p ∣ Q.index

Tactic:
rw [Subgroup.index_map_subtype Q₀.1, P.index_comap_of_surjective hf]

Premises used: Sylow.toSubgroup, Subgroup.index_comap_of_surjective, Subgroup.index_map_subtype
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
⊢ ¬p ∣ (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G'))).index * (↑P : Subgroup G').index

Tactic:
Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index

Premises used: Nat.Prime.not_dvd_mul, Sylow.not_dvd_index, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
⊢ ¬p ∣ (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G'))).index * (↑P : Subgroup G').index

Tactic:
exact Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index

Premises used: Nat.Prime.not_dvd_mul, Sylow.not_dvd_index, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
⊢ ¬p ∣ Q.index

Tactic:
have hQ : ¬ p ∣ Q.index := by
    rw [Subgroup.index_map_subtype Q₀.1, P.index_comap_of_surjective hf]
    exact Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
hQ : ¬p ∣ Q.index
h : mapSurjective hf (hpQ.toSylow hQ) = P
⊢ ∃ (a : Sylow p G), mapSurjective hf a = P

Tactic:
use hpQ.toSylow hQ

Premises used: IsPGroup.toSylow
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
hQ : ¬p ∣ Q.index
h : (↑P : Subgroup G') = map f (↑(hpQ.toSylow hQ) : Subgroup G)
⊢ mapSurjective hf (hpQ.toSylow hQ) = P

Tactic:
rw [Sylow.ext_iff, Sylow.coe_mapSurjective, eq_comm]

Premises used: Sylow.ext_iff, eq_comm, Sylow.coe_mapSurjective
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
hQ : ¬p ∣ Q.index
⊢ (↑P : Subgroup G') = map f (↑(hpQ.toSylow hQ) : Subgroup G)

Tactic:
((hpQ.map f).toSylow (fun h ↦ hQ (h.trans (Q.index_map_dvd hf)))).3 P.2 hPQ

Premises used: Sylow.isPGroup', Subgroup.map, IsPGroup.toSylow, Sylow.is_maximal', Subgroup.index_map_dvd, IsPGroup.map, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
hQ : ¬p ∣ Q.index
⊢ (↑P : Subgroup G') = map f (↑(hpQ.toSylow hQ) : Subgroup G)

Tactic:
exact ((hpQ.map f).toSylow (fun h ↦ hQ (h.trans (Q.index_map_dvd hf)))).3 P.2 hPQ

Premises used: Sylow.isPGroup', IsPGroup.toSylow, Sylow.is_maximal', Subgroup.index_map_dvd, IsPGroup.map, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
⊢ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N = ⊤

Tactic:
top_le_iff.mp fun g _ => ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
refine :
  ∀ (g : G), Membership.mem (γ := Subgroup G) ⊤ g → g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N
⊢ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N = ⊤

Tactic:
refine top_le_iff.mp fun g _ => ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
obtain :
  ∀ (n : ↥N) (hn : n • HSMul.hSMul (α := MulAut ↥N) ((MulAut.conjNormal : (a : G) → MulAut ↥N) g : MulAut ↥N) P = P),
    g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N
⊢ g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N

Tactic:
obtain ⟨n, hn⟩ := exists_smul_eq N ((MulAut.conjNormal g : MulAut N) • P) P

Premises used: MulAut.conjNormal, Membership.mem, Subtype, HSMul.hSMul, MulAction.exists_smul_eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
n : ↥N
hn : n • HSMul.hSMul (α := MulAut ↥N) ((MulAut.conjNormal : (a : G) → MulAut ↥N) g : MulAut ↥N) P = P
rw : (↑n : G)⁻¹ * ((↑n : G) * g) ∈ N ⊔ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)
⊢ g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N

Tactic:
rw [← inv_mul_cancel_left (↑n) g, sup_comm]

Premises used: inv_mul_cancel_left, sup_comm