no goals
α✝ : Type ?u.144755
β : Type ?u.144758
γ : Type ?u.144761
inst✝³ : Fintype α✝
p✝ : α✝ → Prop
inst✝² : DecidablePred p✝
α : Type ?u.144781
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x y : { a // p a }
hy : (fun a => ↑a = ↑x) y
⊢ y = x
simpa [Subtype.ext_iff] using hy
no goals
α✝ : Type ?u.144755
β : Type ?u.144758
γ : Type ?u.144761
inst✝³ : Fintype α✝
p✝ : α✝ → Prop
inst✝² : DecidablePred p✝
α : Type u_1
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x : { a // p a }
h : optParam (∃! a, ↑a = ↑x) (_ : ∃ x_1, (fun a => ↑a = ↑x) x_1 ∧ ∀ (y : { a // p a }), (fun a => ↑a = ↑x) y → y = x_1)
⊢ choose (fun y => ↑y = ↑x) h = x
rw [Subtype.ext_iff, Fintype.choose_spec (fun y : { a : α // p a } => (y : α) = x) _]