α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ { fst := fun b => out { fst := s, snd := h } = b,
      snd := (_ : ∃ a, (fun b => a = b) = fun b => out { fst := s, snd := h } = b) } =
    { fst := s, snd := h }
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ mk (out { fst := s, snd := h }) = { fst := s, snd := h }
simp [mk]
case e_fst
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ (fun b => out { fst := s, snd := h } = b) = s
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ { fst := fun b => out { fst := s, snd := h } = b,
      snd := (_ : ∃ a, (fun b => a = b) = fun b => out { fst := s, snd := h } = b) } =
    { fst := s, snd := h }
congr
no goals
case e_fst
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ (fun b => out { fst := s, snd := h } = b) = s
exact Classical.choose_spec h