[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
P Q : Sylow p G
h : ↑P = ↑Q
⊢ P = Q
[PROOFSTEP]
cases P
[GOAL]
case mk
p : ℕ
G : Type u_1
inst✝ : Group G
Q : Sylow p G
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p { x // x ∈ toSubgroup✝ }
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h : ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = ↑Q
⊢ { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = Q
[PROOFSTEP]
cases Q
[GOAL]
case mk.mk
p : ℕ
G : Type u_1
inst✝ : Group G
toSubgroup✝¹ : Subgroup G
isPGroup'✝¹ : IsPGroup p { x // x ∈ toSubgroup✝¹ }
is_maximal'✝¹ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝¹ ≤ Q → Q = toSubgroup✝¹
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p { x // x ∈ toSubgroup✝ }
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h :
  ↑{ toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
⊢ { toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
[PROOFSTEP]
congr
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
h : ↑P ≤ MonoidHom.range ϕ
src✝ : Subgroup K := comap ϕ ↑P
Q : Subgroup K
hQ : IsPGroup p { x // x ∈ Q }
hle : { toSubmonoid := src✝.toSubmonoid, inv_mem' := (_ : ∀ {x : K}, x ∈ src✝.carrier → x⁻¹ ∈ src✝.carrier) } ≤ Q
⊢ Q = { toSubmonoid := src✝.toSubmonoid, inv_mem' := (_ : ∀ {x : K}, x ∈ src✝.carrier → x⁻¹ ∈ src✝.carrier) }
[PROOFSTEP]
show Q = P.1.comap ϕ
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
h : ↑P ≤ MonoidHom.range ϕ
src✝ : Subgroup K := comap ϕ ↑P
Q : Subgroup K
hQ : IsPGroup p { x // x ∈ Q }
hle : { toSubmonoid := src✝.toSubmonoid, inv_mem' := (_ : ∀ {x : K}, x ∈ src✝.carrier → x⁻¹ ∈ src✝.carrier) } ≤ Q
⊢ Q = comap ϕ ↑P
[PROOFSTEP]
rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
h : ↑P ≤ MonoidHom.range ϕ
src✝ : Subgroup K := comap ϕ ↑P
Q : Subgroup K
hQ : IsPGroup p { x // x ∈ Q }
hle : { toSubmonoid := src✝.toSubmonoid, inv_mem' := (_ : ∀ {x : K}, x ∈ src✝.carrier → x⁻¹ ∈ src✝.carrier) } ≤ Q
⊢ Q = comap ϕ (map ϕ Q)
[PROOFSTEP]
exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
h : ↑P ≤ N
⊢ ↑P ≤ MonoidHom.range (Subgroup.subtype N)
[PROOFSTEP]
rwa [subtype_range]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
P✝ : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
P Q : Sylow p G
hP : ↑P ≤ N
hQ : ↑Q ≤ N
h : Sylow.subtype P hP = Sylow.subtype Q hQ
⊢ P = Q
[PROOFSTEP]
rw [SetLike.ext_iff] at h ⊢
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
P✝ : Sylow p G
K : Type u_2
inst✝ : Group K
ϕ : K →* G
N : Subgroup G
P Q : Sylow p G
hP : ↑P ≤ N
hQ : ↑Q ≤ N
h✝ : Sylow.subtype P hP = Sylow.subtype Q hQ
h : ∀ (x : { x // x ∈ N }), x ∈ Sylow.subtype P hP ↔ x ∈ Sylow.subtype Q hQ
⊢ ∀ (x : G), x ∈ P ↔ x ∈ Q
[PROOFSTEP]
exact fun g => ⟨fun hg => (h ⟨g, hP hg⟩).mp hg, fun hg => (h ⟨g, hQ hg⟩).mpr hg⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p { x // x ∈ P }
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p { x // x ∈ Q }}
hc2 : IsChain (fun x x_1 => x ≤ x_1) c
Q : Subgroup G
hQ : Q ∈ c
x✝ :
  { x //
    x ∈
      {
        toSubmonoid :=
          {
            toSubsemigroup :=
              { carrier := ⋃ (R : ↑c), ↑↑R,
                mul_mem' :=
                  (_ : ∀ {g : G} (h : G), g ∈ ⋃ (R : ↑c), ↑↑R → h ∈ ⋃ (R : ↑c), ↑↑R → g * h ∈ ⋃ (R : ↑c), ↑↑R) },
            one_mem' := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ 1 ∈ t) },
        inv_mem' :=
          (_ :
            ∀ {g : G},
              g ∈
                  {
                        toSubsemigroup :=
                          { carrier := ⋃ (R : ↑c), ↑↑R,
                            mul_mem' :=
                              (_ :
                                ∀ {g : G} (h : G),
                                  g ∈ ⋃ (R : ↑c), ↑↑R → h ∈ ⋃ (R : ↑c), ↑↑R → g * h ∈ ⋃ (R : ↑c), ↑↑R) },
                        one_mem' := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ 1 ∈ t) }.toSubsemigroup.carrier →
                g⁻¹ ∈
                  {
                        toSubsemigroup :=
                          { carrier := ⋃ (R : ↑c), ↑↑R,
                            mul_mem' :=
                              (_ :
                                ∀ {g : G} (h : G),
                                  g ∈ ⋃ (R : ↑c), ↑↑R → h ∈ ⋃ (R : ↑c), ↑↑R → g * h ∈ ⋃ (R : ↑c), ↑↑R) },
                        one_mem' := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ 1 ∈ t) }.toSubsemigroup.carrier) } }
g : G
S : ↑c
hg : g ∈ (fun R => ↑↑R) S
⊢ ∃ k, { val := g, property := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ g ∈ t) } ^ p ^ k = 1
[PROOFSTEP]
refine' Exists.imp (fun k hk => _) (hc1 S.2 ⟨g, hg⟩)
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p { x // x ∈ P }
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p { x // x ∈ Q }}
hc2 : IsChain (fun x x_1 => x ≤ x_1) c
Q : Subgroup G
hQ : Q ∈ c
x✝ :
  { x //
    x ∈
      {
        toSubmonoid :=
          {
            toSubsemigroup :=
              { carrier := ⋃ (R : ↑c), ↑↑R,
                mul_mem' :=
                  (_ : ∀ {g : G} (h : G), g ∈ ⋃ (R : ↑c), ↑↑R → h ∈ ⋃ (R : ↑c), ↑↑R → g * h ∈ ⋃ (R : ↑c), ↑↑R) },
            one_mem' := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ 1 ∈ t) },
        inv_mem' :=
          (_ :
            ∀ {g : G},
              g ∈
                  {
                        toSubsemigroup :=
                          { carrier := ⋃ (R : ↑c), ↑↑R,
                            mul_mem' :=
                              (_ :
                                ∀ {g : G} (h : G),
                                  g ∈ ⋃ (R : ↑c), ↑↑R → h ∈ ⋃ (R : ↑c), ↑↑R → g * h ∈ ⋃ (R : ↑c), ↑↑R) },
                        one_mem' := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ 1 ∈ t) }.toSubsemigroup.carrier →
                g⁻¹ ∈
                  {
                        toSubsemigroup :=
                          { carrier := ⋃ (R : ↑c), ↑↑R,
                            mul_mem' :=
                              (_ :
                                ∀ {g : G} (h : G),
                                  g ∈ ⋃ (R : ↑c), ↑↑R → h ∈ ⋃ (R : ↑c), ↑↑R → g * h ∈ ⋃ (R : ↑c), ↑↑R) },
                        one_mem' := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ 1 ∈ t) }.toSubsemigroup.carrier) } }
g : G
S : ↑c
hg : g ∈ (fun R => ↑↑R) S
k : ℕ
hk : { val := g, property := hg } ^ p ^ k = 1
⊢ { val := g, property := (_ : ∃ t, (t ∈ Set.range fun R => ↑↑R) ∧ g ∈ t) } ^ p ^ k = 1
[PROOFSTEP]
rwa [Subtype.ext_iff, coe_pow] at hk ⊢
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p { x // x ∈ MonoidHom.ker f }
inst✝ : Fintype (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P => exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P => Classical.choose (_ : ∃ Q, comap f ↑Q = ↑P)
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ ↑P = ↑Q
[PROOFSTEP]
rw [← hg, h]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p { x // x ∈ MonoidHom.ker f }
inst✝ : Fintype (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P => exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P => Classical.choose (_ : ∃ Q, comap f ↑Q = ↑P)
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ comap f ↑(g Q) = ↑Q
[PROOFSTEP]
exact (h_exists Q).choose_spec
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite (Sylow p G)
⊢ Finite (Sylow p { x // x ∈ H })
[PROOFSTEP]
cases nonempty_fintype (Sylow p G)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite (Sylow p G)
val✝ : Fintype (Sylow p G)
⊢ Finite (Sylow p { x // x ∈ H })
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ g • P = P ↔ g ∈ normalizer ↑P
[PROOFSTEP]
rw [eq_comm, SetLike.ext_iff, ← inv_mem_iff (G := G) (H := normalizer P.toSubgroup), mem_normalizer_iff, inv_inv]
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ (∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ ↑P ↔ g⁻¹ * h * g ∈ ↑P
[PROOFSTEP]
exact
  forall_congr' fun h =>
    iff_congr Iff.rfl
      ⟨fun ⟨a, b, c⟩ => c ▸ by simpa [mul_assoc] using b, fun hh =>
        ⟨(MulAut.conj g)⁻¹ h, hh, MulAut.apply_inv_self G (MulAut.conj g) h⟩⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : G
x✝ : h ∈ g • P
a : G
b : a ∈ ↑↑P
c : ↑(↑(MulDistribMulAction.toMonoidEnd (MulAut G) G) (↑MulAut.conj g)) a = h
⊢ g⁻¹ * ↑(↑(MulDistribMulAction.toMonoidEnd (MulAut G) G) (↑MulAut.conj g)) a * g ∈ ↑P
[PROOFSTEP]
simpa [mul_assoc] using b
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : Normal ↑P
⊢ g • P = P
[PROOFSTEP]
simp only [Sylow.smul_eq_iff_mem_normalizer, normalizer_eq_top.mpr h, mem_top]
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints { x // x ∈ H } (Sylow p G) ↔ H ≤ normalizer ↑P
[PROOFSTEP]
simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer]
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints { x // x ∈ H } (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P
[PROOFSTEP]
exact Subtype.forall
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p { x // x ∈ P }
Q : Sylow p G
⊢ Q ∈ fixedPoints { x // x ∈ P } (Sylow p G) ↔ P ≤ ↑Q
[PROOFSTEP]
rw [P.sylow_mem_fixedPoints_iff, ← inf_eq_left, hP.inf_normalizer_sylow, inf_eq_left]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
⊢ ∃ g, g • P = Q
[PROOFSTEP]
classical
cases nonempty_fintype (Sylow p G)
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 = card (fixedPoints P (orbit G P)) := ?_
  _ ≡ 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 [← Set.card_singleton (⟨P, mem_orbit_self P⟩ : orbit G P)]
refine' card_congr' (congr_arg _ (Eq.symm _))
rw [Set.eq_singleton_iff_unique_mem]
exact ⟨H.mpr rfl, fun R h => Subtype.ext (Sylow.ext (H.mp h))⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
⊢ ∃ g, g • P = Q
[PROOFSTEP]
cases nonempty_fintype (Sylow p G)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
⊢ ∃ g, g • P = Q
[PROOFSTEP]
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⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
⊢ ∃ g, g • P = Q
[PROOFSTEP]
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
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
this : Set.Nonempty (fixedPoints { x // x ∈ ↑Q } ↑(orbit G P))
⊢ ∃ g, g • P = Q
[PROOFSTEP]
exact
  Exists.elim this fun R hR => by
    rw [← Sylow.ext (H.mp hR)]
    exact R.2
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
this : Set.Nonempty (fixedPoints { x // x ∈ ↑Q } ↑(orbit G P))
R : ↑(orbit G P)
hR : R ∈ fixedPoints { x // x ∈ ↑Q } ↑(orbit G P)
⊢ ∃ g, g • P = Q
[PROOFSTEP]
rw [← Sylow.ext (H.mp hR)]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
this : Set.Nonempty (fixedPoints { x // x ∈ ↑Q } ↑(orbit G P))
R : ↑(orbit G P)
hR : R ∈ fixedPoints { x // x ∈ ↑Q } ↑(orbit G P)
⊢ ∃ g, g • P = ↑R
[PROOFSTEP]
exact R.2
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
⊢ Set.Nonempty (fixedPoints { x // x ∈ ↑Q } ↑(orbit G P))
[PROOFSTEP]
apply Q.2.nonempty_fixed_point_of_prime_not_dvd_card
[GOAL]
case intro.hpα
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
⊢ ¬p ∣ card ↑(orbit G P)
[PROOFSTEP]
refine' fun h => hp.out.not_dvd_one (Nat.modEq_zero_iff_dvd.mp _)
[GOAL]
case intro.hpα
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ card ↑(orbit G P)
⊢ 1 ≡ 0 [MOD p]
[PROOFSTEP]
calc
  1 = card (fixedPoints P (orbit G P)) := ?_
  _ ≡ 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
[GOAL]
case intro.hpα
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ card ↑(orbit G P)
⊢ 1 = card ↑(fixedPoints { x // x ∈ ↑P } ↑(orbit G P))
[PROOFSTEP]
rw [← Set.card_singleton (⟨P, mem_orbit_self P⟩ : orbit G P)]
[GOAL]
case intro.hpα
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ card ↑(orbit G P)
⊢ card ↑{{ val := P, property := (_ : P ∈ orbit G P) }} = card ↑(fixedPoints { x // x ∈ ↑P } ↑(orbit G P))
[PROOFSTEP]
refine' card_congr' (congr_arg _ (Eq.symm _))
[GOAL]
case intro.hpα
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ card ↑(orbit G P)
⊢ fixedPoints { x // x ∈ ↑P } ↑(orbit G P) = {{ val := P, property := (_ : P ∈ orbit G P) }}
[PROOFSTEP]
rw [Set.eq_singleton_iff_unique_mem]
[GOAL]
case intro.hpα
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
val✝ : Fintype (Sylow p G)
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints { x // x ∈ ↑R } ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ card ↑(orbit G P)
⊢ { val := P, property := (_ : P ∈ orbit G P) } ∈ fixedPoints { x // x ∈ ↑P } ↑(orbit G P) ∧
    ∀ (x : ↑(orbit G P)),
      x ∈ fixedPoints { x // x ∈ ↑P } ↑(orbit G P) → x = { val := P, property := (_ : P ∈ orbit G P) }
[PROOFSTEP]
exact ⟨H.mpr rfl, fun R h => Subtype.ext (Sylow.ext (H.mp h))⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
⊢ card (Sylow p G) ≡ 1 [MOD p]
[PROOFSTEP]
refine' Sylow.nonempty.elim fun P : Sylow p G => _
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
⊢ card (Sylow p G) ≡ 1 [MOD p]
[PROOFSTEP]
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
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ card (Sylow p G) ≡ 1 [MOD p]
[PROOFSTEP]
have fin : Fintype (fixedPoints P.1 (Sylow p G)) := by
  rw [this]
  infer_instance
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ Fintype ↑{P}
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
⊢ card (Sylow p G) ≡ 1 [MOD p]
[PROOFSTEP]
have : card (fixedPoints P.1 (Sylow p G)) = 1 := by simp [this]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
⊢ card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) = 1
[PROOFSTEP]
simp [this]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this✝ : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
this : card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) = 1
⊢ card (Sylow p G) ≡ 1 [MOD p]
[PROOFSTEP]
exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this✝ : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
this : card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) = 1
⊢ card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) ≡ 1 [MOD p]
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
⊢ { x // x ∈ ↑P } ≃* { x // x ∈ ↑Q }
[PROOFSTEP]
rw [← Classical.choose_spec (exists_smul_eq G P Q)]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
⊢ { x // x ∈ ↑P } ≃* { x // x ∈ ↑(Classical.choose (_ : ∃ m, m • P = Q) • P) }
[PROOFSTEP]
exact P.equivSMul (Classical.choose (exists_smul_eq G P Q))
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
⊢ stabilizer G P = normalizer ↑P
[PROOFSTEP]
ext
[GOAL]
case h
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
x✝ : G
⊢ x✝ ∈ stabilizer G P ↔ x✝ ∈ normalizer ↑P
[PROOFSTEP]
simp [Sylow.smul_eq_iff_mem_normalizer]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
⊢ ∃ n, n ∈ normalizer ↑P ∧ g⁻¹ * x * g = n⁻¹ * x * n
[PROOFSTEP]
have h1 : ↑P ≤ centralizer (zpowers x : Set G) := by rwa [le_centralizer_iff, zpowers_le]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
⊢ ↑P ≤ centralizer ↑(zpowers x)
[PROOFSTEP]
rwa [le_centralizer_iff, zpowers_le]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
⊢ ∃ n, n ∈ normalizer ↑P ∧ g⁻¹ * x * g = n⁻¹ * x * n
[PROOFSTEP]
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
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
⊢ ↑(g • P) ≤ centralizer ↑(zpowers x)
[PROOFSTEP]
rw [le_centralizer_iff, zpowers_le]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
⊢ x ∈ centralizer ↑↑(g • P)
[PROOFSTEP]
rintro - ⟨z, hz, rfl⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hz : z ∈ ↑↑P
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd (MulAut G) G) (↑MulAut.conj g)) z * x =
    x * ↑(↑(MulDistribMulAction.toMonoidEnd (MulAut G) G) (↑MulAut.conj g)) z
[PROOFSTEP]
specialize hy z hz
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hz : z ∈ ↑↑P
hy : z * (g⁻¹ * x * g) = g⁻¹ * x * g * z
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd (MulAut G) G) (↑MulAut.conj g)) z * x =
    x * ↑(↑(MulDistribMulAction.toMonoidEnd (MulAut G) G) (↑MulAut.conj g)) z
[PROOFSTEP]
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
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
⊢ ∃ n, n ∈ normalizer ↑P ∧ g⁻¹ * x * g = n⁻¹ * x * n
[PROOFSTEP]
obtain ⟨h, hh⟩ := exists_smul_eq (centralizer (zpowers x : Set G)) ((g • P).subtype h2) (P.subtype h1)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : { x_1 // x_1 ∈ centralizer ↑(zpowers x) }
hh : h • Sylow.subtype (g • P) h2 = Sylow.subtype P h1
⊢ ∃ n, n ∈ normalizer ↑P ∧ g⁻¹ * x * g = n⁻¹ * x * n
[PROOFSTEP]
simp_rw [Sylow.smul_subtype, Subgroup.smul_def, smul_smul] at hh
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : { x_1 // x_1 ∈ centralizer ↑(zpowers x) }
hh : Sylow.subtype ((↑h * g) • P) (_ : ↑((↑h * g) • P) ≤ centralizer ↑(zpowers x)) = Sylow.subtype P h1
⊢ ∃ n, n ∈ normalizer ↑P ∧ g⁻¹ * x * g = n⁻¹ * x * n
[PROOFSTEP]
refine' ⟨h * g, Sylow.smul_eq_iff_mem_normalizer.mp (Sylow.subtype_injective hh), _⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : { x_1 // x_1 ∈ centralizer ↑(zpowers x) }
hh : Sylow.subtype ((↑h * g) • P) (_ : ↑((↑h * g) • P) ≤ centralizer ↑(zpowers x)) = Sylow.subtype P h1
⊢ g⁻¹ * x * g = (↑h * g)⁻¹ * x * (↑h * g)
[PROOFSTEP]
rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
⊢ ↑⊤ ≃ ↑(orbit G P)
[PROOFSTEP]
rw [P.orbit_eq_top]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
⊢ G ⧸ stabilizer G P ≃ G ⧸ normalizer ↑P
[PROOFSTEP]
rw [P.stabilizer_eq_normalizer]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
⊢ ¬p ∣ index ↑P
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
h : p ∣ index ↑P
⊢ False
[PROOFSTEP]
letI : Fintype (G ⧸ (P : Subgroup G)) := (P : Subgroup G).fintypeQuotientOfFiniteIndex
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
h : p ∣ index ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
⊢ False
[PROOFSTEP]
rw [index_eq_card (P : Subgroup G)] at h
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h : p ∣ card (G ⧸ ↑P)
⊢ False
[PROOFSTEP]
obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card (G := G ⧸ (P : Subgroup G)) p h
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
⊢ False
[PROOFSTEP]
have h := IsPGroup.of_card ((orderOf_eq_card_zpowers.symm.trans hx).trans (pow_one p).symm)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
⊢ False
[PROOFSTEP]
let Q := (zpowers x).comap (QuotientGroup.mk' (P : Subgroup G))
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
[PROOFSTEP]
have hQ : IsPGroup p Q := by
  apply h.comap_of_ker_isPGroup
  rw [QuotientGroup.ker_mk']
  exact P.2
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ Q }
[PROOFSTEP]
apply h.comap_of_ker_isPGroup
[GOAL]
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ MonoidHom.ker (QuotientGroup.mk' ↑P) }
[PROOFSTEP]
rw [QuotientGroup.ker_mk']
[GOAL]
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ ↑P }
[PROOFSTEP]
exact P.2
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
⊢ False
[PROOFSTEP]
replace hp := mt orderOf_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
hp : ¬x = 1
⊢ False
[PROOFSTEP]
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
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
hp : ↑P < comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
[PROOFSTEP]
exact hp.ne' (P.3 hQ hp.le)
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
⊢ ¬p ∣ index ↑P
[PROOFSTEP]
cases nonempty_fintype (Sylow p G)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
⊢ ¬p ∣ index ↑P
[PROOFSTEP]
rw [← relindex_mul_index le_normalizer, ← card_sylow_eq_index_normalizer]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
[PROOFSTEP]
haveI : (P.subtype le_normalizer : Subgroup (P : Subgroup G).normalizer).Normal := Subgroup.normal_in_normalizer
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
this : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
[PROOFSTEP]
haveI : FiniteIndex ↑(P.subtype le_normalizer : Subgroup (P : Subgroup G).normalizer) := ⟨hP⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
this✝ : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
this : FiniteIndex ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
[PROOFSTEP]
replace hP := not_dvd_index_sylow' (P.subtype le_normalizer)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
val✝ : Fintype (Sylow p G)
this✝ : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
this : FiniteIndex ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
hP : ¬p ∣ index ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
[PROOFSTEP]
exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)
[GOAL]
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
⊢ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N = ⊤
[PROOFSTEP]
refine' top_le_iff.mp fun g _ => _
[GOAL]
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
⊢ g ∈ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_smul_eq N ((MulAut.conjNormal g : MulAut N) • P) P
[GOAL]
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ g ∈ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N
[PROOFSTEP]
rw [← inv_mul_cancel_left (↑n) g, sup_comm]
[GOAL]
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ (↑n)⁻¹ * (↑n * g) ∈ N ⊔ normalizer (map (Subgroup.subtype N) ↑P)
[PROOFSTEP]
apply mul_mem_sup (N.inv_mem n.2)
[GOAL]
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ ↑n * g ∈ normalizer (map (Subgroup.subtype N) ↑P)
[PROOFSTEP]
rw [Sylow.smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← MulAut.conjNormal.map_mul, Sylow.ext_iff,
  Sylow.pointwise_smul_def, Subgroup.pointwise_smul_def] at hn
[GOAL]
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
⊢ ↑n * g ∈ normalizer (map (Subgroup.subtype N) ↑P)
[PROOFSTEP]
refine' fun x =>
  (mem_map_iff_mem
        (show Function.Injective (MulAut.conj (↑n * g)).toMonoidHom from (MulAut.conj (↑n * g)).injective)).symm.trans
    _
[GOAL]
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
x : G
⊢ ↑(MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) x ∈
      map (MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) (map (Subgroup.subtype N) ↑P) ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈ map (Subgroup.subtype N) ↑P
[PROOFSTEP]
rw [map_map, ← congr_arg (map N.subtype) hn, map_map]
[GOAL]
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
x : G
⊢ ↑(MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) x ∈
      map (MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) (Subgroup.subtype N)) ↑P ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈
      map
        (MonoidHom.comp (Subgroup.subtype N)
          (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
            (↑MulAut.conjNormal (↑n * g))))
        ↑P
[PROOFSTEP]
rfl
[GOAL]
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p G
hP : ↑P ≤ N
⊢ normalizer ↑P ⊔ N = ⊤
[PROOFSTEP]
rw [← Sylow.normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype, inf_of_le_left hP]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
s : Subgroup G
t : Set (G ⧸ s)
⊢ Fintype.card ↑(mk ⁻¹' t) = Fintype.card { x // x ∈ s } * Fintype.card ↑t
[PROOFSTEP]
rw [← Fintype.card_prod, Fintype.card_congr (preimageMkEquivSubgroupProdSet _ _)]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints { x // x ∈ H } (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit { x // x ∈ H } ↑x → y = ↑x
n : G
hn : n ∈ H
this : (n⁻¹ * x)⁻¹ * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H
[PROOFSTEP]
rw [mul_inv_rev, inv_inv] at this
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints { x // x ∈ H } (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit { x // x ∈ H } ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H
[PROOFSTEP]
convert this
[GOAL]
case h.e'_4.h.e'_6
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints { x // x ∈ H } (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit { x // x ∈ H } ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹⁻¹ = x
[PROOFSTEP]
rw [inv_inv]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit { x // x ∈ H } ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m => m • ↑x) { val := b, property := hb₁ } = Quotient.mk'' y
hb₂ : (b * x)⁻¹ * y ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H
[PROOFSTEP]
rw [hx] at hb₂
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit { x // x ∈ H } ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m => m • ↑x) { val := b, property := hb₁ } = Quotient.mk'' y
hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H
[PROOFSTEP]
simpa [mul_inv_rev, mul_assoc] using hb₂
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
⊢ ∀ (x y : Subtype ↑(normalizer H)), Setoid.r x y ↔ ↑x ≈ ↑y
[PROOFSTEP]
intros
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : Subtype ↑(normalizer H)
⊢ Setoid.r x✝ y✝ ↔ ↑x✝ ≈ ↑y✝
[PROOFSTEP]
dsimp only [instHasEquiv]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : Subtype ↑(normalizer H)
⊢ Setoid.r x✝ y✝ ↔ Setoid.r ↑x✝ ↑y✝
[PROOFSTEP]
rw [leftRel_apply (α := normalizer H), leftRel_apply]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : Subtype ↑(normalizer H)
⊢ x✝⁻¹ * y✝ ∈ Subgroup.comap (Subgroup.subtype (normalizer H)) H ↔ (↑x✝)⁻¹ * ↑y✝ ∈ H
[PROOFSTEP]
rfl
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
⊢ Fintype.card ({ x // x ∈ normalizer H } ⧸ Subgroup.comap (Subgroup.subtype (normalizer H)) H) ≡
    Fintype.card (G ⧸ H) [MOD p]
[PROOFSTEP]
rw [← Fintype.card_congr (fixedPointsMulLeftCosetsEquivQuotient H)]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
⊢ Fintype.card ↑(MulAction.fixedPoints { x // x ∈ H } (G ⧸ H)) ≡ Fintype.card (G ⧸ H) [MOD p]
[PROOFSTEP]
exact ((IsPGroup.of_card hH).card_modEq_card_fixedPoints _).symm
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
⊢ Fintype.card { x // x ∈ normalizer H } ≡ Fintype.card G [MOD p ^ (n + 1)]
[PROOFSTEP]
have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
this : { x // x ∈ subgroupOf H (normalizer H) } ≃ { x // x ∈ H }
⊢ Fintype.card { x // x ∈ normalizer H } ≡ Fintype.card G [MOD p ^ (n + 1)]
[PROOFSTEP]
rw [card_eq_card_quotient_mul_card_subgroup H, card_eq_card_quotient_mul_card_subgroup (H.subgroupOf (normalizer H)),
  Fintype.card_congr this, hH, pow_succ]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
this : { x // x ∈ subgroupOf H (normalizer H) } ≃ { x // x ∈ H }
⊢ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) * p ^ n ≡ Fintype.card (G ⧸ H) * p ^ n [MOD
    p * p ^ n]
[PROOFSTEP]
exact (card_quotient_normalizer_modEq_card_quotient hH).mul_right' _
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
⊢ Fintype.card (G ⧸ H) * Fintype.card { x // x ∈ H } = s * p * Fintype.card { x // x ∈ H }
[PROOFSTEP]
rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ Subgroup.comap (Subgroup.subtype (normalizer H)) H) % p
⊢ Fintype.card ({ x // x ∈ normalizer H } ⧸ Subgroup.comap (Subgroup.subtype (normalizer H)) H) % p = 0
[PROOFSTEP]
rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
⊢ Fintype.card (G ⧸ H) * Fintype.card { x // x ∈ H } = s * p * Fintype.card { x // x ∈ H }
[PROOFSTEP]
rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
⊢ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p = 0
[PROOFSTEP]
rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
⊢ Fintype.card
      { x_1 //
        x_1 ∈
          Subgroup.map (Subgroup.subtype (normalizer H))
            (Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x)) } =
    p ^ (n + 1)
[PROOFSTEP]
show
  Fintype.card (Subgroup.map H.normalizer.subtype (comap (mk' (H.subgroupOf H.normalizer)) (Subgroup.zpowers x))) =
    p ^ (n + 1)
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
⊢ Fintype.card
      { x_1 //
        x_1 ∈
          Subgroup.map (Subgroup.subtype (normalizer H))
            (Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x)) } =
    p ^ (n + 1)
[PROOFSTEP]
suffices
  Fintype.card (Subtype.val '' (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer)) =
    p ^ (n + 1)
  by convert this using 2
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
this : Fintype.card ↑(Subtype.val '' ↑(Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x))) = p ^ (n + 1)
⊢ Fintype.card
      { x_1 //
        x_1 ∈
          Subgroup.map (Subgroup.subtype (normalizer H))
            (Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x)) } =
    p ^ (n + 1)
[PROOFSTEP]
convert this using 2
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
⊢ Fintype.card ↑(Subtype.val '' ↑(Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x))) = p ^ (n + 1)
[PROOFSTEP]
rw [Set.card_image_of_injective (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer)
    Subtype.val_injective,
  pow_succ', ← hH, Fintype.card_congr hequiv, ← hx, orderOf_eq_card_zpowers, ← Fintype.card_prod]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
⊢ Fintype.card ↑↑(Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x)) =
    Fintype.card ({ x // x ∈ subgroupOf H (normalizer H) } × { x_1 // x_1 ∈ zpowers x })
[PROOFSTEP]
exact @Fintype.card_congr _ _ (_) (_) (preimageMkEquivSubgroupProdSet (H.subgroupOf H.normalizer) (zpowers x))
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
⊢ H ≤ Subgroup.map (Subgroup.subtype (normalizer H)) (Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x))
[PROOFSTEP]
intro y hy
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
y : G
hy : y ∈ H
⊢ y ∈ Subgroup.map (Subgroup.subtype (normalizer H)) (Subgroup.comap (mk' (subgroupOf H (normalizer H))) (zpowers x))
[PROOFSTEP]
simp only [exists_prop, Subgroup.coeSubtype, mk'_apply, Subgroup.mem_map, Subgroup.mem_comap]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
y : G
hy : y ∈ H
⊢ ∃ x_1, ↑x_1 ∈ zpowers x ∧ ↑x_1 = y
[PROOFSTEP]
refine' ⟨⟨y, le_normalizer hy⟩, ⟨0, _⟩, rfl⟩
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
y : G
hy : y ∈ H
⊢ (fun x x_1 => x ^ x_1) x 0 = ↑{ val := y, property := (_ : y ∈ normalizer H) }
[PROOFSTEP]
dsimp only
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
y : G
hy : y ∈ H
⊢ x ^ 0 = ↑{ val := y, property := (_ : y ∈ normalizer H) }
[PROOFSTEP]
rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
s : ℕ
hs : Fintype.card G = s * p ^ (n + 1)
hcard : Fintype.card (G ⧸ H) = s * p
hm : s * p % p = Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)) % p
hm' : p ∣ Fintype.card ({ x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H))
x : { x // x ∈ normalizer H } ⧸ subgroupOf H (normalizer H)
hx : orderOf x = p
hequiv : { x // x ∈ H } ≃ { x // x ∈ subgroupOf H (normalizer H) }
y : G
hy : y ∈ H
⊢ { val := y, property := (_ : y ∈ normalizer H) } ∈ subgroupOf H (normalizer H)
[PROOFSTEP]
simpa using hy
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
_wf : m - 1 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Fintype.card { x // x ∈ K } = p ^ (m - 1) ∧ H ≤ K
⊢ p ^ (m - 1 + 1) ∣ Fintype.card G
[PROOFSTEP]
rwa [tsub_add_cancel_of_le h0m.nat_succ_le]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
_wf : m - 1 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Fintype.card { x // x ∈ K } = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Fintype.card G
K' : Subgroup G
hK' : Fintype.card { x // x ∈ K' } = p ^ (m - 1 + 1) ∧ K ≤ K'
⊢ Fintype.card { x // x ∈ K' } = p ^ m
[PROOFSTEP]
rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Fintype.card G
H : Subgroup G
hH : Fintype.card { x // x ∈ H } = p ^ n
hnm✝ : n ≤ m
hnm : n = m
⊢ Fintype.card { x // x ∈ H } = p ^ m ∧ H ≤ H
[PROOFSTEP]
simp [hH, hnm]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ n ∣ Fintype.card G
⊢ 1 = p ^ 0
[PROOFSTEP]
simp
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
[PROOFSTEP]
rw [← pow_one p] at hdvd
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Fintype.card G
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
[PROOFSTEP]
have key := P.pow_dvd_card_of_pow_dvd_card hdvd
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Fintype.card G
key : p ^ 1 ∣ Fintype.card { x // x ∈ ↑P }
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
[PROOFSTEP]
rwa [pow_one] at key
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
⊢ ↑P ≠ ⊥
[PROOFSTEP]
refine' fun h => hp.out.not_dvd_one _
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
h : ↑P = ⊥
⊢ p ∣ 1
[PROOFSTEP]
have key : p ∣ card (P : Subgroup G) := P.dvd_card_of_dvd_card hdvd
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
h : ↑P = ⊥
key : p ∣ Fintype.card { x // x ∈ ↑P }
⊢ p ∣ 1
[PROOFSTEP]
rwa [h, card_bot] at key
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
⊢ Fintype.card { x // x ∈ ↑P } = p ^ ↑(Nat.factorization (Fintype.card G)) p
[PROOFSTEP]
obtain ⟨n, heq : card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'
[GOAL]
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } = p ^ ↑(Nat.factorization (Fintype.card G)) p
[PROOFSTEP]
refine' Nat.dvd_antisymm _ (P.pow_dvd_card_of_pow_dvd_card (Nat.ord_proj_dvd _ p))
[GOAL]
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } ∣ p ^ ↑(Nat.factorization (Fintype.card G)) p
[PROOFSTEP]
rw [heq, ← hp.out.pow_dvd_iff_dvd_ord_proj (show card G ≠ 0 from card_ne_zero), ← heq]
[GOAL]
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } ∣ Fintype.card G
[PROOFSTEP]
exact P.1.card_subgroup_dvd_card
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Fintype G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Fintype { x // x ∈ H }
card_eq : Fintype.card { x // x ∈ H } = p ^ ↑(Nat.factorization (Fintype.card G)) p
⊢ ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → H ≤ Q → Q = H
[PROOFSTEP]
obtain ⟨P, hHP⟩ := (IsPGroup.of_card card_eq).exists_le_sylow
[GOAL]
case intro
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Fintype G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Fintype { x // x ∈ H }
card_eq : Fintype.card { x // x ∈ H } = p ^ ↑(Nat.factorization (Fintype.card G)) p
P : Sylow p G
hHP : H ≤ ↑P
⊢ ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → H ≤ Q → Q = H
[PROOFSTEP]
exact SetLike.ext' (Set.eq_of_subset_of_card_le hHP (P.card_eq_multiplicity.trans card_eq.symm).le).symm ▸ P.3
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
⊢ Subsingleton (Sylow p G)
[PROOFSTEP]
apply Subsingleton.intro
[GOAL]
case allEq
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
⊢ ∀ (a b : Sylow p G), a = b
[PROOFSTEP]
intro Q R
[GOAL]
case allEq
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
⊢ Q = R
[PROOFSTEP]
obtain ⟨x, h1⟩ := exists_smul_eq G P Q
[GOAL]
case allEq.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x : G
h1 : x • P = Q
⊢ Q = R
[PROOFSTEP]
obtain ⟨x, h2⟩ := exists_smul_eq G P R
[GOAL]
case allEq.intro.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x✝ : G
h1 : x✝ • P = Q
x : G
h2 : x • P = R
⊢ Q = R
[PROOFSTEP]
rw [Sylow.smul_eq_of_normal] at h1 h2
[GOAL]
case allEq.intro.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x✝ : G
h1 : P = Q
x : G
h2 : P = R
⊢ Q = R
[PROOFSTEP]
rw [← h1, ← h2]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
⊢ Characteristic ↑P
[PROOFSTEP]
haveI := Sylow.subsingleton_of_normal P h
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
⊢ Characteristic ↑P
[PROOFSTEP]
rw [characteristic_iff_map_eq]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
⊢ ∀ (ϕ : G ≃* G), Subgroup.map (MulEquiv.toMonoidHom ϕ) ↑P = ↑P
[PROOFSTEP]
intro Φ
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ Subgroup.map (MulEquiv.toMonoidHom Φ) ↑P = ↑P
[PROOFSTEP]
show (Φ • P).toSubgroup = P.toSubgroup
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ ↑(Φ • P) = ↑P
[PROOFSTEP]
congr
[GOAL]
case e_self
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ Φ • P = P
[PROOFSTEP]
simp
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hn : Normal (normalizer ↑P)
⊢ Normal ↑P
[PROOFSTEP]
rw [← normalizer_eq_top, ← normalizer_sup_eq_top' P le_normalizer, sup_idem]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ normalizer (normalizer ↑P) = normalizer ↑P
[PROOFSTEP]
have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this :
  Normal (normalizer ↑(Sylow.subtype P (_ : ↑P ≤ normalizer (normalizer ↑P)))) →
    Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer (normalizer ↑P)))
⊢ normalizer (normalizer ↑P) = normalizer ↑P
[PROOFSTEP]
simp_rw [← normalizer_eq_top, Sylow.coe_subtype, ← subgroupOf_normalizer_eq le_normalizer, ←
  subgroupOf_normalizer_eq le_rfl, subgroupOf_self] at this
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P)) = ⊤
⊢ normalizer (normalizer ↑P) = normalizer ↑P
[PROOFSTEP]
rw [← subtype_range (P : Subgroup G).normalizer.normalizer, MonoidHom.range_eq_map, ← this trivial]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : True → subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P)) = ⊤
⊢ Subgroup.map (Subgroup.subtype (normalizer (normalizer ↑P)))
      (subgroupOf (normalizer ↑P) (normalizer (normalizer ↑P))) =
    normalizer ↑P
[PROOFSTEP]
exact map_comap_eq_self (le_normalizer.trans (ge_of_eq (subtype_range _)))
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ normalizer ↑P = ⊤
[PROOFSTEP]
rcases eq_top_or_exists_le_coatom (↑P : Subgroup G).normalizer with (heq | ⟨K, hK, hNK⟩)
[GOAL]
case inl
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
heq : normalizer ↑P = ⊤
⊢ normalizer ↑P = ⊤
[PROOFSTEP]
exact heq
[GOAL]
case inr.intro.intro
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
⊢ normalizer ↑P = ⊤
[PROOFSTEP]
haveI := hnc _ hK
[GOAL]
case inr.intro.intro
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
this : Normal K
⊢ normalizer ↑P = ⊤
[PROOFSTEP]
have hPK : ↑P ≤ K := le_trans le_normalizer hNK
[GOAL]
case inr.intro.intro
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
this : Normal K
hPK : ↑P ≤ K
⊢ normalizer ↑P = ⊤
[PROOFSTEP]
refine' (hK.1 _).elim
[GOAL]
case inr.intro.intro
G : Type u
α : Type v
β : Type w
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
this : Normal K
hPK : ↑P ≤ K
⊢ K = ⊤
[PROOFSTEP]
rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
⊢ ((p : { x // x ∈ (Nat.factorization (Fintype.card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
[PROOFSTEP]
set ps := (Fintype.card G).factorization.support
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
⊢ ((p : { x // x ∈ ps }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
[PROOFSTEP]
let P : ∀ p, Sylow p G := default
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
⊢ ((p : { x // x ∈ ps }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
[PROOFSTEP]
have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y :=
  by
  rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
  haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
  haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)
  have hne' : p₁ ≠ p₂ := by simpa using hne
  apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))
  apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
⊢ _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
[PROOFSTEP]
rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
[GOAL]
case mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
⊢ ∀ (x y : G), x ∈ P ↑{ val := p₁, property := hp₁ } → y ∈ P ↑{ val := p₂, property := hp₂ } → Commute x y
[PROOFSTEP]
haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
[GOAL]
case mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
⊢ ∀ (x y : G), x ∈ P ↑{ val := p₁, property := hp₁ } → y ∈ P ↑{ val := p₂, property := hp₂ } → Commute x y
[PROOFSTEP]
haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)
[GOAL]
case mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ ∀ (x y : G), x ∈ P ↑{ val := p₁, property := hp₁ } → y ∈ P ↑{ val := p₂, property := hp₂ } → Commute x y
[PROOFSTEP]
have hne' : p₁ ≠ p₂ := by simpa using hne
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ p₁ ≠ p₂
[PROOFSTEP]
simpa using hne
[GOAL]
case mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ ∀ (x y : G), x ∈ P ↑{ val := p₁, property := hp₁ } → y ∈ P ↑{ val := p₂, property := hp₂ } → Commute x y
[PROOFSTEP]
apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))
[GOAL]
case mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ _root_.Disjoint ↑(P p₁) ↑(P p₂)
[PROOFSTEP]
apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : { x // x ∈ ps }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
[PROOFSTEP]
refine'
  MulEquiv.trans (N := ∀ p : ps, P p) _
    _
      -- There is only one Sylow subgroup for each p, so the inner product is trivial
[GOAL]
case refine'_1
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : { x // x ∈ ps }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* ((p : { x // x ∈ ps }) → { x // x ∈ P ↑p })
case refine'_2
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : { x // x ∈ ps }) → { x // x ∈ P ↑p }) ≃* G
[PROOFSTEP]
show (∀ p : ps, ∀ P : Sylow p G, P) ≃* ∀ p : ps, P p
[GOAL]
case refine'_1
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : { x // x ∈ ps }) → (P : Sylow (↑p) G) → { x // x ∈ P }) ≃* ((p : { x // x ∈ ps }) → { x // x ∈ P ↑p })
[PROOFSTEP]
apply @MulEquiv.piCongrRight ps (fun p => ∀ P : Sylow p G, P) (fun p => P p) _ _
[GOAL]
case refine'_1
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ (j : { x // x ∈ ps }) → ((P : Sylow (↑j) G) → { x // x ∈ P }) ≃* { x // x ∈ ↑(P ↑j) }
[PROOFSTEP]
rintro ⟨p, hp⟩
[GOAL]
case refine'_1.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
⊢ ((P : Sylow (↑{ val := p, property := hp }) G) → { x // x ∈ P }) ≃* { x // x ∈ ↑(P ↑{ val := p, property := hp }) }
[PROOFSTEP]
haveI hp' := Fact.mk (Nat.prime_of_mem_factorization hp)
[GOAL]
case refine'_1.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
hp' : Fact (Nat.Prime p)
⊢ ((P : Sylow (↑{ val := p, property := hp }) G) → { x // x ∈ P }) ≃* { x // x ∈ ↑(P ↑{ val := p, property := hp }) }
[PROOFSTEP]
haveI := subsingleton_of_normal _ (hn (P p))
[GOAL]
case refine'_1.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
hp' : Fact (Nat.Prime p)
this : Subsingleton (Sylow p G)
⊢ ((P : Sylow (↑{ val := p, property := hp }) G) → { x // x ∈ P }) ≃* { x // x ∈ ↑(P ↑{ val := p, property := hp }) }
[PROOFSTEP]
change (∀ P : Sylow p G, P) ≃* P p
[GOAL]
case refine'_1.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
hp' : Fact (Nat.Prime p)
this : Subsingleton (Sylow p G)
⊢ ((P : Sylow p G) → { x // x ∈ P }) ≃* { x // x ∈ ↑(P p) }
[PROOFSTEP]
exact MulEquiv.piSubsingleton _ _
[GOAL]
case refine'_2
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : { x // x ∈ ps }) → { x // x ∈ P ↑p }) ≃* G
[PROOFSTEP]
show (∀ p : ps, P p) ≃* G
[GOAL]
case refine'_2
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : { x // x ∈ ps }) → { x // x ∈ P ↑p }) ≃* G
[PROOFSTEP]
apply MulEquiv.ofBijective (Subgroup.noncommPiCoprod hcomm)
[GOAL]
case refine'_2
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Bijective ↑(noncommPiCoprod hcomm)
[PROOFSTEP]
apply (bijective_iff_injective_and_card _).mpr
[GOAL]
case refine'_2
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Injective ↑(noncommPiCoprod hcomm) ∧ Fintype.card ((i : { x // x ∈ ps }) → { x // x ∈ ↑(P ↑i) }) = Fintype.card G
[PROOFSTEP]
constructor
[GOAL]
case refine'_2.left
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Injective ↑(noncommPiCoprod hcomm)
case refine'_2.right
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : { x // x ∈ ps }) → { x // x ∈ ↑(P ↑i) }) = Fintype.card G
[PROOFSTEP]
show Injective _
[GOAL]
case refine'_2.left
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Injective ↑(noncommPiCoprod hcomm)
[PROOFSTEP]
apply Subgroup.injective_noncommPiCoprod_of_independent
[GOAL]
case refine'_2.left.hind
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ CompleteLattice.Independent fun i => ↑(P ↑i)
[PROOFSTEP]
apply independent_of_coprime_order hcomm
[GOAL]
case refine'_2.left.hind
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ∀ (i j : { x // x ∈ ps }), i ≠ j → Nat.coprime (Fintype.card { x // x ∈ ↑(P ↑i) }) (Fintype.card { x // x ∈ ↑(P ↑j) })
[PROOFSTEP]
rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
[GOAL]
case refine'_2.left.hind.mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
⊢ Nat.coprime (Fintype.card { x // x ∈ ↑(P ↑{ val := p₁, property := hp₁ }) })
    (Fintype.card { x // x ∈ ↑(P ↑{ val := p₂, property := hp₂ }) })
[PROOFSTEP]
haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
[GOAL]
case refine'_2.left.hind.mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
⊢ Nat.coprime (Fintype.card { x // x ∈ ↑(P ↑{ val := p₁, property := hp₁ }) })
    (Fintype.card { x // x ∈ ↑(P ↑{ val := p₂, property := hp₂ }) })
[PROOFSTEP]
haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)
[GOAL]
case refine'_2.left.hind.mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ Nat.coprime (Fintype.card { x // x ∈ ↑(P ↑{ val := p₁, property := hp₁ }) })
    (Fintype.card { x // x ∈ ↑(P ↑{ val := p₂, property := hp₂ }) })
[PROOFSTEP]
have hne' : p₁ ≠ p₂ := by simpa using hne
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ p₁ ≠ p₂
[PROOFSTEP]
simpa using hne
[GOAL]
case refine'_2.left.hind.mk.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : { val := p₁, property := hp₁ } ≠ { val := p₂, property := hp₂ }
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ Nat.coprime (Fintype.card { x // x ∈ ↑(P ↑{ val := p₁, property := hp₁ }) })
    (Fintype.card { x // x ∈ ↑(P ↑{ val := p₂, property := hp₂ }) })
[PROOFSTEP]
apply IsPGroup.coprime_card_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
[GOAL]
case refine'_2.right
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : { x // x ∈ ps }) → { x // x ∈ ↑(P ↑i) }) = Fintype.card G
[PROOFSTEP]
show card (∀ p : ps, P p) = card G
[GOAL]
case refine'_2.right
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((p : { x // x ∈ ps }) → { x // x ∈ P ↑p }) = Fintype.card G
[PROOFSTEP]
calc
  card (∀ p : ps, P p) = ∏ p : ps, card (P p) := Fintype.card_pi
  _ = ∏ p : ps, p.1 ^ (card G).factorization p.1 :=
    by
    congr 1 with ⟨p, hp⟩
    exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_factorization hp⟩ (P p)
  _ = ∏ p in ps, p ^ (card G).factorization p := (Finset.prod_finset_coe (fun p => p ^ (card G).factorization p) _)
  _ = (card G).factorization.prod (· ^ ·) := rfl
  _ = card G := Nat.factorization_prod_pow_eq_self Fintype.card_ne_zero
[GOAL]
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ∏ p : { x // x ∈ ps }, Fintype.card { x // x ∈ ↑(P ↑p) } =
    ∏ p : { x // x ∈ ps }, ↑p ^ ↑(Nat.factorization (Fintype.card G)) ↑p
[PROOFSTEP]
congr 1 with ⟨p, hp⟩
[GOAL]
case e_f.h.mk
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
hn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (P : Sylow p G), Normal ↑P
ps : Finset ℕ := (Nat.factorization (Fintype.card G)).support
P : (p : ℕ) → Sylow p G := default
hcomm : _root_.Pairwise fun p₁ p₂ => ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
⊢ Fintype.card { x // x ∈ ↑(P ↑{ val := p, property := hp }) } =
    ↑{ val := p, property := hp } ^ ↑(Nat.factorization (Fintype.card G)) ↑{ val := p, property := hp }
[PROOFSTEP]
exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_factorization hp⟩ (P p)


[GOAL]
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
refine' (iH.comap f).eq_bot_or_eq_top.imp (fun h => _) fun h => _
[GOAL]
case refine'_1
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
h : comap f H = ⊥
⊢ H = ⊥
[PROOFSTEP]
rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
[GOAL]
case refine'_2
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
h : comap f H = ⊤
⊢ H = ⊤
[PROOFSTEP]
rw [← comap_top f] at h
[GOAL]
case refine'_2
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
h : comap f H = comap f ⊤
⊢ H = ⊤
[PROOFSTEP]
exact comap_injective hf h