case pos
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : k = i
⊢ v (↑(swap i j) k) = v k

case neg
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
⊢ v (↑(swap i j) k) = v k
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
⊢ v (↑(swap i j) k) = v k
by_cases hi : k = i
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : k = j
⊢ v (↑(swap i j) k) = v k

case neg
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : ¬k = j
⊢ v (↑(swap i j) k) = v k
case neg
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
⊢ v (↑(swap i j) k) = v k
by_cases hj : k = j
no goals
case neg
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : ¬k = j
⊢ v (↑(swap i j) k) = v k
rw [swap_apply_of_ne_of_ne hi hj]
no goals
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : k = i
⊢ v (↑(swap i j) k) = v k
rw [hi, swap_apply_left, hv]
no goals
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : k = j
⊢ v (↑(swap i j) k) = v k
rw [hj, swap_apply_right, hv]