internlm/Lean-Github huggingface dataset:
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
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
hf : index (MonoidHom.ker f) = Nat.card ↑(Set.range ⇑f)
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
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
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ index (MonoidHom.ker f) ∣ Nat.factorial p
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
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
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Nat.factorial (index H)
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
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
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Nat.factorial (Nat.card (G ⧸ H))
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
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
hf : index (MonoidHom.ker f) = Fintype.card ↑(Set.range ⇑f)
⊢ Fintype.card ↑(Set.range ⇑f) ∣ Fintype.card (Equiv.Perm (G ⧸ H))
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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'
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_smallest_prime_factor
Proof 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)
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 H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ ⊤ ≤ normalCore 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 H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ ⊤ ≤ normalCore H
Tactic:
rw [← eq_top_iff, ← Subgroup.index_eq_one, 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 : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ 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)
this : index H ≠ 0
hf : index (MonoidHom.ker f) = 1
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = 1
Tactic:
exact hf
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
⊢ Normal H
Tactic:
have : Fintype (G ⧸ H) := by
  apply fintypeOfNotInfinite _
  intro h
  apply two_ne_zero (α := ℕ)
  rw [← hH]
  exact Cardinal.mk_toNat_of_infinite
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this : Fintype (G ⧸ H)
⊢ Normal H
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this : Fintype (G ⧸ H)
⊢ Normal H
Tactic:
let f := MulAction.toPermHom G (G ⧸ H)
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ Normal H
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ Normal H
Tactic:
convert MonoidHom.normal_ker f
Proof state after:
case h.e'_3
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ H = MonoidHom.ker f
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
case h.e'_3
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ H = MonoidHom.ker f
Tactic:
suffices H.normalCore.relindex H = 1 by
  rw [← Subgroup.normalCore_eq_ker]
  erw [Subgroup.index_eq_one] at this
  apply le_antisymm _ (Subgroup.normalCore_le _)
  intro x hx
  rw [← Subgroup.coe_mk H x hx, ← Subgroup.mem_subgroupOf, this]
  apply Subgroup.mem_top
Proof state after:
case h.e'_3
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
⊢ relindex (normalCore H) H = 1
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
⊢ Fintype (G ⧸ H)
Tactic:
apply fintypeOfNotInfinite _
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
⊢ ¬Infinite (G ⧸ H)
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
⊢ ¬Infinite (G ⧸ H)
Tactic:
intro h
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
h : Infinite (G ⧸ H)
⊢ False
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
h : Infinite (G ⧸ H)
⊢ False
Tactic:
apply two_ne_zero (α := ℕ)
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
h : Infinite (G ⧸ H)
⊢ 2 = 0
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
h : Infinite (G ⧸ H)
⊢ 2 = 0
Tactic:
rw [← hH]
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
h : Infinite (G ⧸ H)
⊢ index H = 0
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
h : Infinite (G ⧸ H)
⊢ index H = 0
Tactic:
exact Cardinal.mk_toNat_of_infinite
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : relindex (normalCore H) H = 1
⊢ H = MonoidHom.ker f
Tactic:
rw [← Subgroup.normalCore_eq_ker]
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : relindex (normalCore H) H = 1
⊢ H = normalCore H
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : relindex (normalCore H) H = 1
⊢ H = normalCore H
Tactic:
erw [Subgroup.index_eq_one] at this
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : subgroupOf (normalCore H) H = ⊤
⊢ H = normalCore H
Tactic:
apply le_antisymm _ (Subgroup.normalCore_le _)
Proof state after:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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_two
Proof state before:
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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_two
Proof state before:
case a
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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_two
Proof state before:
case a
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
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), one_mul,
  Subgroup.normalCore_eq_ker, hH]
Proof state after:
case a
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = 2
Theorem: Subgroup.normal_of_index_eq_two
Proof state before:
case a
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) = 2
Tactic:
apply Nat.eq_of_lt_succ_of_not_lt
Proof state after:
case a.hmn
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2 + 1

case a.h
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : index H = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ ¬index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2