awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw :
  Eq (α := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆})
    (closure (Set.image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}))
⊢ H.focalSubgroupOf = closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}

Tactic:
rw [← map_subtype_inj, map_focalSubgroupOf, MonoidHom.map_closure, focalSubgroup_def]

Premises used: Subgroup.map_focalSubgroupOf, Subgroup.map_subtype_inj, MonoidHom.map_closure, Subgroup.focalSubgroup_def
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
e_k :
  Eq.{u_1 + 1} (α := G → Prop) (fun (g : G) ↦ g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆) fun (x : G) ↦
    ∃ (a : ↥H),
      Membership.mem (γ := Set ↥H) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆} a ∧ (H.subtype : (a : ↥H) → G) a = x
⊢ Eq (α := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆})
    (closure (Set.image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}))

Tactic:
congr
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
e_k :
  Eq.{u_1 + 1} (α := G → Prop) (fun (g : G) ↦ g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆) fun (x : G) ↦
    (∃ x_1 ∈ H, ∃ (u : G), x = ⁅x_1, u⁆) ∧ x ∈ H
⊢ Eq.{u_1 + 1} (α := G → Prop) (fun (g : G) ↦ g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆) fun (x : G) ↦
    ∃ (a : ↥H),
      Membership.mem (γ := Set ↥H) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆} a ∧ (H.subtype : (a : ↥H) → G) a = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq.{u_1 + 1} (α := G → Prop) (fun (g : G) ↦ g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆) fun (x : G) ↦
    (∃ x_1 ∈ H, ∃ (u : G), x = ⁅x_1, u⁆) ∧ x ∈ H

Tactic:
grind
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : LE.le.{u_1} (α := Subgroup ↥H) (_root_.commutator ↥H) (closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆})
⊢ _root_.commutator ↥H ≤ H.focalSubgroupOf

Tactic:
rw [focalSubgroupOf_eq_closure]

Premises used: Subgroup.focalSubgroupOf_eq_closure
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h' :
  Subset.{u_1} (α := Set ↥H)
    {g : ↥H |
      ∃ (g₁ : ↥H),
        Membership.mem (γ := Subgroup ↥H) ⊤ g₁ ∧ ∃ (g₂ : ↥H), Membership.mem (γ := Subgroup ↥H) ⊤ g₂ ∧ ⁅g₁, g₂⁆ = g}
    {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}
⊢ LE.le.{u_1} (α := Subgroup ↥H) (_root_.commutator ↥H) (closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆})

Tactic:
apply closure_mono

Premises used: Subgroup.closure_mono
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : ↥H
⊢ Membership.mem (γ := Set ↥H) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆} ⁅a, b⁆

Tactic:
⟨a, a.2, b, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : ↥H
⊢ Membership.mem (γ := Set ↥H) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆} ⁅a, b⁆

Tactic:
exact ⟨a, a.2, b, rfl⟩
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
grw : map H.subtype (_root_.commutator ↥H) ≤ H.focalSubgroup
grw₁ : map H.subtype H.focalSubgroupOf ≤ H.focalSubgroup
grw₂ grw₃ : H.focalSubgroup ≤ H.focalSubgroup
⊢ ⁅H, H⁆ ≤ H.focalSubgroup

Tactic:
grw [← map_subtype_commutator, H.commutator_le_focalSubgroupOf, map_focalSubgroupOf]

Premises used: Subgroup.map_focalSubgroupOf, Subgroup.commutator_le_focalSubgroupOf, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ IsMulCommutative.{u_1} (↥H ⧸ H.focalSubgroupOf)

Tactic:
Normal.quotient_commutative_iff_commutator_le.mpr H.commutator_le_focalSubgroupOf

Premises used: Iff.mpr, Subgroup.Normal.quotient_commutative_iff_commutator_le, Subgroup.commutator_le_focalSubgroupOf
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
x : ↥H
have :
  ∀ (this : Fintype (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))),
    (H.transferFocal : (a : G) → ↥H ⧸ H.focalSubgroupOf) (↑x : G) =
      HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf) H.index
⊢ (H.transferFocal : (a : G) → ↥H ⧸ H.focalSubgroupOf) (↑x : G) =
    HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf) H.index

Tactic:
have : Fintype (Quotient (MulAction.orbitRel (zpowers (x : G)) (G ⧸ H))) :=
    Fintype.ofFinite _
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))
rw :
  Eq.{u_1 + 1} (α := ↥H ⧸ H.focalSubgroupOf)
    (∏ q : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
      (QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out q.out)⁻¹ * (↑x : G) ^ minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) q.out *
            Quotient.out q.out)
          ⋯))
    (∏ i : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
      HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf)
        (minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) i.out))
