internlm/Lean-Github huggingface dataset:
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)) * Equiv.Perm.sign f = Equiv.Perm.sign (Equiv.swap x y) * Equiv.Perm.sign f
Tactic:
apply congr_arg₂ _ _ rfl
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
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 (Equiv.swap x y)
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
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 (Equiv.swap x y)
Tactic:
revert x y hxy
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
hg' : s g' ≠ 1
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
⊢ ∀ (x y : α), x ≠ y → Equiv.Perm.sign (φ (Equiv.swap x y)) = Equiv.Perm.sign (Equiv.swap x y)
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
hg' : s g' ≠ 1
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
⊢ ∀ (x y : α), x ≠ y → Equiv.Perm.sign (φ (Equiv.swap x y)) = Equiv.Perm.sign (Equiv.swap x y)
Tactic:
by_contra h
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
hg' : s g' ≠ 1
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
h : ¬∀ (x y : α), x ≠ y → Equiv.Perm.sign (φ (Equiv.swap x y)) = Equiv.Perm.sign (Equiv.swap x y)
⊢ False
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
hg' : s g' ≠ 1
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
h : ¬∀ (x y : α), x ≠ y → Equiv.Perm.sign (φ (Equiv.swap x y)) = Equiv.Perm.sign (Equiv.swap x y)
⊢ False
Tactic:
push_neg at h
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
hg' : s g' ≠ 1
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
h : ∃ x y, x ≠ y ∧ Equiv.Perm.sign (φ (Equiv.swap x y)) ≠ Equiv.Perm.sign (Equiv.swap x y)
⊢ False
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
hg' : s g' ≠ 1
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
h : ∃ x y, x ≠ y ∧ Equiv.Perm.sign (φ (Equiv.swap x y)) ≠ Equiv.Perm.sign (Equiv.swap x y)
⊢ False
Tactic:
obtain ⟨a, b, hab, hk⟩ := h
Proof state after:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ Equiv.Perm.sign (Equiv.swap a b)
⊢ False
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ Equiv.Perm.sign (Equiv.swap a b)
⊢ False
Tactic:
rw [Equiv.Perm.sign_swap hab] at hk
Proof state after:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
⊢ False
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
⊢ False
Tactic:
let hk := Or.resolve_right (Int.units_eq_one_or (s _)) hk
Proof state after:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
⊢ False
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
⊢ False
Tactic:
apply hg'
Proof state after:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
⊢ s g' = 1
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
⊢ s g' = 1
Tactic:
refine' Equiv.Perm.swap_induction_on g' s.map_one _
Proof state after:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
⊢ ∀ (f : Equiv.Perm α) (x y : α), x ≠ y → s f = 1 → s (Equiv.swap x y * f) = 1
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.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
g f : Equiv.Perm α
hf : Equiv.Perm.sign (φ f) = Equiv.Perm.sign f
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
⊢ ∀ (f : Equiv.Perm α) (x y : α), x ≠ y → s f = 1 → s (Equiv.swap x y * f) = 1
Tactic:
intro f x y hxy hf
Proof state after:
case intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
⊢ s (Equiv.swap x y * f) = 1
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
⊢ s (Equiv.swap x y * f) = 1
Tactic:
rw [s.map_mul, hf, mul_one]
Proof state after:
case intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
⊢ s (Equiv.swap x y) = 1
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
⊢ s (Equiv.swap x y) = 1
Tactic:
obtain ⟨u, hu⟩ := Equiv.Perm.isConj_swap hxy hab
Proof state after:
case intro.intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap x y) (Equiv.swap a b)
⊢ s (Equiv.swap x y) = 1
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap x y) (Equiv.swap a b)
⊢ s (Equiv.swap x y) = 1
Tactic:
apply mul_left_cancel (a := s u)
Proof state after:
case intro.intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap x y) (Equiv.swap a b)
⊢ s ↑u * s (Equiv.swap x y) = s ↑u * 1
Theorem: alternatingGroup_is_characteristic
Proof state before:
case intro.intro.intro.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
g f✝ : Equiv.Perm α
hf✝ : Equiv.Perm.sign (φ f✝) = Equiv.Perm.sign f✝
a b : α
hab : a ≠ b
hk✝ : Equiv.Perm.sign (φ (Equiv.swap a b)) ≠ -1
hk : s (Equiv.swap a b) = 1 := Or.resolve_right (Int.units_eq_one_or (s (Equiv.swap a b))) hk✝
f : Equiv.Perm α
x y : α
hxy : x ≠ y
hf : s f = 1
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap x y) (Equiv.swap a b)
⊢ s ↑u * s (Equiv.swap x y) = s ↑u * 1
Tactic:
rw [← s.map_mul, SemiconjBy.eq hu, s.map_mul, hk, mul_one, one_mul]
Proof state after:
no goals
Theorem: isCommutative_of_prime_order
Proof state before:
α : Type ?u.14086
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card G = p
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
haveI := isCyclic_of_prime_card h
Proof state after:
α : Type ?u.14086
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card G = p
this : IsCyclic G
⊢ Std.Commutative fun x x_1 => x * x_1
Theorem: isCommutative_of_prime_order
Proof state before:
α : Type ?u.14086
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card G = p
this : IsCyclic G
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
exact Std.Commutative.mk (IsCyclic.commGroup.mul_comm)
Proof state after:
no goals
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
apply @isCommutative_of_prime_order _ _ _ 3 _
Proof state after:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Fintype.card ↥(alternatingGroup α) = 3
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Fintype.card ↥(alternatingGroup α) = 3
Tactic:
have hα' : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial, hα]
  norm_num
