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)
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ IsPGroup.{u_1} p ↥Q
have hϕ : IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' (↑P : Subgroup G)))
Tactic: apply h.comap_of_ker_isPGroup
-- 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_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ IsPGroup.{u_1} p ↥(MonoidHom.ker (QuotientGroup.mk' (↑P : Subgroup G)))
have hϕ : IsPGroup.{u_1} p ↥(↑P : Subgroup G)
Tactic: rw [QuotientGroup.ker_mk']
-- 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_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
⊢ False
have hQ : IsPGroup.{u_1} p ↥Q
Tactic: have hQ : IsPGroup p Q := by
    apply h.comap_of_ker_isPGroup
    rw [QuotientGroup.ker_mk']
    exact P.2
-- 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_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hQ : IsPGroup.{u_1} p ↥Q
⊢ False
have hp₁ : ¬x = 1
Tactic: replace hp := mt orderOf_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
inst_1 : (↑P : Subgroup G).Normal
inst_2 : (↑P : Subgroup G).FiniteIndex
h_1 : p ∣ Nat.card.{u_1} (G ⧸ (↑P : Subgroup G))
x : G ⧸ (↑P : Subgroup G)
hx : orderOf x = p
h : IsPGroup.{u_1} p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
hQ : IsPGroup.{u_1} p ↥Q
hp : ¬x = 1
⊢ False
have hp₁ : (↑P : Subgroup G) < comap (QuotientGroup.mk' (↑P : Subgroup G)) (zpowers x)
Tactic: rw [← zpowers_eq_bot, ← Ne, ← bot_lt_iff_ne_bot, ←
    comap_lt_comap_of_surjective (QuotientGroup.mk'_surjective _), MonoidHom.comap_bot,
    QuotientGroup.ker_mk'] at hp
Cleared hypotheses: hp
-- 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 : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
⊢ ¬p ∣ (↑P : Subgroup G).index
have rw : ¬p ∣ (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) * Nat.card.{u_1} (Sylow p G)
Tactic: rw [← relIndex_mul_index le_normalizer, P.coe_coe, ← card_eq_index_normalizer]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
⊢ ¬p ∣ (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) * Nat.card.{u_1} (Sylow p G)
have this : (↑(P.subtype sorry) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal
Tactic: haveI : (P.subtype le_normalizer).Normal :=
    Subgroup.normal_in_normalizer
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
this : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal
⊢ ¬p ∣ (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) * Nat.card.{u_1} (Sylow p G)
have this₁ : (↑(P.subtype sorry) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).FiniteIndex
Tactic: haveI : (P.subtype le_normalizer).FiniteIndex := ⟨hP⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
hP : (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) ≠ 0
this_1 : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).Normal
this : (↑(P.subtype ⋯) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).FiniteIndex
⊢ ¬p ∣ (↑P : Subgroup G).relIndex (normalizer (↑P : Set G)) * Nat.card.{u_1} (Sylow p G)
have hP₁ : ¬p ∣ (↑(P.subtype sorry) : Subgroup ↥(normalizer (↑(↑P : Subgroup G) : Set G))).index
Tactic: replace hP := not_dvd_index_aux (P.subtype le_normalizer)
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
P : Sylow p G
inst_2 : (↑P : Subgroup G).FiniteIndex
⊢ ¬p ∣ (↑P : Subgroup G).index
have this : Finite.{u_1 + 1} (Sylow p G)
Tactic: have := P.finite_of_finiteIndex
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
⊢ Function.Surjective (α := Sylow p G) (mapSurjective hf)
have this : Finite G'
Tactic: have : Finite G' := Finite.of_surjective f hf
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
⊢ ∃ (a : Sylow p G), mapSurjective hf a = P
have hPQ : map f Q ≤ (↑P : Subgroup G')
Tactic: have hPQ : Q.map f ≤ P := Subgroup.map_le_iff_le_comap.mpr (Subgroup.map_subtype_le Q₀.1)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
⊢ ∃ (a : Sylow p G), mapSurjective hf a = P
have hpQ : IsPGroup.{u_1} p ↥Q
Tactic: have hpQ : IsPGroup p Q := Q₀.2.map (P.comap f).subtype
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
⊢ ¬p ∣ Q.index
have rw : ¬p ∣ (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G'))).index * (↑P : Subgroup G').index
Tactic: rw [Subgroup.index_map_subtype Q₀.1, P.index_comap_of_surjective hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
⊢ ∃ (a : Sylow p G), mapSurjective hf a = P
have hQ : ¬p ∣ Q.index
Tactic: have hQ : ¬ p ∣ Q.index := by
    rw [Subgroup.index_map_subtype Q₀.1, P.index_comap_of_surjective hf]
    exact Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
hQ : ¬p ∣ Q.index
⊢ ∃ (a : Sylow p G), mapSurjective hf a = P
have h : mapSurjective hf (hpQ.toSylow hQ) = P
Tactic: use hpQ.toSylow hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
G' : Type u_2
inst_2 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
p : ℕ
inst_3 : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f (↑P : Subgroup G')) := Nonempty.some ⋯
Q : Subgroup G := map (comap f (↑P : Subgroup G')).subtype (↑Q₀ : Subgroup ↥(comap f (↑P : Subgroup G')))
hPQ : map f Q ≤ (↑P : Subgroup G')
hpQ : IsPGroup.{u_1} p ↥Q
hQ : ¬p ∣ Q.index
⊢ mapSurjective hf (hpQ.toSylow hQ) = P
have h : (↑P : Subgroup G') = map f (↑(hpQ.toSylow hQ) : Subgroup G)
Tactic: rw [Sylow.ext_iff, Sylow.coe_mapSurjective, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
⊢ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N = ⊤
have refine : ∀ (g : G), Membership.mem (γ := Subgroup G) ⊤ g → g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N
Tactic: refine top_le_iff.mp fun g _ => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
⊢ g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N
have obtain : ∀ (n : ↥N) (hn : n • HSMul.hSMul (α := MulAut ↥N) ((MulAut.conjNormal : (a : G) → MulAut ↥N) g : MulAut ↥N) P = P),
  g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N
Tactic: obtain ⟨n, hn⟩ := exists_smul_eq N ((MulAut.conjNormal g : MulAut N) • P) P
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
n : ↥N
hn : n • HSMul.hSMul (α := MulAut ↥N) ((MulAut.conjNormal : (a : G) → MulAut ↥N) g : MulAut ↥N) P = P
⊢ g ∈ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G) ⊔ N
have rw : (↑n : G)⁻¹ * ((↑n : G) * g) ∈ N ⊔ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)
Tactic: rw [← inv_mul_cancel_left (↑n) g, sup_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
n : ↥N
hn : n • HSMul.hSMul (α := MulAut ↥N) ((MulAut.conjNormal : (a : G) → MulAut ↥N) g : MulAut ↥N) P = P
⊢ (↑n : G)⁻¹ * ((↑n : G) * g) ∈ N ⊔ normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)
have apply : Membership.mem (γ := Subgroup G) (normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)) ((↑n : G) * g)
Tactic: apply mul_mem_sup (N.inv_mem n.2)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
n : ↥N
hn : n • HSMul.hSMul (α := MulAut ↥N) ((MulAut.conjNormal : (a : G) → MulAut ↥N) g : MulAut ↥N) P = P
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)) ((↑n : G) * g)
have hn₁ : map
    ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
      ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
    (↑P : Subgroup ↥N) =
  (↑P : Subgroup ↥N)
Tactic: rw [smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← MulAut.conjNormal.map_mul,
    Sylow.ext_iff, pointwise_smul_def, Subgroup.pointwise_smul_def] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
n : ↥N
hn :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)) ((↑n : G) * g)
have this : Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
  (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)
Tactic: have : Function.Injective (MulAut.conj (n * g)).toMonoidHom := (MulAut.conj (n * g)).injective
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
n : ↥N
hn :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
this :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
    (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)) ((↑n : G) * g)
have refine : ∀ (x : G),
  Membership.mem (α := G) (γ := Subgroup G)
      (map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)))
        (map N.subtype (↑P : Subgroup ↥N)))
      ((MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)) : (a : G) → G) x : G) ↔
    (↑n : G) * g * x * ((↑n : G) * g)⁻¹ ∈ (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)