⊢ (H.transferFocal : (a : G) → ↥H ⧸ H.focalSubgroupOf) (↑x : G) =
    HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf) H.index

Tactic:
rw [transferFocal, index_eq_sum_minimalPeriod H x, ← Finset.prod_pow_eq_pow_sum,
    MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot]

Premises used: Subgroup.index_eq_sum_minimalPeriod, Subgroup.transferFocal, Finset.prod_pow_eq_pow_sum, Subtype.val, MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))
apply :
  ∀ (x_1 : Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H))),
    Membership.mem (γ := Finset (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))) Finset.univ
        x_1 →
      (QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            ((Quotient.out x_1.out)⁻¹ * (↑x : G) ^ minimalPeriod (fun (x_2 : G ⧸ H) ↦ (↑x : G) • x_2) x_1.out *
              Quotient.out x_1.out)
            ⋯) =
        HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf)
          (minimalPeriod (fun (x_2 : G ⧸ H) ↦ (↑x : G) • x_2) x_1.out)
⊢ Eq.{u_1 + 1} (α := ↥H ⧸ H.focalSubgroupOf)
    (∏ q : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
      (QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out q.out)⁻¹ * (↑x : G) ^ minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) q.out *
            Quotient.out q.out)
          ⋯))
    (∏ i : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
      HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf)
        (minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) i.out))

Tactic:
apply Finset.prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))
x_1 : Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H))
h :
  Membership.mem (γ := Finset (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))) Finset.univ
    x_1
⊢ (QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        ((Quotient.out x_1.out)⁻¹ * (↑x : G) ^ minimalPeriod (fun (x_2 : G ⧸ H) ↦ (↑x : G) • x_2) x_1.out *
          Quotient.out x_1.out)
        ⋯) =
    HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf)
      (minimalPeriod (fun (x_2 : G ⧸ H) ↦ (↑x : G) • x_2) x_1.out)

Tactic:
apply focalSubgroupOf.mk'_conj_eq H

