α : Type u_2
β : Type u_1
γ : Type ?u.28780
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑b = x → False
α : Type u_2
β : Type u_1
γ : Type ?u.28780
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑(↑(↑(optionSubtype x).symm e)).symm ↑b = some (↑e.symm b)
simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
           Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.28780
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑b = x → False
exact fun h => False.elim (b.property h)