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)
P : Subgroup G
hP1 : IsPGroup.{u_1} p ↥P
hP2 : ¬p ∣ P.index
⊢ (↑(hP1.toSylow hP2) : Subgroup G) = P

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup.{u_1} p ↥P
hP2 : ¬p ∣ P.index
g : G
⊢ g ∈ hP1.toSylow hP2 ↔ g ∈ P

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p_1 : ℕ
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card.{u_1} ↥H = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
rw : ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣ Nat.card G
⊢ ¬p ∣ H.index

Tactic:
rw [← mul_dvd_mul_iff_left (Nat.card_pos (α := H)).ne', card_mul_index, card_eq, ← pow_succ]

Premises used: Nat.card_pos, pow_succ, LT.lt.ne', mul_dvd_mul_iff_left, Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p_1 : ℕ
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card.{u_1} ↥H = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣ Nat.card G

Tactic:
Nat.pow_succ_factorization_not_dvd Nat.card_pos.ne' Fact.out

Premises used: Nat.pow_succ_factorization_not_dvd, Nat.card_pos, LT.lt.ne', Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p_1 : ℕ
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card.{u_1} ↥H = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ¬p ^ HAdd.hAdd (α := ℕ) (β := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣ Nat.card G

Tactic:
exact Nat.pow_succ_factorization_not_dvd Nat.card_pos.ne' Fact.out

Premises used: Nat.pow_succ_factorization_not_dvd, Nat.card_pos, LT.lt.ne', Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
H : Subgroup G
card_eq : Nat.card.{u_1} ↥H = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (↑(ofCard H card_eq) : Subgroup G) = H

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
h : (↑P : Subgroup G) ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup.{u_2} p ↥Q
hle : comap ϕ (↑P : Subgroup G) ≤ Q
rw : Q = comap ϕ (map ϕ Q)
⊢ Q = comap ϕ (↑P : Subgroup G)

Tactic:
rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]

Premises used: ge_of_eq, Sylow.is_maximal', Subgroup.map_comap_eq_self, Subgroup.map_mono, IsPGroup.map, le_trans
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
h : (↑P : Subgroup G) ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup.{u_2} p ↥Q
hle : comap ϕ (↑P : Subgroup G) ≤ Q
⊢ Q = comap ϕ (map ϕ Q)

Tactic:
(comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm

Premises used: Sylow.toSubgroup, Subgroup.ker_le_comap, Subgroup.comap_map_eq_self, LE.le.trans, Eq.symm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
h : (↑P : Subgroup G) ≤ ϕ.range
Q : Subgroup K
hQ : IsPGroup.{u_2} p ↥Q
hle : comap ϕ (↑P : Subgroup G) ≤ Q
⊢ Q = comap ϕ (map ϕ Q)

Tactic:
exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm

Premises used: Sylow.toSubgroup, Subgroup.ker_le_comap, Subgroup.comap_map_eq_self, LE.le.trans, Eq.symm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
h : (↑P : Subgroup G) ≤ ϕ.range
⊢ (↑(P.comapOfKerIsPGroup ϕ hϕ h) : Subgroup K) = comap ϕ (↑P : Subgroup G)

Tactic:
rfl

Premises used: Subgroup.comap, rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : Function.Injective.{u_2 + 1, u_1 + 1} (α := K) (β := G) (⇑ϕ : (a : K) → G)
h : (↑P : Subgroup G) ≤ ϕ.range
⊢ (↑(P.comapOfInjective ϕ hϕ h) : Subgroup K) = comap ϕ (↑P : Subgroup G)

Tactic:
rfl

Premises used: Subgroup.comap, rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
N : Subgroup G
h rwa rwa₁ rwa₂ rwa₃ : (↑P : Subgroup G) ≤ N
⊢ (↑P : Subgroup G) ≤ N.subtype.range

Tactic:
rwa [range_subtype]

Premises used: Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
N : Subgroup G
h : (↑P : Subgroup G) ≤ N
⊢ (↑(P.subtype h) : Subgroup ↥N) = (↑P : Subgroup G).subgroupOf N

Tactic:
rfl

Premises used: Subgroup.subgroupOf, Subgroup.comap, rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
N : Subgroup G
P Q : Sylow p G
hP : (↑P : Subgroup G) ≤ N
hQ : (↑Q : Subgroup G) ≤ N
h : P.subtype hP = Q.subtype hQ
rw : ∀ (h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ) (x : G), x ∈ P ↔ x ∈ Q
⊢ P = Q

Tactic:
rw [SetLike.ext_iff] at h ⊢

Premises used: SetLike.ext_iff
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
N : Subgroup G
P Q : Sylow p G
hP : (↑P : Subgroup G) ≤ N
hQ : (↑Q : Subgroup G) ≤ N
h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ
⊢ ∀ (x : G), x ∈ P ↔ x ∈ Q

Tactic:
fun g => ⟨fun hg => (h ⟨g, hP hg⟩).mp hg, fun hg => (h ⟨g, hQ hg⟩).mpr hg⟩

Premises used: Iff.mpr, Subtype.mk, Iff.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
N : Subgroup G
P Q : Sylow p G
hP : (↑P : Subgroup G) ≤ N
hQ : (↑Q : Subgroup G) ≤ N
h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ
⊢ ∀ (x : G), x ∈ P ↔ x ∈ Q

Tactic:
exact fun g => ⟨fun hg => (h ⟨g, hP hg⟩).mp hg, fun hg => (h ⟨g, hQ hg⟩).mpr hg⟩
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q : Subgroup G | IsPGroup.{u_1} p ↥Q}
hc2 : IsChain (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x : ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : (↑c : Type u_1)
hg : Membership.mem (γ := Set G) ((fun (R : (↑c : Type u_1)) ↦ (↑(↑R : Subgroup G) : Set G)) S) g
⊢ ∃ (k : ℕ),
    HPow.hPow (α :=
        ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
            inv_mem' := ⋯ : Subgroup G })
        (Subtype.mk (p := fun (x : G) ↦
          Membership.mem (γ := Subgroup G)
            { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
              inv_mem' := ⋯ : Subgroup G }
            x)
          g ⋯)
        (p ^ k) =
      1

Tactic:
Exists.imp (fun k hk => ?_) (hc1 S.2 ⟨g, hg⟩)

Premises used: Exists.imp, Subtype.mk, Subtype.property
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q : Subgroup G | IsPGroup.{u_1} p ↥Q}
hc2 : IsChain (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x : ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : (↑c : Type u_1)
hg : Membership.mem (γ := Set G) ((fun (R : (↑c : Type u_1)) ↦ (↑(↑R : Subgroup G) : Set G)) S) g
refine :
  ∀ (k : ℕ) (hk : Subtype.mk (p := fun (x : G) ↦ x ∈ (↑S : Subgroup G)) g hg ^ p ^ k = 1),
    HPow.hPow (α :=
        ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
            inv_mem' := ⋯ : Subgroup G })
        (Subtype.mk (p := fun (x : G) ↦
          Membership.mem (γ := Subgroup G)
            { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
              inv_mem' := ⋯ : Subgroup G }
            x)
          g ⋯)
        (p ^ k) =
      1
⊢ ∃ (k : ℕ),
    HPow.hPow (α :=
        ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
            inv_mem' := ⋯ : Subgroup G })
        (Subtype.mk (p := fun (x : G) ↦
          Membership.mem (γ := Subgroup G)
            { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
              inv_mem' := ⋯ : Subgroup G }
            x)
          g ⋯)
        (p ^ k) =
      1

Tactic:
refine Exists.imp (fun k hk => ?_) (hc1 S.2 ⟨g, hg⟩)

Premises used: Exists.imp, Subtype.mk, Subtype.property
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q : Subgroup G | IsPGroup.{u_1} p ↥Q}
hc2 : IsChain (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x : ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : (↑c : Type u_1)
hg : Membership.mem (γ := Set G) ((fun (R : (↑c : Type u_1)) ↦ (↑(↑R : Subgroup G) : Set G)) S) g
k : ℕ
hk : Subtype.mk (p := fun (x : G) ↦ x ∈ (↑S : Subgroup G)) g hg ^ p ^ k = 1
rwa :
  ∀ (hk : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ (↑S : Subgroup G)) g hg ^ p ^ k) : G) = (↑1 : G)),
    (↑(HPow.hPow (α :=
            ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
                inv_mem' := ⋯ : Subgroup G })
            (Subtype.mk (p := fun (x : G) ↦
              Membership.mem (γ := Subgroup G)
                { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
                  inv_mem' := ⋯ : Subgroup G }
                x)
              g ⋯)
            (p ^ k)) :
        G) =
      (↑1 : G)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hk : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ (↑S : Subgroup G)) g hg) : G) ^ p ^ k = (↑1 : G)),
    (↑(Subtype.mk (p := fun (x : G) ↦
              Membership.mem (γ := Subgroup G)
                { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
                  inv_mem' := ⋯ : Subgroup G }
                x)
              g ⋯) :
          G) ^
        p ^ k =
      (↑1 : G)
⊢ HPow.hPow (α :=
      ↥{ carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ :
          Subgroup G })
      (Subtype.mk (p := fun (x : G) ↦
        Membership.mem (γ := Subgroup G)
          { carrier := ⋃ (R : (↑c : Type u_1)), (↑(↑R : Subgroup G) : Set G), mul_mem' := ⋯, one_mem' := ⋯,
            inv_mem' := ⋯ : Subgroup G }
          x)
        g ⋯)
      (p ^ k) =
    1

Tactic:
rwa [Subtype.ext_iff, coe_pow] at hk ⊢

Premises used: Subgroup.coe_pow, Subtype.ext_iff
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
⊢ Nonempty.{u_1 + 1} (Sylow p G)

Tactic:
IsPGroup.of_bot.exists_le_sylow.nonempty

Premises used: Exists.nonempty, IsPGroup.exists_le_sylow, IsPGroup.of_bot
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
P : Sylow p H
f : H →* G
hf : IsPGroup.{u_2} p ↥f.ker
⊢ ∃ (Q : Sylow p G), comap f (↑Q : Subgroup G) = (↑P : Subgroup H)

Tactic:
Exists.imp (fun Q hQ => P.3 (Q.2.comap_of_ker_isPGroup f hf) (map_le_iff_le_comap.mp hQ))
    (P.2.map f).exists_le_sylow

Premises used: Sylow.isPGroup', IsPGroup.comap_of_ker_isPGroup, Exists.imp, Sylow.is_maximal', IsPGroup.exists_le_sylow, Subgroup.map_le_iff_le_comap, Iff.mp, IsPGroup.map
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
P : Sylow p H
f : H →* G
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := G) (⇑f : (a : H) → G)
⊢ ∃ (Q : Sylow p G), comap f (↑Q : Subgroup G) = (↑P : Subgroup H)

Tactic:
P.exists_comap_eq_of_ker_isPGroup (IsPGroup.ker_isPGroup_of_injective hf)

Premises used: IsPGroup.ker_isPGroup_of_injective, Sylow.exists_comap_eq_of_ker_isPGroup
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
P : Sylow p ↥H
⊢ ∃ (Q : Sylow p G), comap H.subtype (↑Q : Subgroup G) = (↑P : Subgroup ↥H)

Tactic:
P.exists_comap_eq_of_injective Subtype.coe_injective

Premises used: Sylow.exists_comap_eq_of_injective, Subtype.coe_injective
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : H →* G
hf : IsPGroup.{u_2} p ↥f.ker
inst_2 : Finite.{u_1 + 1} (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ (Q : Sylow p G), comap f (↑Q : Subgroup G) = (↑P : Subgroup H) := ⋯
g : Sylow p H → Sylow p G :=
  fun (P : Sylow p H) ↦ Classical.choose (p := fun (x : Sylow p G) ↦ comap f (↑x : Subgroup G) = (↑P : Subgroup H)) ⋯
hg : ∀ (P : Sylow p H), comap f (↑(g P) : Subgroup G) = (↑P : Subgroup H)
P Q : Sylow p H
h : g P = g Q
rw : comap f (↑(g Q) : Subgroup G) = (↑Q : Subgroup H)
⊢ (↑P : Subgroup H) = (↑Q : Subgroup H)

Tactic:
rw [← hg, h]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : H →* G
hf : IsPGroup.{u_2} p ↥f.ker
inst_2 : Finite.{u_1 + 1} (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ (Q : Sylow p G), comap f (↑Q : Subgroup G) = (↑P : Subgroup H) := ⋯
g : Sylow p H → Sylow p G :=
  fun (P : Sylow p H) ↦ Classical.choose (p := fun (x : Sylow p G) ↦ comap f (↑x : Subgroup G) = (↑P : Subgroup H)) ⋯
hg : ∀ (P : Sylow p H), comap f (↑(g P) : Subgroup G) = (↑P : Subgroup H)
P Q : Sylow p H
h : g P = g Q
⊢ comap f (↑(g Q) : Subgroup G) = (↑Q : Subgroup H)

Tactic:
(h_exists Q).choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : H →* G
hf : IsPGroup.{u_2} p ↥f.ker
inst_2 : Finite.{u_1 + 1} (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ (Q : Sylow p G), comap f (↑Q : Subgroup G) = (↑P : Subgroup H) := ⋯
g : Sylow p H → Sylow p G :=
  fun (P : Sylow p H) ↦ Classical.choose (p := fun (x : Sylow p G) ↦ comap f (↑x : Subgroup G) = (↑P : Subgroup H)) ⋯
hg : ∀ (P : Sylow p H), comap f (↑(g P) : Subgroup G) = (↑P : Subgroup H)
P Q : Sylow p H
h : g P = g Q
⊢ comap f (↑(g Q) : Subgroup G) = (↑Q : Subgroup H)

Tactic:
exact (h_exists Q).choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
f : H →* G
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := G) (⇑f : (a : H) → G)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
⊢ Finite.{u_2 + 1} (Sylow p H)

Tactic:
finite_of_ker_is_pGroup (IsPGroup.ker_isPGroup_of_injective hf)

Premises used: Sylow.finite_of_ker_is_pGroup, IsPGroup.ker_isPGroup_of_injective
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} (Sylow p G)
⊢ Finite.{u_1 + 1} (Sylow p ↥H)

Tactic:
finite_of_injective H.subtype_injective

Premises used: Subgroup.subtype_injective, Sylow.finite_of_injective
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
inst_1 : (↑P : Subgroup G).FiniteIndex
hf : IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' (↑P : Subgroup G).normalCore))
⊢ Finite.{u_1 + 1} (Sylow p G)

Tactic:
apply finite_of_ker_is_pGroup (f := QuotientGroup.mk' P.normalCore)

Premises used: Sylow.finite_of_ker_is_pGroup
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
inst_1 : (↑P : Subgroup G).FiniteIndex
hf : IsPGroup.{u_1} p ↥(↑P : Subgroup G).normalCore
⊢ IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' (↑P : Subgroup G).normalCore))

Tactic:
rw [QuotientGroup.ker_mk']

Premises used: 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).FiniteIndex
⊢ IsPGroup.{u_1} p ↥(↑P : Subgroup G).normalCore

Tactic:
P.isPGroup'.to_le P.normalCore_le

Premises used: Sylow.isPGroup', Sylow.toSubgroup, IsPGroup.to_le, Subgroup.normalCore_le
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
inst_1 : (↑P : Subgroup G).FiniteIndex
⊢ IsPGroup.{u_1} p ↥(↑P : Subgroup G).normalCore

Tactic:
exact P.isPGroup'.to_le P.normalCore_le

Premises used: Sylow.isPGroup', Sylow.toSubgroup, IsPGroup.to_le, Subgroup.normalCore_le
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : Group α
inst_2 : MulDistribMulAction α G
g : α
P : Sylow p G
⊢ (↑(g • P) : Subgroup G) = g • (↑P : Subgroup G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
g : G
P : Sylow p G
⊢ g • P = HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) P

Tactic:
rfl

Premises used: SMul.comp.smul, rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
g : G
P : Sylow p G
⊢ (↑(g • P) : Subgroup G) =
    HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) (↑P : Subgroup G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
g : G
P : Sylow p G
⊢ (↑(g • P) : Set G) = HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) (↑P : Set G)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
H : Subgroup G
hP : (↑P : Subgroup G) ≤ H
h : ↥H
⊢ (↑(h • P) : Subgroup G) ≤ H

Tactic:
Subgroup.conj_smul_le_of_le hP h

Premises used: Set.Mem, Subgroup.conj_smul_le_of_le
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
H : Subgroup G
hP : (↑P : Subgroup G) ≤ H
h : ↥H
⊢ h • P.subtype hP = (h • P).subtype ⋯

Tactic:
ext (Subgroup.conj_smul_subgroupOf hP h)

Premises used: Subgroup.conj_smul_subgroupOf, Sylow.ext
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
g : G
P : Sylow p G
rw : (∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ (↑P : Set G) ↔ g⁻¹ * h * g ∈ (↑P : Set G)
⊢ g • P = P ↔ Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) g

Tactic:
rw [eq_comm, SetLike.ext_iff, ← inv_mem_iff (G := G) (H := normalizer P),
      mem_set_normalizer_iff, inv_inv]

Premises used: inv_mem_iff, SetLike.ext_iff, eq_comm, Subgroup.mem_set_normalizer_iff, inv_inv
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
g : G
P : Sylow p G
h : G
h_1 : h ∈ g • P
a : G
b : a ∈ (↑(↑P : Subgroup G) : Set G)
c :
  (((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
            ((MulAut.conj : (a : G) → MulAut G) g) :
          Monoid.End G) :
        (a : G) → G)
      a =
    h
⊢ HMul.hMul (β := G) g⁻¹
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            a :
          G) *
      g ∈
    (↑P : Set G)

Tactic:
simpa [mul_assoc] using b

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
g : G
P : Sylow p G
⊢ (∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ (↑P : Set G) ↔ g⁻¹ * h * g ∈ (↑P : Set G)

Tactic:
exact
    forall_congr' fun h =>
      iff_congr Iff.rfl
        ⟨fun ⟨a, b, c⟩ => c ▸ by simpa [mul_assoc] using b,
          fun hh => ⟨(MulAut.conj g)⁻¹ h, hh, MulAut.apply_inv_self G (MulAut.conj g) h⟩⟩

Premises used: iff_congr, Iff.rfl, Iff.intro, forall_congr'
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
g : G
P : Sylow p G
h : (↑P : Subgroup G).Normal
⊢ g • P = P

Tactic:
simp only [smul_eq_iff_mem_normalizer, ← P.coe_coe, P.normalizer_eq_top, mem_top]

Premises used: Sylow.toSubgroup, Sylow.smul_eq_iff_mem_normalizer, Subgroup.normalizer_eq_top, Sylow.coe_coe, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
P : Sylow p G
simp_rw : Membership.mem (γ := Set (Sylow p G)) (fixedPoints (↥H) (Sylow p G)) P ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P
⊢ Membership.mem (γ := Set (Sylow p G)) (fixedPoints (↥H) (Sylow p G)) P ↔ H ≤ normalizer (↑P : Set G)

Tactic:
simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer]

Premises used: Sylow.smul_eq_iff_mem_normalizer, SetLike.le_def
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
P : Sylow p G
⊢ Membership.mem (γ := Set (Sylow p G)) (fixedPoints (↥H) (Sylow p G)) P ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P

Tactic:
Subtype.forall

Premises used: Set.Mem, setOf, Subtype.forall, MulAction.fixedPoints
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
P : Sylow p G
⊢ Membership.mem (γ := Set (Sylow p G)) (fixedPoints (↥H) (Sylow p G)) P ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P

Tactic:
exact Subtype.forall

Premises used: Subtype.forall
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
Q : Sylow p G
⊢ P ⊓ normalizer (↑Q : Set G) = P ⊓ (↑Q : Subgroup G)

Tactic:
le_antisymm
    (le_inf inf_le_left
      (sup_eq_right.mp
        (Q.3 (hP.to_inf_left.to_sup_of_normal_right' Q.2 inf_le_right) le_sup_right)))
    (inf_le_inf_left P le_normalizer)

Premises used: Sylow.isPGroup', inf_le_right, inf_le_inf_left, le_sup_right, Subgroup.le_normalizer, IsPGroup.to_inf_left, Sylow.is_maximal', le_inf, le_antisymm, sup_eq_right, IsPGroup.to_sup_of_normal_right', Iff.mp, inf_le_left
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
Q : Sylow p G
rw : P ≤ normalizer (↑Q : Set G) ↔ P ≤ (↑Q : Subgroup G)
rw₁ : P ⊓ normalizer (↑Q : Set G) = P ↔ P ≤ (↑Q : Subgroup G)
rw₂ : P ⊓ (↑Q : Subgroup G) = P ↔ P ≤ (↑Q : Subgroup G)
rw₃ rw₄ : P ≤ (↑Q : Subgroup G) ↔ P ≤ (↑Q : Subgroup G)
⊢ Membership.mem (γ := Set (Sylow p G)) (fixedPoints (↥P) (Sylow p G)) Q ↔ P ≤ (↑Q : Subgroup G)

Tactic:
rw [P.sylow_mem_fixedPoints_iff, ← inf_eq_left, hP.inf_normalizer_sylow, inf_eq_left]

Premises used: Subgroup.sylow_mem_fixedPoints_iff, inf_eq_left, IsPGroup.inf_normalizer_sylow
-- 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 Q : Sylow p G
⊢ ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)

Tactic:
have H := fun {R : Sylow p G} {S : orbit G P} =>
        calc
          S ∈ fixedPoints R (orbit G P) ↔ S.1 ∈ fixedPoints R (Sylow p G) :=
            forall_congr' fun a => Subtype.ext_iff
          _ ↔ R.1 ≤ S := R.2.sylow_mem_fixedPoints_iff
          _ ↔ S.1.1 = R := ⟨fun h => R.3 S.1.2 h, ge_of_eq⟩
-- 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 Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
this : Set.Nonempty.{u_1} (α := (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1))
R : (↑(orbit G P) : Type u_1)
hR : Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1)) R
rw : ∃ (g : G), g • P = (↑R : Sylow p G)
⊢ ∃ (g : G), g • P = Q

Tactic:
rw [← Sylow.ext (H.mp hR)]

Premises used: Sylow.ext, Iff.mp