-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_sumCongr (σa : Perm α) (σb : Perm β) : sign (sumCongr σa σb) = sign σa * sign σb

Proof state:
case right
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (sumCongr 1 σb) = sign σb

Tactic:
refine σb.swap_induction_on ?_ fun σb' b₁ b₂ hb ih => ?_

Result:
case right.refine_1
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (sumCongr 1 1) = sign 1

case right.refine_2
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ sign (sumCongr 1 (swap b₁ b₂ * σb')) = sign (swap b₁ b₂ * σb')

Proof state:
case left.refine_2
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign ((swap a₁ a₂ * σa').sumCongr 1) = sign (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)]

Result:
no goals

Proof state:
case left.refine_1
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (sumCongr 1 1) = sign 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
this : sign (σa.sumCongr 1) = sign σa ∧ sign (sumCongr 1 σb) = sign σb
⊢ sign (σa.sumCongr σb) = sign σa * sign σb

Tactic:
rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]

Result:
no goals

Proof state:
case right.refine_1
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (sumCongr 1 1) = sign 1

Tactic:
simp

Result:
no goals

Proof state:
case left
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr 1) = sign σa

Tactic:
refine σa.swap_induction_on ?_ fun σa' a₁ a₂ ha ih => ?_

Result:
case left.refine_1
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (sumCongr 1 1) = sign 1

case left.refine_2
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign ((swap a₁ a₂ * σa').sumCongr 1) = sign (swap a₁ a₂ * σa')

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr 1) = sign σa ∧ sign (sumCongr 1 σb) = sign σb

Tactic:
constructor

Result:
case left
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr 1) = sign σa

case right
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (sumCongr 1 σb) = sign σb

Proof state:
case right.refine_2
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ sign (sumCongr 1 (swap b₁ b₂ * σb')) = sign (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)]

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr σb) = sign σa * sign σb

Tactic:
suffices sign (sumCongr σa (1 : Perm β)) = sign σa ∧ sign (sumCongr (1 : Perm α) σb) = sign σb
  by rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]

Result:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr 1) = sign σa ∧ sign (sumCongr 1 σb) = sign σb