awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
have have₁ have₂ :
  ∀
    (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)),
    ∃ (g : G), g • P = Q
have₃ :
  ∀
    (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)),
    Set.Nonempty.{u_1} (α := (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1))
hpα :
  ∀
    (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)),
    ¬p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
hpα₁ :
  ∀
    (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))
    (h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)), 1 ≡ 0 [MOD p]
⊢ ∃ (g : G), g • P = Q
have hpα₂ : ∀
  (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))
  (h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)),
  1 = Nat.card.{u_1} (↑(fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) : Type u_1)
Tactic: classical
      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⟩
      suffices Set.Nonempty (fixedPoints Q (orbit G P)) by
        exact Exists.elim this fun R hR => by
          rw [← Sylow.ext (H.mp hR)]
          exact R.2
      apply Q.2.nonempty_fixed_point_of_prime_not_dvd_card
      refine fun h => hp.out.not_dvd_one (Nat.modEq_zero_iff_dvd.mp ?_)
      calc
        1 = Nat.card (fixedPoints P (orbit G P)) := ?_
        _ ≡ Nat.card (orbit G P) [MOD p] := (P.2.card_modEq_card_fixedPoints (orbit G P)).symm
        _ ≡ 0 [MOD p] := Nat.modEq_zero_iff_dvd.mpr h
      rw [← Nat.card_unique (α := ({⟨P, mem_orbit_self P⟩} : Set (orbit G P))), eq_comm]
      congr
      rw [Set.eq_singleton_iff_unique_mem]
      exact ⟨H.mpr rfl, fun R h => Subtype.ext (Sylow.ext (H.mp h))⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
⊢ Nat.card.{u_1} (Sylow p G) ≡ 1 [MOD p]
have refine : ∀ (P : Sylow p G), Nat.card.{u_1} (Sylow p G) ≡ 1 [MOD p]
Tactic: refine Sylow.nonempty.elim fun P : Sylow p G => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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) ≡ 1 [MOD p]
have this : Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}
Tactic: have : fixedPoints P.1 (Sylow p G) = {P} :=
    Set.ext fun Q : Sylow p G =>
      calc
        Q ∈ fixedPoints P (Sylow p G) ↔ P.1 ≤ Q := P.2.sylow_mem_fixedPoints_iff
        _ ↔ Q.1 = P.1 := ⟨P.3 Q.2, ge_of_eq⟩
        _ ↔ Q ∈ {P} := Sylow.ext_iff.symm.trans Set.mem_singleton_iff.symm
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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
this : Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}
⊢ Nat.card.{u_1} (Sylow p G) ≡ 1 [MOD p]
have this₁ : Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) = 1
Tactic: have : Nat.card (fixedPoints P.1 (Sylow p G)) = 1 := by simp [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
this_1 : Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}
this : Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) = 1
⊢ Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) ≡ 1 [MOD p]
have rw : 1 ≡ 1 [MOD p]
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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 Q : Sylow p G
⊢ ↥(↑P : Subgroup G) ≃* ↥(↑Q : Subgroup G)
have rw : ↥(↑P : Subgroup G) ≃* ↥(↑(Classical.choose (p := fun (x : G) ↦ x • P = Q) sorry • P) : Subgroup G)
Tactic: rw [← Classical.choose_spec (exists_smul_eq G P Q)]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
⊢ Eq (α := Subgroup G) (stabilizer G P) (normalizer (↑P : Set G))
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (stabilizer G P) x ↔ Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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)
⊢ (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
have rwa : LE.le (α := Subgroup G) (zpowers x) (centralizer (↑(↑P : Subgroup G) : Set G))
Tactic: rwa [le_centralizer_iff, zpowers_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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)
rwa : LE.le (α := Subgroup G) (zpowers x) (centralizer (↑(↑P : Subgroup G) : Set G))
⊢ (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
have rwa₁ : Membership.mem (γ := Subgroup G) (centralizer (↑(↑P : Subgroup G) : Set G)) x
Tactic: rwa [le_centralizer_iff, zpowers_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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)
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n
have h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
Tactic: have h1 : P ≤ centralizer (zpowers x : Set G) := by rwa [le_centralizer_iff, zpowers_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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)
⊢ (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
have rw : Membership.mem (γ := Subgroup G) (centralizer (↑(↑(g • P) : Subgroup G) : Set G)) x
Tactic: rw [le_centralizer_iff, zpowers_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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)
z : G
hz : z ∈ (↑(↑P : Subgroup G) : Set G)
⊢ HMul.hMul (α := 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)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
have hy₁ : z * (g⁻¹ * x * g) = g⁻¹ * x * g * z
Tactic: specialize hy z hz
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
z : G
hz : z ∈ (↑(↑P : Subgroup G) : Set G)
hy : z * (g⁻¹ * x * g) = g⁻¹ * x * g * z
⊢ HMul.hMul (α := 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)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
have rwa : ∀ (hy : z * (g⁻¹ * x) * g = g⁻¹ * x * g * z),
  HMul.hMul (α := 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)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
Tactic: rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
z : G
hz : z ∈ (↑(↑P : Subgroup G) : Set G)
hy : z * (g⁻¹ * x * g) = g⁻¹ * x * g * z
rwa :
  ∀ (hy : z * (g⁻¹ * x) * g = g⁻¹ * x * g * z),
    HMul.hMul (α := 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)
            z :
          G)
        x =
      HMul.hMul (β := G) x
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
⊢ HMul.hMul (α := 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)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
have rwa₁ : ∀ (hy : z * (g⁻¹ * x) = g⁻¹ * x * g * z * g⁻¹),
  HMul.hMul (α := 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)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
Tactic: rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
z : G
hz : z ∈ (↑(↑P : Subgroup G) : Set G)
hy : z * (g⁻¹ * x * g) = g⁻¹ * x * g * z
rwa :
  ∀ (hy : z * (g⁻¹ * x) * g = g⁻¹ * x * g * z),
    HMul.hMul (α := 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)
            z :
          G)
        x =
      HMul.hMul (β := G) x
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
rwa₁ :
  ∀ (hy : z * (g⁻¹ * x) = g⁻¹ * x * g * z * g⁻¹),
    HMul.hMul (α := 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)
            z :
          G)
        x =
      HMul.hMul (β := G) x
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
⊢ HMul.hMul (α := 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)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
have rwa₂ : ∀ (hy : z * (g⁻¹ * x) = g⁻¹ * x * g * (z * g⁻¹)),
  HMul.hMul (α := 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)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