Premises used: Subgroup.focalSubgroupOf.mk'_conj_eq
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ Surjective (β := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
    fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index

Tactic:
((P.2.to_quotient P.focalSubgroupOf).powEquiv' P.not_dvd_index).surjective

Premises used: Sylow.isPGroup', Sylow.toSubgroup, IsPGroup.powEquiv', IsPGroup.to_quotient, Sylow.not_dvd_index, Subgroup.focalSubgroupOf, Equiv.surjective
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
x : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf
obtain :
  ∀ (x : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf),
    ∃ (a : G),
      Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
        (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
          ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
        ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index) x :
          ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
⊢ ∃ (a : G), ((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a = x

Tactic:
obtain ⟨x, rfl⟩ := focalSubgroupOf.pow_index_surjective P x

Premises used: Subgroup.focalSubgroupOf.pow_index_surjective, rfl
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
x : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf
obtain :
  ∀ (x : ↥(↑P : Subgroup G)),
    ∃ (a : G),
      Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
        (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
          ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
        ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index)
            ((QuotientGroup.mk' (↑P : Subgroup G).focalSubgroupOf :
                (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
              x) :
          ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
⊢ ∃ (a : G),
    Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index) x :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective _ x

Premises used: QuotientGroup.mk'_surjective, rfl
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
x : ↥(↑P : Subgroup G)
⊢ ∃ (a : G),
    Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index)
          ((QuotientGroup.mk' (↑P : Subgroup G).focalSubgroupOf :
              (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
            x) :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)

Tactic:
⟨x, P.transferFocal_eq_pow x⟩

Premises used: Sylow.toSubgroup, Subgroup.transferFocal_eq_pow, Exists.intro, Subtype.val
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
x : ↥(↑P : Subgroup G)
⊢ ∃ (a : G),
    Eq (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      (((↑P : Subgroup G).transferFocal : (a : G) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) a :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
      ((fun (y : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) ↦ y ^ (↑P : Subgroup G).index)
          ((QuotientGroup.mk' (↑P : Subgroup G).focalSubgroupOf :
              (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
            x) :
        ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)

Tactic:
exact ⟨x, P.transferFocal_eq_pow x⟩
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
h :
  ∀ (g : ↥P),
    Membership.mem (γ := Subgroup ↥P) (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict P)) g ↔
      g ∈ (↑P : Subgroup G).focalSubgroupOf
⊢ MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict P) = (↑P : Subgroup G).focalSubgroupOf

Tactic:
ext g
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
g : ↥P
⊢ IsPGroup.{u_1} p (↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)

Tactic:
have hQ : IsPGroup p (P ⧸ P.focalSubgroupOf) := P.2.to_quotient P.focalSubgroupOf
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
g : ↥P
hQ : IsPGroup.{u_1} p (↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
h :
  HPow.hPow (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
        (↑g : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) (↑P : Subgroup G).index =
      1 ↔
    g ∈ (↑P : Subgroup G).focalSubgroupOf
⊢ Membership.mem (γ := Subgroup ↥P) (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict P)) g ↔
    g ∈ (↑P : Subgroup G).focalSubgroupOf

Tactic:
rw [MonoidHom.mem_ker, MonoidHom.restrict_apply, transferFocal_eq_pow]

Premises used: MonoidHom.mem_ker, MonoidHom.restrict_apply, Subgroup.transferFocal_eq_pow
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
g : ↥P
hQ : IsPGroup.{u_1} p (↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
⊢ HPow.hPow (α := ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf)
        (↑g : ↥(↑P : Subgroup G) ⧸ (↑P : Subgroup G).focalSubgroupOf) (↑P : Subgroup G).index =
      1 ↔
    g ∈ (↑P : Subgroup G).focalSubgroupOf

Tactic:
simpa using (hQ.powEquiv' P.not_dvd_index).apply_eq_iff_eq (x := g) (y := 1)

Premises used: IsPGroup.powEquiv', Sylow.not_dvd_index, Equiv.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
rw :
  map (↑P : Subgroup G).subtype (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict (↑P : Subgroup G))) =
    map (↑P : Subgroup G).subtype (↑P : Subgroup G).focalSubgroupOf
⊢ (↑P : Subgroup G).transferFocal.ker ⊓ (↑P : Subgroup G) = (↑P : Subgroup G).focalSubgroup

Tactic:
rw [← subgroupOf_map_subtype, ← MonoidHom.ker_restrict, ← map_focalSubgroupOf]

Premises used: Subgroup.map_focalSubgroupOf, Subgroup.subgroupOf_map_subtype, MonoidHom.ker_restrict
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ map (↑P : Subgroup G).subtype (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict (↑P : Subgroup G))) =
    map (↑P : Subgroup G).subtype (↑P : Subgroup G).focalSubgroupOf

Tactic:
congr_arg _ (ker_restrict_transferFocal_eq_focalSubgroupOf P)

Premises used: congr_arg, Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ map (↑P : Subgroup G).subtype (MonoidHom.ker ((↑P : Subgroup G).transferFocal.restrict (↑P : Subgroup G))) =
    map (↑P : Subgroup G).subtype (↑P : Subgroup G).focalSubgroupOf

Tactic:
exact congr_arg _ (ker_restrict_transferFocal_eq_focalSubgroupOf P)

Premises used: congr_arg, Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
a : _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).focalSubgroup
a₁ : (↑P : Subgroup G).focalSubgroup ≤ _root_.commutator G ⊓ (↑P : Subgroup G)
⊢ _root_.commutator G ⊓ (↑P : Subgroup G) = (↑P : Subgroup G).focalSubgroup

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
apply : _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).transferFocal.ker ⊓ (↑P : Subgroup G)
⊢ _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).focalSubgroup

Tactic:
apply le_trans ?_ (ker_transferFocal_inf_eq_focalSubgroup P).le

Premises used: Eq.le, Subgroup.ker_transferFocal_inf_eq_focalSubgroup, le_trans
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).transferFocal.ker ⊓ (↑P : Subgroup G)

Tactic:
inf_le_inf_right _ (Abelianization.commutator_subset_ker P.transferFocal)

Premises used: Sylow.toSubgroup, Set.Mem, inf_le_inf_right, Subgroup.transferFocal, Abelianization.commutator_subset_ker
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ _root_.commutator G ⊓ (↑P : Subgroup G) ≤ (↑P : Subgroup G).transferFocal.ker ⊓ (↑P : Subgroup G)

Tactic:
exact inf_le_inf_right _ (Abelianization.commutator_subset_ker P.transferFocal)

Premises used: Sylow.toSubgroup, inf_le_inf_right, Subgroup.transferFocal, Abelianization.commutator_subset_ker
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ (↑P : Subgroup G).focalSubgroup ≤ _root_.commutator G ⊓ (↑P : Subgroup G)

Tactic:
le_inf P.focalSubgroup_le_commutator P.focalSubgroup_le

Premises used: Sylow.toSubgroup, Set.Mem, le_inf, Subgroup.focalSubgroup_le_commutator, Subgroup.focalSubgroup_le
-- Module: Mathlib.GroupTheory.Focal
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ (↑P : Subgroup G).focalSubgroup ≤ _root_.commutator G ⊓ (↑P : Subgroup G)

Tactic:
exact le_inf P.focalSubgroup_le_commutator P.focalSubgroup_le

Premises used: Sylow.toSubgroup, le_inf, Subgroup.focalSubgroup_le_commutator, Subgroup.focalSubgroup_le
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
h : IsCoatom K
⊢ frattini G ≤ K

Tactic:
Order.radical_le_coatom h

Premises used: Set.Mem, setOf, Order.radical_le_coatom
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
simp_rw :
  ∀ (i : Subgroup H) (i_1 : Membership.mem (γ := Set (Subgroup H)) {H_1 : Subgroup H | IsCoatom H_1} i),
    ⨅ (a : Subgroup G), ⨅ (_ : Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} a), a ≤ comap φ i
⊢ frattini G ≤ comap φ (frattini H)

Tactic:
simp_rw [frattini, Order.radical, comap_iInf, le_iInf_iff]

Premises used: Order.radical, le_iInf_iff, frattini, Subgroup.comap_iInf
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : Membership.mem (γ := Set (Subgroup H)) {H_1 : Subgroup H | IsCoatom H_1} M
hi : Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} (comap φ M)
⊢ ⨅ (a : Subgroup G), ⨅ (_ : Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} a), a ≤ comap φ M

Tactic:
apply biInf_le

Premises used: biInf_le
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : Membership.mem (γ := Set (Subgroup H)) {H_1 : Subgroup H | IsCoatom H_1} M
⊢ Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} (comap φ M)

