internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ ↑(kg (h (kg.symm { val := x, property := hx' }))) = g ↑(h { val := g⁻¹ x, property := hx })
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))
Tactic:
suffices hx' : x ∉ g • s by
  rw [ofSubtype_apply_of_not_mem h hx]
  rw [ofSubtype_apply_of_not_mem ((Equiv.permCongrMul kg) h) hx']
  simp only [apply_inv_self]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
⊢ x ∉ g • s
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
⊢ x ∉ g • s
Tactic:
rw [← Finset.inv_smul_mem_iff]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
⊢ g⁻¹ • x ∉ s
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
⊢ g⁻¹ • x ∉ s
Tactic:
exact hx
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
hx' : x ∉ g • s
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))
Tactic:
rw [ofSubtype_apply_of_not_mem h hx]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
hx' : x ∉ g • s
⊢ (ofSubtype (kg' h)) x = g (g⁻¹ x)
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
hx' : x ∉ g • s
⊢ (ofSubtype (kg' h)) x = g (g⁻¹ x)
Tactic:
rw [ofSubtype_apply_of_not_mem ((Equiv.permCongrMul kg) h) hx']
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
hx' : x ∉ g • s
⊢ x = g (g⁻¹ x)
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
hx' : x ∉ g • s
⊢ x = g (g⁻¹ x)
Tactic:
simp only [apply_inv_self]
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ alternatingGroup α ≤ N
Tactic:
rw [← alternatingGroup.commutator_group_eq hα]
Proof state after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ commutator (Perm α) ≤ N
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ commutator (Perm α) ≤ N
Tactic:
refine' commutator_le_iwasawa _ iwasawa_two hnN _
Proof state after:
case refine'_1
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsQuasipreprimitive (Perm α) ↑(Nat.Combination α 2)

case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ fixedPoints ↥N ↑(Nat.Combination α 2) ≠ ⊤
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ fixedPoints ↥N ↑(Nat.Combination α 2) ≠ ⊤
Tactic:
intro h
Proof state after:
case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
⊢ False
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
⊢ False
Tactic:
obtain ⟨g, hgN, hg_ne⟩ := N.nontrivial_iff_exists_ne_one.mp ntN
Proof state after:
case refine'_2.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ False
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_2.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ False
Tactic:
obtain ⟨s, hs⟩ := Nat.combination.mulAction_faithful
  (G := Equiv.Perm α) (α := α) (g := g) 2
  (by norm_num)
  (by rw [PartENat.card_eq_coe_fintype_card, PartENat.coe_le_coe]
      apply le_trans (by norm_num) hα)
  (by exact hg_ne)
Proof state after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ False
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ False
Tactic:
apply hs
Proof state after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ g • s = s
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ g • s = s
Tactic:
suffices s ∈ fixedPoints N (Nat.Combination α 2) by
  rw [mem_fixedPoints] at this
  exact this ⟨g, hgN⟩
Proof state after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ fixedPoints ↥N ↑(Nat.Combination α 2)
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ fixedPoints ↥N ↑(Nat.Combination α 2)
Tactic:
rw [h, Set.top_eq_univ]
Proof state after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ _root_.Set.univ
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ _root_.Set.univ
Tactic:
apply Set.mem_univ
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_1
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsQuasipreprimitive (Perm α) ↑(Nat.Combination α 2)
Tactic:
apply IsPreprimitive.isQuasipreprimitive
Proof state after:
case refine'_1.hGX
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsPreprimitive (Perm α) ↑(Nat.Combination α 2)
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_1.hGX
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsPreprimitive (Perm α) ↑(Nat.Combination α 2)
Tactic:
apply Nat.Combination_isPreprimitive
Proof state after:
case refine'_1.hGX.h_one_le
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_1.hGX.h_one_le
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
norm_num
Proof state after:
case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
apply lt_of_lt_of_le _ hα
Proof state after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < 5

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < 5

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
norm_num
Proof state after:
case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
apply ne_of_gt
Proof state after:
case refine'_1.hGX.hα.h
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < Fintype.card α
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
case refine'_1.hGX.hα.h
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < Fintype.card α
Tactic:
apply lt_of_lt_of_le _ hα
Proof state after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < 5
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < 5
Tactic:
norm_num
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ ↑(Nat.succ 2) ≤ PartENat.card α
Tactic:
rw [PartENat.card_eq_coe_fintype_card, PartENat.coe_le_coe]
Proof state after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ Nat.succ 2 ≤ Fintype.card α
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ Nat.succ 2 ≤ Fintype.card α
Tactic:
apply le_trans (by norm_num) hα
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ Nat.succ 2 ≤ 5
Tactic:
norm_num
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ toPerm g ≠ 1
Tactic:
exact hg_ne
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
this : s ∈ fixedPoints ↥N ↑(Nat.Combination α 2)
⊢ g • s = s
Tactic:
rw [mem_fixedPoints] at this
Proof state after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
this : ∀ (m : ↥N), m • s = s
⊢ g • s = s
Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups
Proof state before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
this : ∀ (m : ↥N), m • s = s
⊢ g • s = s
Tactic:
exact this ⟨g, hgN⟩
Proof state after:
no goals
Theorem: Equiv.Perm.disjoint_iff_support_disjoint
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
⊢ Disjoint f g ↔ _root_.Disjoint (support f) (support g)
Tactic:
simp only [Equiv.Perm.disjoint_iff_eq_or_eq,
  Finset.disjoint_iff_inter_eq_empty, ← Equiv.Perm.not_mem_support,
  ← Finset.mem_compl, ← Finset.mem_union, ← Finset.compl_inter,
  ← Finset.compl_eq_univ_iff, ← Finset.eq_univ_iff_forall]
Proof state after:
no goals
Theorem: Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ c = cycleOf g x ↔ x ∈ support c
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ c = cycleOf g x → x ∈ support c

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c → c = cycleOf g x
Theorem: Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ c = cycleOf g x → x ∈ support c
Tactic:
intro hcx
Proof state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ x ∈ support c