internlm/Lean-Github huggingface dataset:
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ g • s = s ↔ g • ↑s = ↑s
Tactic:
rw [← Finset.coe_smul_finset, ← Finset.coe_inj]
Proof state after:
no goals
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro.h0
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Set.Nonempty ↑s
Tactic:
simp only [Finset.coe_nonempty, ← Finset.card_pos, hs]
Proof state after:
case inr.intro.h0
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ 0 < n
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro.h0
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ 0 < n
Tactic:
apply lt_trans one_pos h_one_lt
Proof state after:
no goals
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Set.Nonempty (↑s)ᶜ
Tactic:
simp only [← Finset.coe_compl, Finset.coe_nonempty,
  ← Finset.card_compl_lt_iff_nonempty, compl_compl, hs]
Proof state after:
case inr.intro.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ n < Fintype.card α
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ n < Fintype.card α
Tactic:
exact hn
Proof state after:
no goals
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro.hα
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Fintype.card α ≠ 2 * Set.ncard ↑s
Tactic:
simp only [Set.ncard_coe_Finset, ne_eq]
Proof state after:
case inr.intro.hα
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ ¬Fintype.card α = 2 * s.card
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro.hα
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ ¬Fintype.card α = 2 * s.card
Tactic:
simp only [Finset.coe_sort_coe, Fintype.card_coe, hs]
Proof state after:
case inr.intro.hα
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ ¬Fintype.card α = 2 * n
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro.hα
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ ¬Fintype.card α = 2 * n
Tactic:
exact hα
Proof state after:
no goals
Theorem: alternatingGroup_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Subgroup.Characteristic (alternatingGroup α)
Tactic:
cases' subsingleton_or_nontrivial α with hα hα
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Subsingleton α
⊢ Subgroup.Characteristic (alternatingGroup α)

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
⊢ Subgroup.Characteristic (alternatingGroup α)
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
⊢ Subgroup.Characteristic (alternatingGroup α)
Tactic:
apply Subgroup.Characteristic.mk
Proof state after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
⊢ ∀ (ϕ : Equiv.Perm α ≃* Equiv.Perm α),
    Subgroup.comap (MulEquiv.toMonoidHom ϕ) (alternatingGroup α) = alternatingGroup α
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
⊢ ∀ (ϕ : Equiv.Perm α ≃* Equiv.Perm α),
    Subgroup.comap (MulEquiv.toMonoidHom ϕ) (alternatingGroup α) = alternatingGroup α
Tactic:
intro φ
Proof state after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
⊢ Subgroup.comap (MulEquiv.toMonoidHom φ) (alternatingGroup α) = alternatingGroup α
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
⊢ Subgroup.comap (MulEquiv.toMonoidHom φ) (alternatingGroup α) = alternatingGroup α
Tactic:
rw [alternatingGroup_eq_sign_ker]
Proof state after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
⊢ Subgroup.comap (MulEquiv.toMonoidHom φ) (MonoidHom.ker Equiv.Perm.sign) = MonoidHom.ker Equiv.Perm.sign
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
⊢ Subgroup.comap (MulEquiv.toMonoidHom φ) (MonoidHom.ker Equiv.Perm.sign) = MonoidHom.ker Equiv.Perm.sign
Tactic:
rw [MonoidHom.comap_ker]
Proof state after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Tactic:
let s := Equiv.Perm.sign.comp φ.toMonoidHom
Proof state after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Tactic:
have hs : Function.Surjective s :=  by
  change Function.Surjective (Equiv.Perm.sign ∘ φ)
  rw [Function.Surjective.of_comp_iff _]
  exact Equiv.Perm.sign_surjective α
  exact MulEquiv.surjective φ
