internlm/Lean-Github huggingface dataset:
Theorem: Subgroup.normal_of_index_eq_two
Proof 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]
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
⊢ 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
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
⊢ 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
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
⊢ 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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]
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
⊢ 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
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 : index H ≠ 0
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ 2 ≤ index (MonoidHom.ker (MulAction.toPermHom G (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
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]
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 : index H ≠ 0
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ index H ≤ index (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 : index H ≠ 0
h : index (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))) ≤ 1
⊢ index H ≤ index (normalCore H)
Tactic:
apply Nat.le_of_dvd
Proof 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)
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
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)
Proof state after:
no goals
Theorem: Subgroup.normal_of_index_eq_two
Proof 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]
Proof 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
Theorem: Subgroup.normal_of_index_eq_two
Proof 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
Proof state after:
no goals
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)
⊢ index H ≠ 0
Tactic:
rw [hH]
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)
⊢ 2 ≠ 0
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)
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ g = List.prod l
Tactic:
induction' g using Equiv.Perm.swap_induction_on with f x y hxy hf
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ 1 = List.prod l

case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
hf : ∃ l, (∀ s ∈ l, IsSwap s) ∧ f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ 1 = List.prod l
Tactic:
use List.nil
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (∀ s ∈ [], IsSwap s) ∧ 1 = List.prod []
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (∀ s ∈ [], IsSwap s) ∧ 1 = List.prod []
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∀ s ∈ [], IsSwap s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ 1 = List.prod []
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∀ s ∈ [], IsSwap s
Tactic:
intro s hs
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ IsSwap s
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ IsSwap s
Tactic:
exfalso
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ False
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ False
Tactic:
exact List.not_mem_nil s hs
Proof state after:
no goals
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ 1 = List.prod []
Tactic:
simp only [List.prod_nil]
Proof state after:
no goals
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
hf : ∃ l, (∀ s ∈ l, IsSwap s) ∧ f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l
Tactic:
obtain ⟨l, hl, hf⟩ := hf
Proof state after:
case a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l
Tactic:
use Equiv.swap x y::l
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ (∀ s ∈ swap x y :: l, IsSwap s) ∧ swap x y * f = List.prod (swap x y :: l)
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ (∀ s ∈ swap x y :: l, IsSwap s) ∧ swap x y * f = List.prod (swap x y :: l)
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∀ s ∈ swap x y :: l, IsSwap s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = List.prod (swap x y :: l)
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = List.prod (swap x y :: l)
Tactic:
rw [List.prod_cons]
Proof state after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = swap x y * List.prod l
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = swap x y * List.prod l
Tactic:
rw [hf]
Proof state after:
no goals
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∀ s ∈ swap x y :: l, IsSwap s
Tactic:
intro s hs
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ swap x y :: l
⊢ IsSwap s
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ swap x y :: l
⊢ IsSwap s
Tactic:
rw [List.mem_cons] at hs
Proof state after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y ∨ s ∈ l
⊢ IsSwap s
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y ∨ s ∈ l
⊢ IsSwap s
Tactic:
cases' hs with hs hs
Proof state after:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap s

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap s

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Tactic:
rw [hs]
Proof state after:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap (swap x y)

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s