α : Type ?u.4851
β : Type ?u.4854
I : Type u_2
f : I → Type u_1
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)
α : Type ?u.4851
β : Type ?u.4854
I : Type u_2
f : I → Type u_1
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)
letI := Classical.decEq (∀ i : I, f i)
no goals
α : Type ?u.4851
β : Type ?u.4854
I : Type u_2
f : I → Type u_1
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)
exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial