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

Tactic:
rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]

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