α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
⊢ ((fun a x => f a) ∈ pi s fun a => {f a}) ∧ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
⊢ (pi s fun a => {f a}) = {fun a x => f a}
rw [eq_singleton_iff_unique_mem]
case left
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
⊢ (fun a x => f a) ∈ pi s fun a => {f a}

case right
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
⊢ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
⊢ ((fun a x => f a) ∈ pi s fun a => {f a}) ∧ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
constructor
case right
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
⊢ a = fun a x => f a
case right
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
⊢ ∀ (x : (a : α) → a ∈ s → β), (x ∈ pi s fun a => {f a}) → x = fun a x => f a
intro a ha
case right.h.h
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
i : α
hi : i ∈ s
⊢ a i hi = f i
case right
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
⊢ a = fun a x => f a
ext (i hi)
case right.h.h
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : ∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h ∈ {f a_1}
i : α
hi : i ∈ s
⊢ a i hi = f i
case right.h.h
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : a ∈ pi s fun a => {f a}
i : α
hi : i ∈ s
⊢ a i hi = f i
rw [mem_pi] at ha
no goals
case right.h.h
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
a : (a : α) → a ∈ s → β
ha : ∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h ∈ {f a_1}
i : α
hi : i ∈ s
⊢ a i hi = f i
simpa using ha i hi
no goals
case left
α : Type u_2
β✝ : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
β : Type u_1
s : Finset α
f : α → β
⊢ (fun a x => f a) ∈ pi s fun a => {f a}
simp