Proof state after:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 3
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 3
Tactic:
apply mul_right_injective₀ (a := 2) (by norm_num)
Proof state after:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 3
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 3
Tactic:
simp only [two_mul_card_alternatingGroup, Fintype.card_perm, hα]
Proof state after:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 2 * 3
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 2 * 3
Tactic:
norm_num
Proof state after:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 6
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 6
Tactic:
rfl
Proof state after:
no goals
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Nontrivial α
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, hα]
Proof state after:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ 1 < 3
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ 1 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: alternatingGroup.isCommutative_of_order_three
Proof state before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: aux_dvd_lemma
Proof state before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ p
Tactic:
rw [← Nat.Coprime.dvd_mul_right _]
Proof state after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ r ∣ p * ?m.17725

α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ ℕ

α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.Coprime r ?m.17725
Theorem: aux_dvd_lemma
Proof state before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.Coprime r (Nat.factorial (p - 1))
Tactic:
rw [Nat.coprime_iff_gcd_eq_one]
Proof state after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.gcd r (Nat.factorial (p - 1)) = 1
Theorem: aux_dvd_lemma
Proof state before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
⊢ Nat.gcd r (Nat.factorial (p - 1)) = 1
Tactic:
by_contra h
Proof state after:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
⊢ False
Theorem: aux_dvd_lemma
Proof state before:
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
⊢ False
Tactic:
obtain ⟨l, hl, hl'⟩ := Nat.exists_prime_and_dvd h
Proof state after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ Nat.gcd r (Nat.factorial (p - 1))
⊢ False
Theorem: aux_dvd_lemma
Proof state before:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ Nat.gcd r (Nat.factorial (p - 1))
⊢ False
Tactic:
rw [Nat.dvd_gcd_iff, Nat.Prime.dvd_factorial hl] at hl'
Proof state after:
case intro.intro
α : Type ?u.17644
inst✝¹ : Fintype α
inst✝ : DecidableEq α
r p : ℕ
hp : Nat.Prime p
h✝ : r ∣ Nat.factorial p
hr : ∀ {l : ℕ}, Nat.Prime l → l ∣ r → p ≤ l
h : ¬Nat.gcd r (Nat.factorial (p - 1)) = 1
l : ℕ
hl : Nat.Prime l
hl' : l ∣ r ∧ l ≤ p - 1
⊢ False