Tactic:
isCoatom_comap_of_surjective hφ hM

Premises used: Set.Mem, Subgroup.isCoatom_comap_of_surjective, setOf, IsCoatom
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : Membership.mem (γ := Set (Subgroup H)) {H_1 : Subgroup H | IsCoatom H_1} M
⊢ Membership.mem (γ := Set (Subgroup G)) {H : Subgroup G | IsCoatom H} (comap φ M)

Tactic:
exact isCoatom_comap_of_surjective hφ hM

Premises used: Subgroup.isCoatom_comap_of_surjective
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ : G →* H
rw : ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom (frattini G) = frattini G
⊢ Characteristic (frattini G)

Tactic:
rw [characteristic_iff_comap_eq]

Premises used: Subgroup.characteristic_iff_comap_eq
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
φ_1 : G →* H
φ : G ≃* G
⊢ comap φ.toMonoidHom (frattini G) = frattini G

Tactic:
apply φ.comapSubgroup.map_radical

Premises used: OrderIso.map_radical, MulEquiv.comapSubgroup
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
inst : Group G
inst_1 : IsCoatomic.{u_1} (Subgroup G)
K : Subgroup G
h : K ⊔ frattini G = ⊤
⊢ K = ⊤

Tactic:
Order.radical_nongenerating h

Premises used: Order.radical_nongenerating
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ Group.IsNilpotent.{u_1} ↥(frattini G) ↔
    ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p ↥(frattini G)), (↑P : Subgroup ↥(frattini G)).Normal

Tactic:
have q := (Group.isNilpotent_of_finite_tfae (G := frattini G)).out 0 3
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
q :
  Group.IsNilpotent.{u_1} ↥(frattini G) ↔
    ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p ↥(frattini G)), (↑P : Subgroup ↥(frattini G)).Normal
rw : ∀ (p : ℕ) (_hp : Fact (Nat.Prime p)) (P : Sylow p ↥(frattini G)), (↑P : Subgroup ↥(frattini G)).Normal
⊢ Group.IsNilpotent.{u_1} ↥(frattini G)

Tactic:
rw [q]
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
⊢ Eq (α := Subgroup G)
    (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G) ⊔ frattini G) ⊤

Tactic:
have frattini_argument := Sylow.normalizer_sup_eq_top P
-- Module: Mathlib.GroupTheory.Frattini
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument :
  Eq (α := Subgroup G)
    (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G) ⊔ frattini G) ⊤
⊢ Eq (α := Subgroup G) (normalizer (↑(map (Subgroup.subtype (frattini G)) (↑P : Subgroup ↥(frattini G))) : Set G)) ⊤

Tactic:
have normalizer_P := frattini_nongenerating frattini_argument