case h.e'_1.h.e'_1
α : Sort ?u.67949
β : Sort ?u.67953
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (↑e a)
a : β
⊢ a = ↑e (↑e.symm a)
α : Sort ?u.67949
β : Sort ?u.67953
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (↑e a)
a : β
⊢ q a ↔ p (↑e.symm a)
convert (h <| e.symm a).symm
no goals
case h.e'_1.h.e'_1
α : Sort ?u.67949
β : Sort ?u.67953
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (↑e a)
a : β
⊢ a = ↑e (↑e.symm a)
exact (e.apply_symm_apply a).symm