awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
apply : Membership.mem (γ := Subgroup G) (normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)) ((↑n : G) * g)
⊢ (↑n : G)⁻¹ * ((↑n : G) * g) ∈ N ⊔ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)

Tactic:
apply mul_mem_sup (N.inv_mem n.2)

Premises used: Subgroup.inv_mem, Subgroup.mul_mem_sup, Subtype.property
-- 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
⊢ map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)

Tactic:
rw [smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← MulAut.conjNormal.map_mul,
    Sylow.ext_iff, pointwise_smul_def, Subgroup.pointwise_smul_def] at hn

Premises used: Sylow.pointwise_smul_def, MulAut.conjNormal_val, MulAut.conjNormal, Sylow.ext_iff, Subgroup.pointwise_smul_def, MonoidHom.map_mul, Sylow.smul_def, SemigroupAction.mul_smul
-- 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 :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
    (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)

Tactic:
have : Function.Injective (MulAut.conj (n * g)).toMonoidHom := (MulAut.conj (n * g)).injective
-- 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 :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
this :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
    (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)) ((↑n : G) * g)

Tactic:
fun x ↦ (mem_map_iff_mem this).symm.trans ?_

Premises used: Set.Mem, setOf, Subgroup.mem_map_iff_mem, Iff.trans, Iff.symm
-- 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 :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
this :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
    (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)
refine :
  ∀ (x : G),
    Membership.mem (α := G) (γ := Subgroup G)
        (map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)))
          (map N.subtype (↑P : Subgroup ↥N)))
        ((MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)) : (a : G) → G) x : G) ↔
      (↑n : G) * g * x * ((↑n : G) * g)⁻¹ ∈ (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)) ((↑n : G) * g)

Tactic:
refine fun x ↦ (mem_map_iff_mem this).symm.trans ?_

Premises used: Subgroup.mem_map_iff_mem, Iff.trans, Iff.symm
-- 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 :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
this :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
    (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)
x : G
rw :
  Membership.mem (α := G) (γ := Subgroup G)
      (map (MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) N.subtype)
        (↑P : Subgroup ↥N))
      ((MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)) : (a : G) → G) x : G) ↔
    (↑n : G) * g * x * ((↑n : G) * g)⁻¹ ∈
      (↑(map
            (N.subtype.comp
              ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
                ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g))))
            (↑P : Subgroup ↥N)) :
        Set G)
⊢ Membership.mem (α := G) (γ := Subgroup G)
      (map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)))
        (map N.subtype (↑P : Subgroup ↥N)))
      ((MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)) : (a : G) → G) x : G) ↔
    (↑n : G) * g * x * ((↑n : G) * g)⁻¹ ∈ (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)

Tactic:
rw [map_map, ← congr_arg (map N.subtype) hn, map_map]

Premises used: Subgroup.map, Subgroup.subtype, congr_arg, Subgroup.map_map
-- 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 :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
this :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
    (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)
x : G
⊢ Membership.mem (α := G) (γ := Subgroup G)
      (map (MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) N.subtype)
        (↑P : Subgroup ↥N))
      ((MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)) : (a : G) → G) x : G) ↔
    (↑n : G) * g * x * ((↑n : G) * g)⁻¹ ∈
      (↑(map
            (N.subtype.comp
              ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
                ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g))))
            (↑P : Subgroup ↥N)) :
        Set G)

Tactic:
rfl
-- 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 G
hP : (↑P : Subgroup G) ≤ N
rw : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype (↑(P.subtype hP) : Subgroup ↥N)) : Set G) ⊔ N
rw₁ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype ((↑P : Subgroup G).subgroupOf N)) : Set G) ⊔ N
rw₂ : normalizer (↑P : Set G) ⊔ N = normalizer (↑((↑P : Subgroup G) ⊓ N) : Set G) ⊔ N
rw₃ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(↑P : Subgroup G) : Set G) ⊔ N
rw₄ rw₅ : normalizer (↑P : Set G) ⊔ N = normalizer (↑P : Set G) ⊔ N
⊢ normalizer (↑P : Set G) ⊔ N = ⊤

Tactic:
rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
    inf_of_le_left hP, P.coe_coe]