Tactic: refine fun x ↦ (mem_map_iff_mem this).symm.trans ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p ↥N
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
n : ↥N
hn :
  map
      ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
        ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g)))
      (↑P : Subgroup ↥N) =
    (↑P : Subgroup ↥N)
this :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := G) (β := G)
    (⇑(MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) : (a : G) → G)
x : G
⊢ Membership.mem (α := G) (γ := Subgroup G)
      (map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)))
        (map N.subtype (↑P : Subgroup ↥N)))
      ((MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)) : (a : G) → G) x : G) ↔
    (↑n : G) * g * x * ((↑n : G) * g)⁻¹ ∈ (↑(map N.subtype (↑P : Subgroup ↥N)) : Set G)
have rw : Membership.mem (α := G) (γ := Subgroup G)
    (map (MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g))) N.subtype)
      (↑P : Subgroup ↥N))
    ((MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((↑n : G) * g)) : (a : G) → G) x : G) ↔
  (↑n : G) * g * x * ((↑n : G) * g)⁻¹ ∈
    (↑(map
          (N.subtype.comp
            ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N : (a : MulAut ↥N) → Monoid.End ↥N)
              ((MulAut.conjNormal : (a : G) → MulAut ↥N) ((↑n : G) * g))))
          (↑P : Subgroup ↥N)) :
      Set G)
