α✝ : Sort ?u.6831
β✝ : Sort ?u.6834
γ : Sort ?u.6837
p✝ q : α✝ → Prop
α : Sort u_1
β : α → Type u_2
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
⊢ Surjective fun f => restrict p f
α✝ : Sort ?u.6831
β✝ : Sort ?u.6834
γ : Sort ?u.6837
p✝ q : α✝ → Prop
α : Sort u_1
β : α → Type u_2
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
⊢ Surjective fun f => restrict p f
letI := Classical.decPred p
α✝ : Sort ?u.6831
β✝ : Sort ?u.6834
γ : Sort ?u.6837
p✝ q : α✝ → Prop
α : Sort u_1
β : α → Type u_2
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
⊢ ∀ (x : Subtype p),
    (fun f => restrict p f)
        (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x))) x =
      f x
α✝ : Sort ?u.6831
β✝ : Sort ?u.6834
γ : Sort ?u.6837
p✝ q : α✝ → Prop
α : Sort u_1
β : α → Type u_2
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
⊢ Surjective fun f => restrict p f
refine' fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), funext <| _⟩
case mk
α✝ : Sort ?u.6831
β✝ : Sort ?u.6834
γ : Sort ?u.6837
p✝ q : α✝ → Prop
α : Sort u_1
β : α → Type u_2
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
x : α
hx : p x
⊢ (fun f => restrict p f)
      (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x)))
      { val := x, property := hx } =
    f { val := x, property := hx }
α✝ : Sort ?u.6831
β✝ : Sort ?u.6834
γ : Sort ?u.6837
p✝ q : α✝ → Prop
α : Sort u_1
β : α → Type u_2
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
⊢ ∀ (x : Subtype p),
    (fun f => restrict p f)
        (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x))) x =
      f x
rintro ⟨x, hx⟩
no goals
case mk
α✝ : Sort ?u.6831
β✝ : Sort ?u.6834
γ : Sort ?u.6837
p✝ q : α✝ → Prop
α : Sort u_1
β : α → Type u_2
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
x : α
hx : p x
⊢ (fun f => restrict p f)
      (fun x => if h : p x then f { val := x, property := h } else Nonempty.some (_ : Nonempty (β x)))
      { val := x, property := hx } =
    f { val := x, property := hx }
exact dif_pos hx