awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this : Fact (Nat.Prime p)
⊢ ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n
have this₁ : Finite G
Tactic: have : Finite G := Nat.finite_of_card_ne_zero <| by linarith [Nat.one_le_pow n p hp.pos]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this_1 : Fact (Nat.Prime p)
this : Finite G
⊢ ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n
have obtain : ∀ (m : ℕ) (hm : Nat.card G = p ^ m), ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n
Tactic: obtain ⟨m, hm⟩ := h.exists_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this_1 : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ ∃ (H : Subgroup G), Nat.card.{u} ↥H = p ^ n
have refine : p ^ n ∣ Nat.card G
Tactic: refine exists_subgroup_card_pow_prime _ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this_1 : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ Nat.card G
have rw : ∀ (hn : p ^ n ≤ p ^ m) (hm : Nat.card G = p ^ m), p ^ n ∣ p ^ m
Tactic: rw [hm] at hn ⊢
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' = p ^ n
have obtain : ∀ (H' : Subgroup ↥H) (H'card : Nat.card.{u} ↥H' = p ^ n), ∃ H' ≤ H, Nat.card.{u} ↥H' = p ^ n
Tactic: obtain ⟨H', H'card⟩ := exists_subgroup_card_pow_prime_of_le_card hp (h.to_subgroup H) hn
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
H' : Subgroup ↥H
H'card : Nat.card.{u} ↥H' = p ^ n
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' = p ^ n
have refine : Nat.card.{u} ↥(Subgroup.map H.subtype H') = p ^ n
Tactic: refine ⟨H'.map H.subtype, map_subtype_le _, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card.{u} ↥H
H' : Subgroup ↥H
H'card : Nat.card.{u} ↥H' = p ^ n
⊢ Nat.card.{u} ↥(Subgroup.map H.subtype H') = p ^ n
have rw : Nat.card.{u} ↥(Subgroup.map H.subtype H') = Nat.card.{u} ↥H'
Tactic: rw [← H'card]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
have obtain : ∀ (m : ℕ) (hmk : p ^ m ≤ k) (hkm : k < p ^ (m + 1)), ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
Tactic: obtain ⟨m, hmk, hkm⟩ : ∃ s, p ^ s ≤ k ∧ k < p ^ (s + 1) :=
    exists_nat_pow_near (Nat.one_le_iff_ne_zero.2 hk₀) hp.one_lt
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
have obtain : ∀ (H' : Subgroup G) (H'H : H' ≤ H) (H'card : Nat.card.{u} ↥H' = p ^ m),
  ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
Tactic: obtain ⟨H', H'H, H'card⟩ := exists_subgroup_le_card_pow_prime_of_le_card hp h (hmk.trans hk)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card.{u} ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card.{u} ↥H' = p ^ m
⊢ ∃ H' ≤ H, Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
have refine : Nat.card.{u} ↥H' ≤ k ∧ k < p * Nat.card.{u} ↥H'
Tactic: refine ⟨H', H'H, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ n ∣ Nat.card G
⊢ p ^ n ∣ Nat.card.{u} ↥(↑P : Subgroup G)
have hdvd₁ : p ^ n ∣ (↑P : Subgroup G).index * Nat.card.{u} ↥(↑P : Subgroup G)
Tactic: rw [← index_mul_card P.1] at hdvd
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
have hdvd₁ : HPow.hPow (β := ℕ) p 1 ∣ Nat.card G
Tactic: rw [← pow_one p] at hdvd
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Sylow p G
hdvd : HPow.hPow (β := ℕ) p 1 ∣ Nat.card G
⊢ p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
have key : HPow.hPow (β := ℕ) p 1 ∣ Nat.card.{u} ↥(↑P : Subgroup G)
Tactic: have key := P.pow_dvd_card_of_pow_dvd_card hdvd
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
inst_2 : Fact (Nat.Prime p)
P : Sylow p G
hdvd : HPow.hPow (β := ℕ) p 1 ∣ Nat.card G
key : HPow.hPow (β := ℕ) p 1 ∣ Nat.card.{u} ↥(↑P : Subgroup G)
⊢ p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
have rwa : ∀ (key : p ∣ Nat.card.{u} ↥(↑P : Subgroup G)), p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
Tactic: rwa [pow_one] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ (↑P : Subgroup G) ≠ ⊥
have refine : ∀ (h : (↑P : Subgroup G) = ⊥), p ∣ 1
Tactic: refine fun h => hp.out.not_dvd_one ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : (↑P : Subgroup G) = ⊥
⊢ p ∣ 1
have key : p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
Tactic: have key : p ∣ Nat.card P := P.dvd_card_of_dvd_card hdvd
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : (↑P : Subgroup G) = ⊥
key : p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
⊢ p ∣ 1
have rwa : ∀ (key : p ∣ Nat.card.{u} ↥⊥), p ∣ 1
Tactic: rwa [h, card_bot] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : (↑P : Subgroup G) = ⊥
key : p ∣ Nat.card.{u} ↥(↑P : Subgroup G)
rwa : ∀ (key : p ∣ Nat.card.{u} ↥⊥), p ∣ 1
⊢ p ∣ 1
have rwa₁ : ∀ (key : p ∣ 1), p ∣ 1
Tactic: rwa [h, card_bot] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
⊢ Nat.card.{u} ↥(↑P : Subgroup G) = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
have obtain : ∀ (n : ℕ) (heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n),
  Nat.card.{u} ↥(↑P : Subgroup G) = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: obtain ⟨n, heq : Nat.card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n
⊢ Nat.card.{u} ↥(↑P : Subgroup G) = HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
have refine : Nat.card.{u} ↥(↑P : Subgroup G) ∣ HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine Nat.dvd_antisymm ?_ (P.pow_dvd_card_of_pow_dvd_card (Nat.ordProj_dvd _ p))
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Nat.card.{u} ↥(↑P : Subgroup G) = p ^ n
⊢ Nat.card.{u} ↥(↑P : Subgroup G) ∣ HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : Nat.card.{u} ↥(↑P : Subgroup G) ∣ Nat.card G
Tactic: rw [heq, ← hp.out.pow_dvd_iff_dvd_ordProj (show Nat.card G ≠ 0 from Nat.card_pos.ne'), ← heq]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
⊢ Unique (Sylow p G)
have refine : ∀ (Q : Sylow p G), Q = default
Tactic: refine { uniq := fun Q ↦ ?_ }
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
⊢ Q = default
have obtain : ∀ (x : G) (h1 : x • P = Q), Q = default
Tactic: obtain ⟨x, h1⟩ := exists_smul_eq G P Q
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
x : G
h1 : x • P = Q
⊢ Q = default
have obtain : ∀ (x : G) (h2 : x • P = default), Q = default
Tactic: obtain ⟨x, h2⟩ := exists_smul_eq G P default
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
x_1 : G
h1 : x_1 • P = Q
x : G
h2 : x • P = default
⊢ Q = default
have rw : ∀ (h1 : P = Q) (x : G) (h2 : P = default), Q = default
Tactic: rw [smul_eq_of_normal] at h1 h2
Cleared hypotheses: h1, x, h2
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
Q : Sylow p G
x_1 : G
h1 : P = Q
x : G
h2 rw : P = default
⊢ Q = default
have rw₁ : P = P
Tactic: rw [← h1, ← h2]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
⊢ (↑P : Subgroup G).Characteristic
have refine : ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
Tactic: refine Subgroup.characteristic_iff_map_eq.mpr fun ϕ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
⊢ Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
have h : ϕ • (↑P : Subgroup G) =
  Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)
Tactic: have h := Subgroup.pointwise_smul_def (a := ϕ) (P : Subgroup G)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h :
  ϕ • (↑P : Subgroup G) =
    Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)
⊢ Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
have rwa : ∀
  (h :
    (↑(ϕ • P) : Subgroup G) =
      Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)),
  Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
Tactic: rwa [← pointwise_smul_def, Subsingleton.elim (ϕ • P) P, eq_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h :
  ϕ • (↑P : Subgroup G) =
    Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)
rwa :
  ∀
    (h :
      (↑(ϕ • P) : Subgroup G) =
        Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)),
    Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
⊢ Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
have rwa₁ : ∀
  (h :
    (↑P : Subgroup G) =
      Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)),
  Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
Tactic: rwa [← pointwise_smul_def, Subsingleton.elim (ϕ • P) P, eq_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Subsingleton.{u + 1} (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h :
  ϕ • (↑P : Subgroup G) =
    Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)
rwa :
  ∀
    (h :
      (↑(ϕ • P) : Subgroup G) =
        Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)),
    Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
rwa₁ :
  ∀
    (h :
      (↑P : Subgroup G) =
        Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G)),
    Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
⊢ Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
have rwa₂ : ∀
  (h :
    Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G : (a : G ≃* G) → Monoid.End G) ϕ) (↑P : Subgroup G) =
      (↑P : Subgroup G)),
  Subgroup.map ϕ.toMonoidHom (↑P : Subgroup G) = (↑P : Subgroup G)