Proof state after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Tactic:
obtain ⟨g', hg'⟩ := hs (-1)
Proof state after:
case inr.fixed.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg' : s g' = -1
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg' : s g' = -1
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Tactic:
have hg' : s g' ≠ 1 := by
  rw [hg', ← bne_iff_ne]
  rfl
Proof state after:
case inr.fixed.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
⊢ MonoidHom.ker (MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) = MonoidHom.ker Equiv.Perm.sign
Tactic:
apply congr_arg
Proof state after:
case inr.fixed.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
⊢ MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ) = Equiv.Perm.sign
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
⊢ MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ) = Equiv.Perm.sign
Tactic:
ext g
Proof state after:
case inr.fixed.intro.h.h.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ ↑((MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) g) = ↑(Equiv.Perm.sign g)
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro.h.h.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ ↑((MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)) g) = ↑(Equiv.Perm.sign g)
Tactic:
simp only [MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom, Function.comp_apply]
Proof state after:
case inr.fixed.intro.h.h.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ ↑(Equiv.Perm.sign (φ g)) = ↑(Equiv.Perm.sign g)
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro.h.h.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ ↑(Equiv.Perm.sign (φ g)) = ↑(Equiv.Perm.sign g)
Tactic:
apply congr_arg
Proof state after:
case inr.fixed.intro.h.h.a.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ Equiv.Perm.sign (φ g) = Equiv.Perm.sign g
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro.h.h.a.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ Equiv.Perm.sign (φ g) = Equiv.Perm.sign g
Tactic:
refine' Equiv.Perm.swap_induction_on g _ _
Proof state after:
case inr.fixed.intro.h.h.a.h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ Equiv.Perm.sign (φ 1) = Equiv.Perm.sign 1

case inr.fixed.intro.h.h.a.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ ∀ (f : Equiv.Perm α) (x y : α),
    x ≠ y →
      Equiv.Perm.sign (φ f) = Equiv.Perm.sign f →
        Equiv.Perm.sign (φ (Equiv.swap x y * f)) = Equiv.Perm.sign (Equiv.swap x y * f)
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Subsingleton α
⊢ Subgroup.Characteristic (alternatingGroup α)
Tactic:
rw [alternatingGroup_of_subsingleton]
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Subsingleton α
⊢ Subgroup.Characteristic ⊥
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Subsingleton α
⊢ Subgroup.Characteristic ⊥
Tactic:
exact Subgroup.botCharacteristic
Proof state after:
no goals
Theorem: alternatingGroup_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective ⇑s
Tactic:
change Function.Surjective (Equiv.Perm.sign ∘ φ)
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective (⇑Equiv.Perm.sign ∘ ⇑φ)
Theorem: alternatingGroup_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective (⇑Equiv.Perm.sign ∘ ⇑φ)
Tactic:
rw [Function.Surjective.of_comp_iff _]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective ⇑Equiv.Perm.sign

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective ⇑φ
Theorem: alternatingGroup_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective ⇑Equiv.Perm.sign

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective ⇑φ
Tactic:
exact Equiv.Perm.sign_surjective α
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective ⇑φ
Theorem: alternatingGroup_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
⊢ Function.Surjective ⇑φ
Tactic:
exact MulEquiv.surjective φ
Proof state after:
no goals
Theorem: alternatingGroup_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg' : s g' = -1
⊢ s g' ≠ 1
Tactic:
rw [hg', ← bne_iff_ne]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg' : s g' = -1
⊢ (-1 != 1) = true
Theorem: alternatingGroup_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg' : s g' = -1
⊢ (-1 != 1) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro.h.h.a.h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ Equiv.Perm.sign (φ 1) = Equiv.Perm.sign 1
Tactic:
rw [map_one, Equiv.Perm.sign.map_one]
Proof state after:
no goals
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro.h.h.a.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g : Equiv.Perm α
⊢ ∀ (f : Equiv.Perm α) (x y : α),
    x ≠ y →
      Equiv.Perm.sign (φ f) = Equiv.Perm.sign f →
        Equiv.Perm.sign (φ (Equiv.swap x y * f)) = Equiv.Perm.sign (Equiv.swap x y * f)
Tactic:
intro f x y hxy hf
Proof state after:
case inr.fixed.intro.h.h.a.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
⊢ Equiv.Perm.sign (φ (Equiv.swap x y * f)) = Equiv.Perm.sign (Equiv.swap x y * f)
Theorem: alternatingGroup_is_characteristic
Proof state before:
case inr.fixed.intro.h.h.a.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
⊢ Equiv.Perm.sign (φ (Equiv.swap x y * f)) = Equiv.Perm.sign (Equiv.swap x y * f)
Tactic:
simp only [map_mul, hf]
Proof state after:
case inr.fixed.intro.h.h.a.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
s : Equiv.Perm α →* ℤˣ := MonoidHom.comp Equiv.Perm.sign (MulEquiv.toMonoidHom φ)
hs : Function.Surjective ⇑s
g' : Equiv.Perm α
hg'✝ : s g' = -1
hg' : s g' ≠ 1
g f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
⊢ Equiv.Perm.sign (φ (Equiv.swap x y)) * Equiv.Perm.sign f = Equiv.Perm.sign (Equiv.swap x y) * Equiv.Perm.sign f