Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor (Jordan/IndexNormal.lean)

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
⊢ Normal H
Tactic:
let f := MulAction.toPermHom G (G ⧸ H)
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ Normal H

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ Normal H
Tactic:
suffices f.ker = H by
  rw [← this]
  apply MonoidHom.normal_ker f
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ MonoidHom.ker f = H

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ MonoidHom.ker f = H
Tactic:
suffices H.normalCore.relindex H = 1 by
  rw [← Subgroup.normalCore_eq_ker]
  unfold Subgroup.relindex at this
  rw [Subgroup.index_eq_one] at this
  apply le_antisymm; apply Subgroup.normalCore_le
  intro x hx
  rw [← Subgroup.coe_mk H x hx, ← Subgroup.mem_subgroupOf, this]
  apply Subgroup.mem_top
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ relindex (normalCore H) H = 1

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ index H ≠ 0
Tactic:
rw [hHp]
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ p ≠ 0

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ p ≠ 0
Tactic:
exact Nat.Prime.ne_zero hp
State after:
no goals

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : MonoidHom.ker f = H
⊢ Normal H
Tactic:
rw [← this]
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : MonoidHom.ker f = H
⊢ Normal (MonoidHom.ker f)

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : MonoidHom.ker f = H
⊢ Normal (MonoidHom.ker f)
Tactic:
apply MonoidHom.normal_ker f
State after:
no goals

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : relindex (normalCore H) H = 1
⊢ MonoidHom.ker f = H
Tactic:
rw [← Subgroup.normalCore_eq_ker]
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : relindex (normalCore H) H = 1
⊢ normalCore H = H

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : relindex (normalCore H) H = 1
⊢ normalCore H = H
Tactic:
unfold Subgroup.relindex at this
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index (subgroupOf (normalCore H) H) = 1
⊢ normalCore H = H

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index (subgroupOf (normalCore H) H) = 1
⊢ normalCore H = H
Tactic:
rw [Subgroup.index_eq_one] at this
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ normalCore H = H

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ normalCore H = H
Tactic:
apply le_antisymm
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ normalCore H ≤ H

case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ H ≤ normalCore H

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ normalCore H ≤ H

case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ H ≤ normalCore H
Tactic:
apply Subgroup.normalCore_le
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ H ≤ normalCore H

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ H ≤ normalCore H
Tactic:
intro x hx
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
x : G
hx : x ∈ H
⊢ x ∈ normalCore H

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
x : G
hx : x ∈ H
⊢ x ∈ normalCore H
Tactic:
rw [← Subgroup.coe_mk H x hx, ← Subgroup.mem_subgroupOf, this]
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
x : G
hx : x ∈ H
⊢ { val := x, property := hx } ∈ ⊤

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
x : G
hx : x ∈ H
⊢ { val := x, property := hx } ∈ ⊤
Tactic:
apply Subgroup.mem_top
State after:
no goals

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ relindex (normalCore H) H = 1
Tactic:
apply mul_left_injective₀ this
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ (fun a => a * index H) (relindex (normalCore H) H) = (fun a => a * index H) 1

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ (fun a => a * index H) (relindex (normalCore H) H) = (fun a => a * index H) 1
Tactic:
dsimp
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ relindex (normalCore H) H * index H = 1 * index H

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ relindex (normalCore H) H * index H = 1 * index H
Tactic:
rw [Subgroup.relindex_mul_index (Subgroup.normalCore_le H)]
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (normalCore H) = 1 * index H

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (normalCore H) = 1 * index H
Tactic:
rw [one_mul]
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (normalCore H) = index H

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (normalCore H) = index H
Tactic:
rw [Subgroup.normalCore_eq_ker]
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = index H

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = index H
Tactic:
rw [hHp]
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = p

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = p
Tactic:
change f.ker.index = p
State after:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker f) = p

State before:
case a
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker f) = p
Tactic:
refine' Or.resolve_left (Nat.Prime.eq_one_or_self_of_dvd hp f.ker.index _) _
State after:
case a.refine'_1
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker f) ∣ p

case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ ¬index (MonoidHom.ker f) = 1

State before:
case a.refine'_1
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker f) ∣ p

case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ ¬index (MonoidHom.ker f) = 1
Tactic:
apply aux_dvd_lemma hp
State after:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p

case a.refine'_1.hr
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ ∀ {l : ℕ}, Nat.Prime l → l ∣ index (MonoidHom.ker f) → p ≤ l

case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ ¬index (MonoidHom.ker f) = 1

State before:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p
Tactic:
have hf := Subgroup.index_ker f
State after:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Nat.card ↑(Set.range ⇑f)
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p

State before:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Nat.card ↑(Set.range ⇑f)
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p
Tactic:
rw [Nat.card_eq_fintype_card] at hf
State after:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p

State before:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p
Tactic:
rw [hf, ← hHp]
State after:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Nat.factorial (index H)

State before:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Nat.factorial (index H)
Tactic:
unfold Subgroup.index
State after:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Nat.factorial (Nat.card (G ⧸ H))

State before:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Nat.factorial (Nat.card (G ⧸ H))
Tactic:
rw [Nat.card_eq_fintype_card, ← Fintype.card_perm]
State after:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Fintype.card (Equiv.Perm (G ⧸ H))

State before:
case a.refine'_1.h
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Fintype.card (Equiv.Perm (G ⧸ H))
Tactic:
apply f.range.card_subgroup_dvd_card
State after:
no goals

State before:
case a.refine'_1.hr
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ ∀ {l : ℕ}, Nat.Prime l → l ∣ index (MonoidHom.ker f) → p ≤ l
Tactic:
intro l hl hl'
State after:
case a.refine'_1.hr
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
l : ℕ
hl : Nat.Prime l
hl' : l ∣ index (MonoidHom.ker f)
⊢ p ≤ l

State before:
case a.refine'_1.hr
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
l : ℕ
hl : Nat.Prime l
hl' : l ∣ index (MonoidHom.ker f)
⊢ p ≤ l
Tactic:
apply hp' hl
State after:
case a.refine'_1.hr
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
l : ℕ
hl : Nat.Prime l
hl' : l ∣ index (MonoidHom.ker f)
⊢ l ∣ Fintype.card G

State before:
case a.refine'_1.hr
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
l : ℕ
hl : Nat.Prime l
hl' : l ∣ index (MonoidHom.ker f)
⊢ l ∣ Fintype.card G
Tactic:
exact dvd_trans hl' f.ker.index_dvd_card
State after:
no goals

State before:
case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ ¬index (MonoidHom.ker f) = 1
Tactic:
intro hf
State after:
case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ False

State before:
case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ False
Tactic:
apply Nat.Prime.ne_one hp
State after:
case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ p = 1

State before:
case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ p = 1
Tactic:
rw [← hHp, Subgroup.index_eq_one, eq_top_iff]
State after:
case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ ⊤ ≤ H

State before:
case a.refine'_2
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ ⊤ ≤ H
Tactic:
apply le_trans _ (Subgroup.normalCore_le H)
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ ⊤ ≤ normalCore H

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ ⊤ ≤ normalCore H
Tactic:
rw [← eq_top_iff, ← Subgroup.index_eq_one, Subgroup.normalCore_eq_ker]
State after:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = 1

State before:
α : Type ?u.18788
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Group G
H : Subgroup G
p : ℕ
hp : Nat.Prime p
hHp : index H = p
hp' : ∀ {l : ℕ}, Nat.Prime l → l ∣ Fintype.card G → p ≤ l
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = 1
Tactic:
exact hf
State after:
no goals