Tactic: rwa [← pointwise_smul_def, Subsingleton.elim (ϕ • P) P, eq_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
h : (↑P : Subgroup G).Normal
⊢ (↑P : Subgroup G).Characteristic
have have : ∀ (x : Unique (Sylow p G)), (↑P : Subgroup G).Characteristic
Tactic: have _ := unique_of_normal P h
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
⊢ Eq (α := Subgroup G) (normalizer (↑(normalizer (↑P : Set G)) : Set G)) (normalizer (↑P : Set G))
have this : ∀ (hn : Normal (normalizer (↑(P.subtype sorry) : Set ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))))),
  (↑(P.subtype sorry) : Subgroup ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))).Normal
Tactic: have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
this :
  ∀
    (hn :
      Normal (normalizer (↑(P.subtype ⋯) : Set ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))))),
    (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))).Normal
⊢ Eq (α := Subgroup G) (normalizer (↑(normalizer (↑P : Set G)) : Set G)) (normalizer (↑P : Set G))
have this₁ : ∀
  (hn :
    Normal (G := ↥(normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))
      (subgroupOf (normalizer (↑(↑P : Subgroup G) : Set G))
        (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G)))),
  LE.le (α := Subgroup G) (normalizer (↑(normalizer (↑(↑P : Subgroup G) : Set G)) : Set G))
    (normalizer (↑(↑P : Subgroup G) : Set G))
