Theorem: alternatingGroup_is_characteristic (Jordan/IndexNormal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Subgroup.Characteristic (alternatingGroup α)
Tactic:
cases' subsingleton_or_nontrivial α with hα hα
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 α)

State before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
⊢ Subgroup.Characteristic (alternatingGroup α)
Tactic:
apply Subgroup.Characteristic.mk
State after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
⊢ ∀ (ϕ : Equiv.Perm α ≃* Equiv.Perm α),
    Subgroup.comap (MulEquiv.toMonoidHom ϕ) (alternatingGroup α) = alternatingGroup α

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 φ
State after:
case inr.fixed
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nontrivial α
φ : Equiv.Perm α ≃* Equiv.Perm α
⊢ Subgroup.comap (MulEquiv.toMonoidHom φ) (alternatingGroup α) = alternatingGroup α

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

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

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

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

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

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

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

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

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

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

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

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Subsingleton α
⊢ Subgroup.Characteristic (alternatingGroup α)
Tactic:
rw [alternatingGroup_of_subsingleton]
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Subsingleton α
⊢ Subgroup.Characteristic ⊥

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Subsingleton α
⊢ Subgroup.Characteristic ⊥
Tactic:
exact Subgroup.botCharacteristic
State after:
no goals

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 ∘ φ)
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 ∘ ⇑φ)

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 _]
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 ⇑φ

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 α
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 ⇑φ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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