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

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
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

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)
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

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
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

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
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

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 _
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)

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
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

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 (α := ℕ)
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

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]
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

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
State after:
no goals

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]
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

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
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

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 _)
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

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
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

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]
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 } ∈ ⊤

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
State after:
no goals

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
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

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
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

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]
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

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
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

State before:
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
Tactic:
rw [Subgroup.index_ker f, Nat.card_eq_fintype_card, Nat.lt_succ_iff]
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
⊢ Fintype.card ↑(Set.range ⇑f) ≤ 2

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

State before:
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
⊢ Fintype.card ↑(Set.range ⇑f) ≤ 2

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
Tactic:
apply Nat.le_of_dvd two_pos
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
⊢ Fintype.card ↑(Set.range ⇑f) ∣ 2

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

State before:
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
⊢ Fintype.card ↑(Set.range ⇑f) ∣ 2

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
Tactic:
apply dvd_trans f.range.card_subgroup_dvd_card
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
⊢ Fintype.card (Equiv.Perm (G ⧸ H)) ∣ 2

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

State before:
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
⊢ Fintype.card (Equiv.Perm (G ⧸ H)) ∣ 2

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
Tactic:
rw [Fintype.card_perm, ← Nat.card_eq_fintype_card]
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
⊢ Nat.factorial (Nat.card (G ⧸ H)) ∣ 2

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

State before:
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
⊢ Nat.factorial (Nat.card (G ⧸ H)) ∣ 2

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
Tactic:
unfold Subgroup.index at hH
State after:
case a.hmn
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Nat.card (G ⧸ H) = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ Nat.factorial (Nat.card (G ⧸ H)) ∣ 2

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

State before:
case a.hmn
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Nat.card (G ⧸ H) = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ Nat.factorial (Nat.card (G ⧸ H)) ∣ 2

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
Tactic:
rw [hH]
State after:
case a.hmn
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Nat.card (G ⧸ H) = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ Nat.factorial 2 ∣ 2

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

State before:
case a.hmn
α : Type ?u.28021
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Nat.card (G ⧸ H) = 2
this✝ : Fintype (G ⧸ H)
f : G →* Equiv.Perm (G ⧸ H) := MulAction.toPermHom G (G ⧸ H)
this : index H ≠ 0
⊢ Nat.factorial 2 ∣ 2

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
Tactic:
norm_num
State after:
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

State before:
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
Tactic:
intro h
State after:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2
⊢ False

State before:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2
⊢ False
Tactic:
apply Nat.not_succ_le_self 1
State after:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2
⊢ Nat.succ 1 ≤ 1

State before:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2
⊢ Nat.succ 1 ≤ 1
Tactic:
change 2 ≤ 1
State after:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2
⊢ 2 ≤ 1

State before:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) < 2
⊢ 2 ≤ 1
Tactic:
rw [Nat.lt_succ_iff] at h
State after:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ 2 ≤ 1

State before:
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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ 2 ≤ 1
Tactic:
apply le_trans _ h
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 : index H ≠ 0
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ 2 ≤ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)))

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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ 2 ≤ index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)))
Tactic:
rw [← hH, ← Subgroup.normalCore_eq_ker H]
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 : index H ≠ 0
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ index H ≤ index (normalCore H)

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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ index H ≤ index (normalCore H)
Tactic:
apply Nat.le_of_dvd
State after:
case 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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ 0 < index (normalCore H)

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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ index H ∣ index (normalCore H)

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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ index H ∣ index (normalCore H)
Tactic:
exact Subgroup.index_dvd_of_le (Subgroup.normalCore_le H)
State after:
no goals

State before:
case 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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ 0 < index (normalCore H)
Tactic:
rw [zero_lt_iff, Subgroup.normalCore_eq_ker H, Subgroup.index_ker f,
  Nat.card_eq_fintype_card]
State after:
case 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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ Fintype.card ↑(Set.range ⇑f) ≠ 0

State before:
case 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
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ Fintype.card ↑(Set.range ⇑f) ≠ 0
Tactic:
exact Fintype.card_ne_zero
State after:
no goals

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)
⊢ index H ≠ 0
Tactic:
rw [hH]
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)
⊢ 2 ≠ 0

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)
⊢ 2 ≠ 0
Tactic:
norm_num
State after:
no goals