Tactic: rw [← (P.subtype _).coe_coe, coe_subtype,
    normal_subgroupOf_iff_le_normalizer (le_normalizer.trans le_normalizer),
    ← subgroupOf_normalizer_eq (le_normalizer.trans le_normalizer)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
have inl : ∀ (heq : Eq (α := Subgroup G) (normalizer (↑P : Set G)) ⊤),
  Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
Tactic: rcases eq_top_or_exists_le_coatom (normalizer (P : Set G))
        with (heq | ⟨K, hK, hNK⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
inl :
  ∀ (heq : Eq (α := Subgroup G) (normalizer (↑P : Set G)) ⊤),
    Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
have inr : ∀ (K : Subgroup G) (hK : IsCoatom K) (hNK : normalizer (↑P : Set G) ≤ K),
  Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
Tactic: rcases eq_top_or_exists_le_coatom (normalizer (P : Set G))
        with (heq | ⟨K, hK, hNK⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
have this : K.Normal
Tactic: haveI := hnc _ hK
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
have hPK : (↑P : Subgroup G) ≤ K
Tactic: have hPK : P ≤ K := le_trans le_normalizer hNK
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
hPK : (↑P : Subgroup G) ≤ K
⊢ Eq (α := Subgroup G) (normalizer (↑(↑P : Subgroup G) : Set G)) ⊤
have inr : K = ⊤
Tactic: refine (hK.1 ?_).elim
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
hPK : (↑P : Subgroup G) ≤ K
⊢ K = ⊤
have inr : normalizer (↑P : Set G) ⊔ K = ⊤
Tactic: rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : Finite.{u + 1} (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer (↑P : Set G) ≤ K
this : K.Normal
hPK : (↑P : Subgroup G) ≤ K
inr : normalizer (↑P : Set G) ⊔ K = ⊤
⊢ K = ⊤
have inr₁ : Eq.{u + 1} (α := Subgroup G) ⊤ ⊤
Tactic: rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
⊢ ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
have have : (this : Fintype G) → ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
Tactic: have := Fintype.ofFinite G
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
have have : (this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)) → ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
Tactic: have : ∀ p, Fintype (P p) := fun p ↦ Fintype.ofFinite (P p)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
⊢ ∀ (x y : G),
    Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ) G)
        (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) x →
      Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ) G)
          (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) y →
        Commute x y
have hp₁' : Fact (Nat.Prime p₁)
Tactic: haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
⊢ ∀ (x y : G),
    Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ) G)
        (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) x →
      Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ) G)
          (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) y →
        Commute x y
have hp₂' : Fact (Nat.Prime p₂)
Tactic: haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ ∀ (x y : G),
    Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ) G)
        (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) x →
      Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ) G)
          (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) y →
        Commute x y
have hne' : p₁ ≠ p₂
Tactic: have hne' : p₁ ≠ p₂ := by simpa using hne
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ ∀ (x y : G),
    Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ) G)
        (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) x →
      Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ) G)
          (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) y →
        Commute x y
have apply : _root_.Disjoint (↑(P p₁) : Subgroup G) (↑(P p₂) : Subgroup G)
Tactic: apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))