Premises used: inf_of_le_left, Subgroup.subgroupOf_map_subtype, Sylow.coe_coe, Sylow.coe_subtype, Sylow.normalizer_sup_eq_top, Sylow.subtype
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
s : Subgroup G
t : Set (G ⧸ s)
rw : Nat.card.{u} (↑(mk ⁻¹' t) : Type u) = Nat.card.{u} (↥s × (↑t : Type u))
rw₁ rw₂ : Nat.card.{u} (↥s × (↑t : Type u)) = Nat.card.{u} (↥s × (↑t : Type u))
⊢ Nat.card.{u} (↑(mk ⁻¹' t) : Type u) = Nat.card.{u} ↥s * Nat.card.{u} (↑t : Type u)

Tactic:
rw [← Nat.card_prod, Nat.card_congr (preimageMkEquivSubgroupProdSet _ _)]

Premises used: Nat.card_congr, QuotientGroup.preimageMkEquivSubgroupProdSet, Nat.card_prod
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : Membership.mem (γ := Set (G ⧸ H)) (MulAction.fixedPoints (↥H) (G ⧸ H)) (↑x : G ⧸ H)
ha : ∀ {y : G ⧸ H}, Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) y → y = (↑x : G ⧸ H)
n : G
hn : n ∈ H
this : (n⁻¹ * x)⁻¹ * x ∈ H
⊢ x⁻¹ * n * x ∈ H

Tactic:
rw [mul_inv_rev, inv_inv] at this

Premises used: inv_inv, mul_inv_rev
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : Membership.mem (γ := Set (G ⧸ H)) (MulAction.fixedPoints (↥H) (G ⧸ H)) (↑x : G ⧸ H)
ha : ∀ {y : G ⧸ H}, Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) y → y = (↑x : G ⧸ H)
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹ * n * x ∈ H

Tactic:
this
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : Membership.mem (γ := Set (G ⧸ H)) (MulAction.fixedPoints (↥H) (G ⧸ H)) (↑x : G ⧸ H)
ha : ∀ {y : G ⧸ H}, Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) y → y = (↑x : G ⧸ H)
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
h : x⁻¹⁻¹ = x
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H

Tactic:
convert! this
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : Membership.mem (γ := Set (G ⧸ H)) (MulAction.fixedPoints (↥H) (G ⧸ H)) (↑x : G ⧸ H)
ha : ∀ {y : G ⧸ H}, Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) y → y = (↑x : G ⧸ H)
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
h h₁ : x = x
⊢ x⁻¹⁻¹ = x

Tactic:
rw [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y_1 : G ⧸ H
y : G
hy : Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) (Quotient.mk'' y)
b : G
hb₁ : b ∈ H
hb₂_1 :
  Eq (α := G ⧸ H)
    ((fun (m : ↥H) ↦ HSMul.hSMul (β := G ⧸ H) m (↑x : G ⧸ H)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) b hb₁))
    (Quotient.mk'' y)
hb₂ : (b * x)⁻¹ * y ∈ H
⊢ x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H

Tactic:
rw [hx] at hb₂
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y_1 : G ⧸ H
y : G
hy : Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) (Quotient.mk'' y)
b : G
hb₁ : b ∈ H
hb₂_1 :
  Eq (α := G ⧸ H)
    ((fun (m : ↥H) ↦ HSMul.hSMul (β := G ⧸ H) m (↑x : G ⧸ H)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) b hb₁))
    (Quotient.mk'' y)
hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H

Tactic:
simpa [mul_inv_rev, mul_assoc] using hb₂