Tactic: rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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)
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n
have h2 : (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
Tactic: have h2 : ↑(g • P) ≤ centralizer (zpowers x : Set G) := by
    rw [le_centralizer_iff, zpowers_le]
    rintro - ⟨z, hz, rfl⟩
    specialize hy z hz
    rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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)
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n
have obtain : ∀ (h : ↥(centralizer (↑(zpowers x) : Set G))) (hh : h • (g • P).subtype h2 = P.subtype h1),
  ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n
Tactic: obtain ⟨h, hh⟩ :=
    exists_smul_eq (centralizer (zpowers x : Set G)) ((g • P).subtype h2) (P.subtype h1)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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 • P).subtype h2 = P.subtype h1
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n
have hh₁ : (((↑h : G) * g) • P).subtype sorry = P.subtype h1
Tactic: simp_rw [smul_subtype, Subgroup.smul_def, smul_smul] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n
have refine : g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * ((↑h : G) * g)
Tactic: refine ⟨h * g, smul_eq_iff_mem_normalizer.mp (subtype_injective hh), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
⊢ g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * ((↑h : G) * g)
have rw : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
⊢ g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * ((↑h : G) * g)
have rw₁ : g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * (↑h : G) * x * g
Tactic: rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
⊢ g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * ((↑h : G) * g)
have rw₂ : g⁻¹ * x * g = g⁻¹ * (↑h : G)⁻¹ * (↑h : G) * x * g
Tactic: rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
⊢ g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * ((↑h : G) * g)
have rw₃ : g⁻¹ * x * g = g⁻¹ * x * g
Tactic: rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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
⊢ HasQuotient.Quotient G (B := Subgroup G) (stabilizer G P) ≃
    HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G))
have rw : HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G)) ≃
  HasQuotient.Quotient G (B := Subgroup G) (normalizer (↑P : Set G))
Tactic: rw [P.stabilizer_eq_normalizer]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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
⊢ False
have h₁ : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
Tactic: rw [P.index_eq_card] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
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))
⊢ False
have obtain : ∀ (x : G ⧸ (↑P : Subgroup G)) (hx : orderOf x = p), False
Tactic: obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card' (G := G ⧸ (P : Subgroup G)) p h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
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
⊢ False
have h₁ : IsPGroup.{u_1} p ↥(zpowers x)
Tactic: have h := IsPGroup.of_card (((Nat.card_zpowers x).trans hx).trans (pow_one p).symm)