case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : z = x
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)

case neg
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
by_cases hx:z = x
case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : z = y
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)

case neg
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : ¬z = y
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
case neg
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
by_cases hy:z = y
no goals
case neg
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : ¬z = y
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
rw [Equiv.swap_apply_of_ne_of_ne hx hy, Equiv.swap_apply_of_ne_of_ne (hf.ne hx) (hf.ne hy)]
no goals
case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : z = x
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
simp [hx]
no goals
case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : z = y
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
simp [hy]