Tactic: rw [map_map, ← congr_arg (map N.subtype) hn, map_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p G
hP : (↑P : Subgroup G) ≤ N
⊢ normalizer (↑P : Set G) ⊔ N = ⊤
have rw : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype (↑(P.subtype hP) : Subgroup ↥N)) : Set G) ⊔ N
Tactic: rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
    inf_of_le_left hP, P.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p G
hP : (↑P : Subgroup G) ≤ N
rw : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype (↑(P.subtype hP) : Subgroup ↥N)) : Set G) ⊔ N
⊢ normalizer (↑P : Set G) ⊔ N = ⊤
have rw₁ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype ((↑P : Subgroup G).subgroupOf N)) : Set G) ⊔ N
Tactic: rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
    inf_of_le_left hP, P.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p G
hP : (↑P : Subgroup G) ≤ N
rw : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype (↑(P.subtype hP) : Subgroup ↥N)) : Set G) ⊔ N
rw₁ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype ((↑P : Subgroup G).subgroupOf N)) : Set G) ⊔ N
⊢ normalizer (↑P : Set G) ⊔ N = ⊤
have rw₂ : normalizer (↑P : Set G) ⊔ N = normalizer (↑((↑P : Subgroup G) ⊓ N) : Set G) ⊔ N
Tactic: rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
    inf_of_le_left hP, P.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p G
hP : (↑P : Subgroup G) ≤ N
rw : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype (↑(P.subtype hP) : Subgroup ↥N)) : Set G) ⊔ N
rw₁ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype ((↑P : Subgroup G).subgroupOf N)) : Set G) ⊔ N
rw₂ : normalizer (↑P : Set G) ⊔ N = normalizer (↑((↑P : Subgroup G) ⊓ N) : Set G) ⊔ N
⊢ normalizer (↑P : Set G) ⊔ N = ⊤
have rw₃ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(↑P : Subgroup G) : Set G) ⊔ N
Tactic: rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
    inf_of_le_left hP, P.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
N : Subgroup G
inst_2 : N.Normal
inst_3 : Finite.{u_1 + 1} (Sylow p ↥N)
P : Sylow p G
hP : (↑P : Subgroup G) ≤ N
rw : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype (↑(P.subtype hP) : Subgroup ↥N)) : Set G) ⊔ N
rw₁ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(map N.subtype ((↑P : Subgroup G).subgroupOf N)) : Set G) ⊔ N
rw₂ : normalizer (↑P : Set G) ⊔ N = normalizer (↑((↑P : Subgroup G) ⊓ N) : Set G) ⊔ N
rw₃ : normalizer (↑P : Set G) ⊔ N = normalizer (↑(↑P : Subgroup G) : Set G) ⊔ N
⊢ normalizer (↑P : Set G) ⊔ N = ⊤
have rw₄ : normalizer (↑P : Set G) ⊔ N = normalizer (↑P : Set G) ⊔ N
Tactic: rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
    inf_of_le_left hP, P.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
