α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
⊢ ↑((e.symm.trans (swap a b)).trans e) x = ↑(swap (↑e a) (↑e b)) x
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
⊢ ↑((e.symm.trans (swap a b)).trans e) x = ↑(swap (↑e a) (↑e b)) x
have : ∀ a, e.symm x = a ↔ x = e a := fun a => by
  rw [@eq_comm _ (e.symm x)]
  constructor <;> intros <;> simp_all
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
⊢ ↑e (if x = ↑e a then b else if x = ↑e b then a else ↑e.symm x) =
    if x = ↑e a then ↑e b else if x = ↑e b then ↑e a else x
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
⊢ ↑((e.symm.trans (swap a b)).trans e) x = ↑(swap (↑e a) (↑e b)) x
simp [trans_apply, swap_apply_def, this]
no goals
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
⊢ ↑e (if x = ↑e a then b else if x = ↑e b then a else ↑e.symm x) =
    if x = ↑e a then ↑e b else if x = ↑e b then ↑e a else x
split_ifs <;> simp
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : (fun x => α) x
⊢ a = ↑e.symm x ↔ x = ↑e a
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : (fun x => α) x
⊢ ↑e.symm x = a ↔ x = ↑e a
rw [@eq_comm _ (e.symm x)]
no goals
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : (fun x => α) x
⊢ a = ↑e.symm x ↔ x = ↑e a
constructor <;> intros <;> simp_all