case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑Perm.sign (optionCongr 1) = ↑Perm.sign 1

case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ∀ (f : Perm α) (x y : α),
    x ≠ y →
      ↑Perm.sign (optionCongr f) = ↑Perm.sign f → ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑Perm.sign (optionCongr e) = ↑Perm.sign e
refine Perm.swap_induction_on e ?_ ?_
no goals
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑Perm.sign (optionCongr 1) = ↑Perm.sign 1
simp [Perm.one_def]
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e f : Perm α
x y : α
hne : x ≠ y
h : ↑Perm.sign (optionCongr f) = ↑Perm.sign f
⊢ ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ∀ (f : Perm α) (x y : α),
    x ≠ y →
      ↑Perm.sign (optionCongr f) = ↑Perm.sign f → ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
intro f x y hne h
no goals
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e f : Perm α
x y : α
hne : x ≠ y
h : ↑Perm.sign (optionCongr f) = ↑Perm.sign f
⊢ ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
simp [h, hne, Perm.mul_def, ← Equiv.optionCongr_trans]