case mk
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
toFun✝ invFun✝ : α → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ ↑({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (swap a b)) x =
    if ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = a then b
    else
      if ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = b then a
      else ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
π : Perm α
⊢ ↑(π.trans (swap a b)) x = if ↑π x = a then b else if ↑π x = b then a else ↑π x
cases π
no goals
case mk
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
toFun✝ invFun✝ : α → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ ↑({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (swap a b)) x =
    if ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = a then b
    else
      if ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = b then a
      else ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x
rfl