case h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ((fun x' => if h : x' ≠ x then f { val := x', property := h } else y) ∘ Subtype.val) x' = f x'
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
⊢ (fun x' => if h : x' ≠ x then f { val := x', property := h } else y) ∘ Subtype.val = f
funext x'
case h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ↑x' = x → y = f x'
case h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ((fun x' => if h : x' ≠ x then f { val := x', property := h } else y) ∘ Subtype.val) x' = f x'
simp only [ne_eq, dite_not, comp_apply, Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
case h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ y = f x'
case h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ↑x' = x → y = f x'
intro w
case h.h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ False
case h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ y = f x'
exfalso
no goals
case h.h
X : Sort ?u.87976
inst✝ : DecidableEq X
x : X
Y : Sort ?u.88012
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ False
exact x'.property w