Premises used: mul_assoc, mul_inv_rev
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x y : ↥(normalizer (↑H : Set G))
unfold_projs :
  (leftRel (comap (normalizer H.carrier).subtype H) :
        { x : G // (normalizer H.carrier).carrier.Mem x } → { x : G // (normalizer H.carrier).carrier.Mem x } → Prop)
      x y ↔
    (leftRel H : G → G → Prop) (↑x : G) (↑y : G)
⊢ (leftRel (comap (normalizer (↑H : Set G)).subtype H) : ↥(normalizer (↑H : Set G)) → ↥(normalizer (↑H : Set G)) → Prop)
      x y ↔
    (leftRel H : G → G → Prop) (↑x : G) (↑y : G)

Tactic:
unfold_projs
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x y : ↥(normalizer (↑H : Set G))
rw :
  Membership.mem (γ := Subgroup ↥(normalizer (↑H : Set G))) (comap (Subgroup.subtype (normalizer H.carrier)) H)
      (x⁻¹ * y) ↔
    (↑x : G)⁻¹ * (↑y : G) ∈ H
⊢ (leftRel (comap (normalizer H.carrier).subtype H) :
        { x : G // (normalizer H.carrier).carrier.Mem x } → { x : G // (normalizer H.carrier).carrier.Mem x } → Prop)
      x y ↔
    (leftRel H : G → G → Prop) (↑x : G) (↑y : G)

Tactic:
rw [leftRel_apply (α := normalizer (H : Set G)), leftRel_apply]

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x y : ↥(normalizer (↑H : Set G))
⊢ Membership.mem (γ := Subgroup ↥(normalizer (↑H : Set G))) (comap (Subgroup.subtype (normalizer H.carrier)) H)
      (x⁻¹ * y) ↔
    (↑x : G)⁻¹ * (↑y : G) ∈ H

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
rw : Nat.card.{u} (↑(MulAction.fixedPoints (↥H) (G ⧸ H)) : Type u) ≡ Nat.card.{u} (G ⧸ H) [MOD p]
⊢ Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (comap (Subgroup.subtype (normalizer (↑H : Set G))) H)) ≡
    Nat.card.{u} (G ⧸ H) [MOD p]

Tactic:
rw [← Nat.card_congr (fixedPointsMulLeftCosetsEquivQuotient H)]

Premises used: Sylow.fixedPointsMulLeftCosetsEquivQuotient, Nat.card_congr
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
⊢ Nat.card.{u} (↑(MulAction.fixedPoints (↥H) (G ⧸ H)) : Type u) ≡ Nat.card.{u} (G ⧸ H) [MOD p]

Tactic:
((IsPGroup.of_card hH).card_modEq_card_fixedPoints _).symm

Premises used: IsPGroup.card_modEq_card_fixedPoints, Nat.ModEq.symm, IsPGroup.of_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
⊢ Nat.card.{u} (↑(MulAction.fixedPoints (↥H) (G ⧸ H)) : Type u) ≡ Nat.card.{u} (G ⧸ H) [MOD p]

Tactic:
exact ((IsPGroup.of_card hH).card_modEq_card_fixedPoints _).symm

Premises used: IsPGroup.card_modEq_card_fixedPoints, Nat.ModEq.symm, IsPGroup.of_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
have :
  ∀ (this : ↥(H.subgroupOf (normalizer (↑H : Set G))) ≃ ↥H),
    Nat.card.{u} ↥(normalizer (↑H : Set G)) ≡ Nat.card G [MOD p ^ (n + 1)]
⊢ Nat.card.{u} ↥(normalizer (↑H : Set G)) ≡ Nat.card G [MOD p ^ (n + 1)]

Tactic:
have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer (↑H : Set G))) ≃ ↥H
rw :
  Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) *
      p ^ n ≡
    Nat.card.{u} (G ⧸ H) * p ^ n [MOD p * p ^ n]
⊢ Nat.card.{u} ↥(normalizer (↑H : Set G)) ≡ Nat.card G [MOD p ^ (n + 1)]

Tactic:
rw [card_eq_card_quotient_mul_card_subgroup H,
    card_eq_card_quotient_mul_card_subgroup (H.subgroupOf (normalizer H)), Nat.card_congr this,
    hH, pow_succ']

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, Subgroup.subgroupOf, Subgroup.normalizer, Nat.card_congr, SetLike.coe, pow_succ'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer (↑H : Set G))) ≃ ↥H
⊢ Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) *
      p ^ n ≡
    Nat.card.{u} (G ⧸ H) * p ^ n [MOD p * p ^ n]

Tactic:
(card_quotient_normalizer_modEq_card_quotient hH).mul_right' _

Premises used: Subgroup.subgroupOf, Sylow.card_quotient_normalizer_modEq_card_quotient, Nat.ModEq.mul_right'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer (↑H : Set G))) ≃ ↥H
⊢ Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) *
      p ^ n ≡
    Nat.card.{u} (G ⧸ H) * p ^ n [MOD p * p ^ n]

Tactic:
exact (card_quotient_normalizer_modEq_card_quotient hH).mul_right' _

