α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa 1) = ↑sign σa ∧ ↑sign (sumCongr 1 σb) = ↑sign σb
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa σb) = ↑sign σa * ↑sign σb
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]
case left
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa 1) = ↑sign σa

case right
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 σb) = ↑sign σb
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa 1) = ↑sign σa ∧ ↑sign (sumCongr 1 σb) = ↑sign σb
constructor
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
this : ↑sign (sumCongr σa 1) = ↑sign σa ∧ ↑sign (sumCongr 1 σb) = ↑sign σb
⊢ ↑sign (sumCongr σa σb) = ↑sign σa * ↑sign σb
rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
case left.refine'_1
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 1) = ↑sign 1

case left.refine'_2
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : ↑sign (sumCongr σa' 1) = ↑sign σa'
⊢ ↑sign (sumCongr (swap a₁ a₂ * σa') 1) = ↑sign (swap a₁ a₂ * σa')
case left
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa 1) = ↑sign σa
refine' σa.swap_induction_on ?_ fun σa' a₁ a₂ ha ih => ?_
no goals
case left.refine'_1
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 1) = ↑sign 1
simp
no goals
case left.refine'_2
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : ↑sign (sumCongr σa' 1) = ↑sign σa'
⊢ ↑sign (sumCongr (swap a₁ a₂ * σa') 1) = ↑sign (swap a₁ a₂ * σa')
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)]
case right.refine'_1
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 1) = ↑sign 1

case right.refine'_2
α : Type u
β : Type v
inst✝³ : DecidableEq α
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')
case right
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 σb) = ↑sign σb
refine' σb.swap_induction_on ?_ fun σb' b₁ b₂ hb ih => ?_
no goals
case right.refine'_1
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 1) = ↑sign 1
simp
no goals
case right.refine'_2
α : Type u
β : Type v
inst✝³ : DecidableEq α
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')
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)]