case H
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
x : α ⊕ β
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) x = ↑(swap (Sum.inl i) (Sum.inl j)) x
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
⊢ sumCongr (swap i j) (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)
ext x
case H.inl
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) (Sum.inl val✝) = ↑(swap (Sum.inl i) (Sum.inl j)) (Sum.inl val✝)

case H.inr
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
val✝ : β
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) (Sum.inr val✝) = ↑(swap (Sum.inl i) (Sum.inl j)) (Sum.inr val✝)
case H
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
x : α ⊕ β
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) x = ↑(swap (Sum.inl i) (Sum.inl j)) x
cases x
case H.inl
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ Sum.inl (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inl j else if val✝ = j then Sum.inl i else Sum.inl val✝
case H.inl
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) (Sum.inl val✝) = ↑(swap (Sum.inl i) (Sum.inl j)) (Sum.inl val✝)
simp only [Equiv.sumCongr_apply, Sum.map, coe_refl, comp.right_id, Sum.elim_inl, comp_apply,
  swap_apply_def, Sum.inl.injEq]
no goals
case H.inl
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ Sum.inl (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inl j else if val✝ = j then Sum.inl i else Sum.inl val✝
split_ifs <;> rfl
no goals
case H.inr
α✝ : Sort ?u.117460
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
val✝ : β
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) (Sum.inr val✝) = ↑(swap (Sum.inl i) (Sum.inl j)) (Sum.inr val✝)
simp [Sum.map, swap_apply_of_ne_of_ne]