s : Subgroup G
t : Set (G ⧸ s)
⊢ Nat.card.{u} (↑(mk ⁻¹' t) : Type u) = Nat.card.{u} ↥s * Nat.card.{u} (↑t : Type u)
have rw : Nat.card.{u} (↑(mk ⁻¹' t) : Type u) = Nat.card.{u} (↥s × (↑t : Type u))
Tactic: rw [← Nat.card_prod, Nat.card_congr (preimageMkEquivSubgroupProdSet _ _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
s : Subgroup G
t : Set (G ⧸ s)
rw : Nat.card.{u} (↑(mk ⁻¹' t) : Type u) = Nat.card.{u} (↥s × (↑t : Type u))
⊢ Nat.card.{u} (↑(mk ⁻¹' t) : Type u) = Nat.card.{u} ↥s * Nat.card.{u} (↑t : Type u)
have rw₁ : Nat.card.{u} (↥s × (↑t : Type u)) = Nat.card.{u} (↥s × (↑t : Type u))
Tactic: rw [← Nat.card_prod, Nat.card_congr (preimageMkEquivSubgroupProdSet _ _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : Membership.mem (γ := Set (G ⧸ H)) (MulAction.fixedPoints (↥H) (G ⧸ H)) (↑x : G ⧸ H)
ha : ∀ {y : G ⧸ H}, Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) y → y = (↑x : G ⧸ H)
n : G
hn : n ∈ H
this : (n⁻¹ * x)⁻¹ * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H
have this₁ : x⁻¹ * n * x ∈ H
Tactic: rw [mul_inv_rev, inv_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : Membership.mem (γ := Set (G ⧸ H)) (MulAction.fixedPoints (↥H) (G ⧸ H)) (↑x : G ⧸ H)
ha : ∀ {y : G ⧸ H}, Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) y → y = (↑x : G ⧸ H)
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H
have h : x⁻¹⁻¹ = x
Tactic: convert! this
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : Membership.mem (γ := Set (G ⧸ H)) (MulAction.fixedPoints (↥H) (G ⧸ H)) (↑x : G ⧸ H)
ha : ∀ {y : G ⧸ H}, Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) y → y = (↑x : G ⧸ H)
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹⁻¹ = x
have h : x = x
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y_1 : G ⧸ H
y : G
hy : Membership.mem (γ := Set (G ⧸ H)) (orbit ↥H (↑x : G ⧸ H)) (Quotient.mk'' y)
b : G
hb₁ : b ∈ H
hb₂_1 :
  Eq (α := G ⧸ H)
    ((fun (m : ↥H) ↦ HSMul.hSMul (β := G ⧸ H) m (↑x : G ⧸ H)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) b hb₁))
    (Quotient.mk'' y)
hb₂ : (b * x)⁻¹ * y ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H
have hb₃ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
Tactic: rw [hx] at hb₂
Cleared hypotheses: hb₂
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
H : Subgroup G
inst_1 : Finite.{u + 1} (↑(↑H : Set G) : Type u)
x y : ↥(normalizer (↑H : Set G))
⊢ (leftRel (comap (normalizer H.carrier).subtype H) :
        { x : G // (normalizer H.carrier).carrier.Mem x } → { x : G // (normalizer H.carrier).carrier.Mem x } → Prop)
      x y ↔
    (leftRel H : G → G → Prop) (↑x : G) (↑y : G)
have rw : Membership.mem (γ := Subgroup ↥(normalizer (↑H : Set G))) (comap (Subgroup.subtype (normalizer H.carrier)) H)
    (x⁻¹ * y) ↔
  (↑x : G)⁻¹ * (↑y : G) ∈ H
Tactic: rw [leftRel_apply (α := normalizer (H : Set G)), leftRel_apply]