Premises used: Sylow.card_quotient_normalizer_modEq_card_quotient, Nat.ModEq.mul_right'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
inst_2 : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
rw : Nat.card G = s * p * Nat.card.{u} ↥H
rw₁ : Nat.card G = s * p * p ^ n
rw₂ : s * p ^ (n + 1) = s * p * p ^ n
rw₃ : s * (p * p ^ n) = s * p * p ^ n
rw₄ : s * (p * p ^ n) = s * (p * p ^ n)
rw₅ rw₆ : s * (p ^ n * p) = s * (p ^ n * p)
⊢ Nat.card.{u} (G ⧸ H) * Nat.card.{u} ↥H = s * p * Nat.card.{u} ↥H

Tactic:
rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, mul_assoc, mul_comm, pow_succ'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
inst_2 : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (comap (Subgroup.subtype (normalizer (↑H : Set G))) H)) %
      p
rwa :
  ∀
    (hm :
      0 =
        Nat.card.{u}
            (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
              (comap (Subgroup.subtype (normalizer (↑H : Set G))) H)) %
          p),
    Nat.card.{u}
          (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
            (comap (Subgroup.subtype (normalizer (↑H : Set G))) H)) %
        p =
      0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hm :
      Nat.card.{u}
            (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
              (comap (Subgroup.subtype (normalizer (↑H : Set G))) H)) %
          p =
        0),
    Nat.card.{u}
          (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
            (comap (Subgroup.subtype (normalizer (↑H : Set G))) H)) %
        p =
      0
⊢ Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (comap (Subgroup.subtype (normalizer (↑H : Set G))) H)) %
      p =
    0

Tactic:
rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm

Premises used: eq_comm, dvd_mul_left, Nat.mod_eq_zero_of_dvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
_hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
⊢ p ^ (n + 1) ∣ Nat.card.{u} ↥(normalizer (↑H : Set G))

Tactic:
Nat.modEq_zero_iff_dvd.1 ((card_normalizer_modEq_card hH).trans hdvd.modEq_zero_nat)

Premises used: Dvd.dvd.modEq_zero_nat, Iff.mp, Nat.modEq_zero_iff_dvd, Nat.ModEq.trans, Sylow.card_normalizer_modEq_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
rw : Nat.card G = s * p * Nat.card.{u} ↥H
rw₁ : Nat.card G = s * p * p ^ n
rw₂ : s * p ^ (n + 1) = s * p * p ^ n
rw₃ : s * (p * p ^ n) = s * p * p ^ n
rw₄ : s * (p * p ^ n) = s * (p * p ^ n)
rw₅ rw₆ : s * (p ^ n * p) = s * (p ^ n * p)
⊢ Nat.card.{u} (G ⧸ H) * Nat.card.{u} ↥H = s * p * Nat.card.{u} ↥H

Tactic:
rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, mul_assoc, mul_comm, pow_succ'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
rwa :
  ∀
    (hm :
      0 =
        Nat.card.{u}
            (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
              (H.subgroupOf (normalizer (↑H : Set G)))) %
          p),
    Nat.card.{u}
          (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
            (H.subgroupOf (normalizer (↑H : Set G)))) %
        p =
      0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hm :
      Nat.card.{u}
            (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
              (H.subgroupOf (normalizer (↑H : Set G)))) %
          p =
        0),
    Nat.card.{u}
          (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
            (H.subgroupOf (normalizer (↑H : Set G)))) %
        p =
      0
⊢ Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p =
    0

Tactic:
rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm

Premises used: eq_comm, dvd_mul_left, Nat.mod_eq_zero_of_dvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card.{u} ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card.{u} (G ⧸ H) = s * p
hm :
  s * p % p =
    Nat.card.{u}
        (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
          (H.subgroupOf (normalizer (↑H : Set G)))) %
      p
hm' :
  p ∣
    Nat.card.{u}
      (HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
        (H.subgroupOf (normalizer (↑H : Set G))))
x :
  HasQuotient.Quotient ↥(normalizer (↑H : Set G)) (B := Subgroup ↥(normalizer (↑H : Set G)))
    (H.subgroupOf (normalizer (↑H : Set G)))
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer (↑H : Set G)))
this :
  Nat.card.{u}
      (↑(Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) ''
            (↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G)))) :
        Type u) =
    p ^ (n + 1)
⊢ Nat.card.{u}
      (↑(Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) x) ''
            (↑(comap (mk' (H.subgroupOf (normalizer (↑H : Set G)))) (zpowers x)) : Set ↥(normalizer (↑H : Set G)))) :
        Type u) =
    p ^ (n + 1)

Tactic:
this