-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb')
right₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₅ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inr b₁) (Sum.inr b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₆ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inr b₁) (Sum.inr b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₇ right₈ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂ * σb')) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)

Tactic:
rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap,
        sign_swap hb, sign_swap (Sum.inr_injective.ne_iff.mpr hb)]

Premises used: Iff.mpr, Sum.inr_injective, Function.Injective.ne_iff, Equiv.Perm.sign_mul, Equiv.Perm.sumCongr_one_swap, Equiv.Perm.sumCongr_mul, OfNat.ofNat, one_mul, Equiv.Perm.sign_swap