α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f (↑(Equiv.swap x y) z) = if f z = f x then f y else if f z = f y then f x else f z
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f (↑(Equiv.swap x y) z) = ↑(Equiv.swap (f x) (f y)) (f z)
conv_rhs => rw [Equiv.swap_apply_def]
case inl
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : f z = f x
⊢ f (↑(Equiv.swap x y) z) = f y

case inr.inl
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : f z = f y
⊢ f (↑(Equiv.swap x y) z) = f x

case inr.inr
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : ¬f z = f y
⊢ f (↑(Equiv.swap x y) z) = f z
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f (↑(Equiv.swap x y) z) = if f z = f x then f y else if f z = f y then f x else f z
split_ifs with h₁ h₂
no goals
case inl
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : f z = f x
⊢ f (↑(Equiv.swap x y) z) = f y
rw [hf h₁, Equiv.swap_apply_left]
no goals
case inr.inl
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : f z = f y
⊢ f (↑(Equiv.swap x y) z) = f x
rw [hf h₂, Equiv.swap_apply_right]
no goals
case inr.inr
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : ¬f z = f y
⊢ f (↑(Equiv.swap x y) z) = f z
rw [Equiv.swap_apply_of_ne_of_ne (mt (congr_arg f) h₁) (mt (congr_arg f) h₂)]