internlm/Lean-Github huggingface dataset:
Theorem: aux_dvd_lemma
Proof state before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ False
Tactic:
apply (lt_iff_not_ge p.pred p).mp (Nat.pred_lt (Nat.Prime.ne_zero hp))
Proof state after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ Nat.pred p ≥ p
Theorem: aux_dvd_lemma
Proof state before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ Nat.pred p ≥ p
Tactic:
rw [Nat.pred_eq_sub_one]
Proof state after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p - 1 ≥ p
Theorem: aux_dvd_lemma
Proof state before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p - 1 ≥ p
Tactic:
rw [ge_iff_le]
Proof state after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p ≤ p - 1
Theorem: aux_dvd_lemma
Proof state before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ p ≤ p - 1
Tactic:
exact le_trans (hr hl hl'.left) hl'.right
Proof state after:
no goals
Theorem: aux_dvd_lemma
Proof state before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ p * ?m.17725
Tactic:
rw [Nat.mul_factorial_pred (Nat.Prime.pos hp)]
Proof state after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ Nat.factorial p
Theorem: aux_dvd_lemma
Proof state before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ Nat.factorial p
Tactic:
exact h
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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)
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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)
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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 } ∈ ⊤
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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)]
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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 _) _
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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