α✝ : Type ?u.198791
β : Type ?u.198794
β₂ : Type ?u.198797
γ : Type ?u.198800
ι : Sort ?u.198803
ι' : Sort ?u.198806
κ : ι → Sort ?u.198811
κ' : ι' → Sort ?u.198816
α : Type u_1
s : Set (α → Prop)
a : α
⊢ (⨅ (f : ↑s), ↑f a) ↔ ∀ (r : α → Prop), r ∈ s → r a
α✝ : Type ?u.198791
β : Type ?u.198794
β₂ : Type ?u.198797
γ : Type ?u.198800
ι : Sort ?u.198803
ι' : Sort ?u.198806
κ : ι → Sort ?u.198811
κ' : ι' → Sort ?u.198816
α : Type u_1
s : Set (α → Prop)
a : α
⊢ sInf s a ↔ ∀ (r : α → Prop), r ∈ s → r a
rw [sInf_apply]
no goals
α✝ : Type ?u.198791
β : Type ?u.198794
β₂ : Type ?u.198797
γ : Type ?u.198800
ι : Sort ?u.198803
ι' : Sort ?u.198806
κ : ι → Sort ?u.198811
κ' : ι' → Sort ?u.198816
α : Type u_1
s : Set (α → Prop)
a : α
⊢ (⨅ (f : ↑s), ↑f a) ↔ ∀ (r : α → Prop), r ∈ s → r a
simp [← eq_iff_iff]