chore(data/set/constructions): Make has_finite_inter Prop-valued (#17824)

YaelDillies · YaelDillies · commit a95b16cbade0 · 2022-12-06T00:34:20.000Z
`has_finite_inter` was accidentally defined to be Type-valued, despite only having propositional fields.
diff --git a/src/data/set/constructions.lean b/src/data/set/constructions.lean
@@ -24,24 +24,19 @@ set of subsets of `α` which is closed under finite intersections.
 variables {α : Type*} (S : set (set α))
 
 /-- A structure encapsulating the fact that a set of sets is closed under finite intersection. -/
-structure has_finite_inter :=
+structure has_finite_inter : Prop :=
 (univ_mem : set.univ ∈ S)
 (inter_mem : ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ t ∈ S)
 
 namespace has_finite_inter
 
--- Satisfying the inhabited linter...
-instance : inhabited (has_finite_inter ({set.univ} : set (set α))) :=
-⟨⟨by tauto, λ _ h1 _ h2, by simp [set.mem_singleton_iff.1 h1, set.mem_singleton_iff.1 h2]⟩⟩
-
 /-- The smallest set of sets containing `S` which is closed under finite intersections. -/
 inductive finite_inter_closure : set (set α)
 | basic {s} : s ∈ S → finite_inter_closure s
 | univ : finite_inter_closure set.univ
 | inter {s t} : finite_inter_closure s → finite_inter_closure t → finite_inter_closure (s ∩ t)
 
-/-- Defines `has_finite_inter` for `finite_inter_closure S`. -/
-def finite_inter_closure_has_finite_inter : has_finite_inter (finite_inter_closure S) :=
+lemma finite_inter_closure_has_finite_inter : has_finite_inter (finite_inter_closure S) :=
 { univ_mem := finite_inter_closure.univ,
   inter_mem := λ _ h _, finite_inter_closure.inter h }
 
