Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-

! This file was ported from Lean 3 source module data.set.constructions
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Basic

/-!
# Constructions involving sets of sets.

## Finite Intersections

We define a structure `FiniteInter` which asserts that a set `S` of subsets of `α` is
closed under finite intersections.

We define `finiteInterClosure` which, given a set `S` of subsets of `α`, is the smallest
set of subsets of `α` which is closed under finite intersections.

`finiteInterClosure S` is endowed with a term of type `FiniteInter` using
`finiteInterClosure_finiteInter`.

-/

variable {α: Type ?u.169α : Type _: Type (?u.497+1)Type _} (S: Set (Set α)S : Set: Type ?u.500 → Type ?u.500Set (Set: Type ?u.180 → Type ?u.180Set α: Type ?u.490α))

/-- A structure encapsulating the fact that a set of sets is closed under finite intersection. -/
structure FiniteInter: {α : Type u_1} → Set (Set α) → PropFiniteInter : Prop: TypeProp where
/-- `univ_mem` states that `Set.univ` is in `S`. -/
univ_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ Suniv_mem : Set.univ: {α : Type ?u.34} → Set αSet.univ ∈ S: Set (Set α)S
/-- `inter_mem` states that any two intersections of sets in `S` is also in `S`. -/
inter_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ Sinter_mem : ∀ ⦃s: ?m.54s⦄, s: ?m.54s ∈ S: Set (Set α)S → ∀ ⦃t: ?m.86t⦄, t: ?m.86t ∈ S: Set (Set α)S → s: ?m.54s ∩ t: ?m.86t ∈ S: Set (Set α)S
#align has_finite_inter FiniteInter: {α : Type u_1} → Set (Set α) → PropFiniteInter

namespace FiniteInter

/-- The smallest set of sets containing `S` which is closed under finite intersections. -/
inductive finiteInterClosure: Set (Set α)finiteInterClosure : Set: Type ?u.183 → Type ?u.183Set (Set: Type ?u.184 → Type ?u.184Set α: Type ?u.176α)
| basic: ∀ {α : Type u_1} {S : Set (Set α)} {s : Set α}, s ∈ S → finiteInterClosure S sbasic {s: ?m.189s} : s: ?m.189s ∈ S: Set (Set α)S → finiteInterClosure: Set (Set α)finiteInterClosure s: ?m.189s
| univ: ∀ {α : Type u_1} {S : Set (Set α)}, finiteInterClosure S Set.univuniv : finiteInterClosure: Set (Set α)finiteInterClosure Set.univ: {α : Type ?u.230} → Set αSet.univ
| inter: ∀ {α : Type u_1} {S : Set (Set α)} {s t : Set α},
finiteInterClosure S s → finiteInterClosure S t → finiteInterClosure S (s ∩ t)inter {s: ?m.234s t: ?m.237t} : finiteInterClosure: Set (Set α)finiteInterClosure s: ?m.234s → finiteInterClosure: Set (Set α)finiteInterClosure t: ?m.237t → finiteInterClosure: Set (Set α)finiteInterClosure (s: ?m.234s ∩ t: ?m.237t)
#align has_finite_inter.finite_inter_closure FiniteInter.finiteInterClosure: {α : Type u_1} → Set (Set α) → Set (Set α)FiniteInter.finiteInterClosure

theorem finiteInterClosure_finiteInter: ∀ {α : Type u_1} (S : Set (Set α)), FiniteInter (finiteInterClosure S)finiteInterClosure_finiteInter : FiniteInter: {α : Type ?u.504} → Set (Set α) → PropFiniteInter (finiteInterClosure: {α : Type ?u.506} → Set (Set α) → Set (Set α)finiteInterClosure S: Set (Set α)S) :=
{ univ_mem := finiteInterClosure.univ: ∀ {α : Type ?u.522} {S : Set (Set α)}, finiteInterClosure S Set.univfiniteInterClosure.univ
inter_mem := fun _: ?m.532_ h: ?m.535h _: ?m.538_ => finiteInterClosure.inter: ∀ {α : Type ?u.540} {S : Set (Set α)} {s t : Set α},
finiteInterClosure S s → finiteInterClosure S t → finiteInterClosure S (s ∩ t)finiteInterClosure.inter h: ?m.535h }
#align has_finite_inter.finite_inter_closure_has_finite_inter FiniteInter.finiteInterClosure_finiteInter: ∀ {α : Type u_1} (S : Set (Set α)), FiniteInter (finiteInterClosure S)FiniteInter.finiteInterClosure_finiteInter

variable {S: ?m.574S}

theorem finiteInter_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ (F : Finset (Set α)), ↑F ⊆ S → ⋂₀ ↑F ∈ SfiniteInter_mem (cond: FiniteInter Scond : FiniteInter: {α : Type ?u.584} → Set (Set α) → PropFiniteInter S: Set (Set α)S) (F: Finset (Set α)F : Finset: Type ?u.591 → Type ?u.591Finset (Set: Type ?u.592 → Type ?u.592Set α: Type ?u.577α)) :
↑F: Finset (Set α)F ⊆ S: Set (Set α)S → ⋂₀ (↑F: Finset (Set α)F : Set: Type ?u.636 → Type ?u.636Set (Set: Type ?u.637 → Type ?u.637Set α: Type ?u.577α)) ∈ S: Set (Set α)S := byGoals accomplished! 🐙
α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)↑F ⊆ S → ⋂₀ ↑F ∈ Sclassical
α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)↑F ⊆ S → ⋂₀ ↑F ∈ Srefine' Finset.induction_on: ∀ {α : Type ?u.761} {p : Finset α → Prop} [inst : DecidableEq α] (s : Finset α),
p ∅ → (∀ ⦃a : α⦄ {s : Finset α}, ¬a ∈ s → p s → p (insert a s)) → p sFinset.induction_on F: Finset (Set α)F (fun _: ?m.970_ => _: ⋂₀ ↑∅ ∈ S_) _: ∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S_α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)x✝: ↑∅ ⊆ Srefine'_1⋂₀ ↑∅ ∈ Sα: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)refine'_2∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)↑F ⊆ S → ⋂₀ ↑F ∈ S·α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)x✝: ↑∅ ⊆ Srefine'_1⋂₀ ↑∅ ∈ S α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)x✝: ↑∅ ⊆ Srefine'_1⋂₀ ↑∅ ∈ Sα: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)refine'_2∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ Ssimp [cond: FiniteInter Scond.univ_mem: ∀ {α : Type ?u.977} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ Suniv_mem]Goals accomplished! 🐙
α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)↑F ⊆ S → ⋂₀ ↑F ∈ S·α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)refine'_2∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)refine'_2∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ Sintro a: Set αa s: Finset (Set α)s _: ¬a ∈ s_ h1: ↑s ⊆ S → ⋂₀ ↑s ∈ Sh1 h2: ↑(insert a s) ⊆ Sh2α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)a: Set αs: Finset (Set α)a✝: ¬a ∈ sh1: ↑s ⊆ S → ⋂₀ ↑s ∈ Sh2: ↑(insert a s) ⊆ Srefine'_2⋂₀ ↑(insert a s) ∈ S
α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)refine'_2∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ Ssuffices a: Set αa ∩ ⋂₀ ↑s: Finset (Set α)s ∈ S: Set (Set α)S by α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)a: Set αs: Finset (Set α)a✝: ¬a ∈ sh1: ↑s ⊆ S → ⋂₀ ↑s ∈ Sh2: ↑(insert a s) ⊆ Srefine'_2⋂₀ ↑(insert a s) ∈ SsimpaGoals accomplished! 🐙
α: Type u_1S: Set (Set α)cond: FiniteInter SF: Finset (Set α)refine'_2∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ Sexact
cond: FiniteInter Scond.inter_mem: ∀ {α : Type ?u.1565} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ Sinter_mem (h2: ↑(insert a s) ⊆ Sh2 (Finset.mem_insert_self: ∀ {α : Type ?u.1578} [inst : DecidableEq α] (a : α) (s : Finset α), a ∈ insert a sFinset.mem_insert_self a: Set αa s: Finset (Set α)s))
(h1: ↑s ⊆ S → ⋂₀ ↑s ∈ Sh1 fun x: ?m.1595x hx: ?m.1598hx => h2: ↑(insert a s) ⊆ Sh2 <| Finset.mem_insert_of_mem: ∀ {α : Type ?u.1601} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ s → a ∈ insert b sFinset.mem_insert_of_mem hx: ?m.1598hx)Goals accomplished! 🐙
#align has_finite_inter.finite_inter_mem FiniteInter.finiteInter_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ (F : Finset (Set α)), ↑F ⊆ S → ⋂₀ ↑F ∈ SFiniteInter.finiteInter_mem

theorem finiteInterClosure_insert: ∀ {A : Set α}, FiniteInter S → ∀ (P : Set α), P ∈ finiteInterClosure (insert A S) → P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ QfiniteInterClosure_insert {A: Set αA : Set: Type ?u.1703 → Type ?u.1703Set α: Type ?u.1696α} (cond: FiniteInter Scond : FiniteInter: {α : Type ?u.1706} → Set (Set α) → PropFiniteInter S: Set (Set α)S) (P: Set αP)
(H: P ∈ finiteInterClosure (insert A S)H : P: ?m.1713P ∈ finiteInterClosure: {α : Type ?u.1733} → Set (Set α) → Set (Set α)finiteInterClosure (insert: {α : outParam (Type ?u.1737)} → {γ : Type ?u.1736} → [self : Insert α γ] → α → γ → γinsert A: Set αA S: Set (Set α)S)) : P: ?m.1713P ∈ S: Set (Set α)S ∨ ∃ Q: ?m.1793Q ∈ S: Set (Set α)S, P: ?m.1713P = A: Set αA ∩ Q: ?m.1793Q := byGoals accomplished! 🐙
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αH: P ∈ finiteInterClosure (insert A S)P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Qinduction' H: P ∈ finiteInterClosure (insert A S)H with S: Set ?m.1865S h: S ∈ ?m.1866h T1: Set ?m.1865T1 T2: Set ?m.1865T2 _ _ h1: ?m.1867 T1 a✝¹h1 h2: ?m.1867 T2 a✝h2α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh: S ∈ insert A S✝basicS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αunivSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αH: P ∈ finiteInterClosure (insert A S)P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q·α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh: S ∈ insert A S✝basicS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh: S ∈ insert A S✝basicS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αunivSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qcases h: S ∈ ?m.1866hα: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S = Abasic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qα: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S ∈ S✝basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh: S ∈ insert A S✝basicS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q·α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S = Abasic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S = Abasic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qα: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S ∈ S✝basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr ⟨Set.univ: {α : Type ?u.1969} → Set αSet.univ, cond: FiniteInter S✝cond.univ_mem: ∀ {α : Type ?u.1980} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ Suniv_mem, α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S = Abasic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ QbyGoals accomplished! 🐙 α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S = AS = A ∩ Set.univsimpaGoals accomplished! 🐙⟩Goals accomplished! 🐙
α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh: S ∈ insert A S✝basicS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q·α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S ∈ S✝basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S ∈ S✝basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl (α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S ∈ S✝basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ QbyGoals accomplished! 🐙 α: Type u_1S✝: Set (Set α)A: Set αcond: FiniteInter S✝P, S: Set αh✝: S ∈ S✝S ∈ S✝assumptionGoals accomplished! 🐙)Goals accomplished! 🐙
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αH: P ∈ finiteInterClosure (insert A S)P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q·α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αunivSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αunivSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl cond: FiniteInter Scond.univ_mem: ∀ {α : Type ?u.2085} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ Suniv_memGoals accomplished! 🐙
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP: Set αH: P ∈ finiteInterClosure (insert A S)P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q·α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qrcases h1: ?m.1867 T1 a✝¹h1 with (h | ⟨Q, hQ, rfl⟩): ?m.1867 T1 a✝¹(h: T1 ∈ Shh | ⟨Q, hQ, rfl⟩: ?m.1867 T1 a✝¹ | ⟨Q, hQ, rfl⟩: ∃ Q, Q ∈ S ∧ T1 = A ∩ Q⟨Q: Set αQ⟨Q, hQ, rfl⟩: ∃ Q, Q ∈ S ∧ T1 = A ∩ Q, hQ: Q ∈ ShQ⟨Q, hQ, rfl⟩: ∃ Q, Q ∈ S ∧ T1 = A ∩ Q, rfl: T1 = A ∩ Qrfl⟨Q, hQ, rfl⟩: ∃ Q, Q ∈ S ∧ T1 = A ∩ Q⟩(h | ⟨Q, hQ, rfl⟩): ?m.1867 T1 a✝¹)α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Qh: T1 ∈ Sinter.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QQ: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)inter.inr.intro.introA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1 α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q<;>α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Qh: T1 ∈ Sinter.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QQ: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)inter.inr.intro.introA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1 α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qrcases h2: ?m.1867 T2 a✝¹h2 with (i | ⟨R, hR, rfl⟩): ?m.1867 T2 a✝¹(i: T2 ∈ Sii | ⟨R, hR, rfl⟩: ?m.1867 T2 a✝¹ | ⟨R, hR, rfl⟩: ∃ Q, Q ∈ S ∧ T2 = A ∩ Q⟨R: Set αR⟨R, hR, rfl⟩: ∃ Q, Q ∈ S ∧ T2 = A ∩ Q, hR: R ∈ ShR⟨R, hR, rfl⟩: ∃ Q, Q ∈ S ∧ T2 = A ∩ Q, rfl: T2 = A ∩ Rrfl⟨R, hR, rfl⟩: ∃ Q, Q ∈ S ∧ T2 = A ∩ Q⟩(i | ⟨R, hR, rfl⟩): ?m.1867 T2 a✝¹)α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h: T1 ∈ Si: T2 ∈ Sinter.inl.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1: Set αa✝¹: finiteInterClosure (insert A S) T1h: T1 ∈ SR: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h: T1 ∈ Si: T2 ∈ Sinter.inl.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h: T1 ∈ Si: T2 ∈ Sinter.inl.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1: Set αa✝¹: finiteInterClosure (insert A S) T1h: T1 ∈ SR: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2Q: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)i: T2 ∈ Sinter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inr.intro.intro.inr.intro.introA ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1exact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl (cond: FiniteInter Scond.inter_mem: ∀ {α : Type ?u.2330} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ Sinter_mem h: T1 ∈ Sh i: T2 ∈ Si)Goals accomplished! 🐙
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1: Set αa✝¹: finiteInterClosure (insert A S) T1h: T1 ∈ SR: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1: Set αa✝¹: finiteInterClosure (insert A S) T1h: T1 ∈ SR: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Qα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2Q: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)i: T2 ∈ Sinter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inr.intro.intro.inr.intro.introA ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1exact
Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr ⟨T1: Set ?m.1865T1 ∩ R: Set αR, cond: FiniteInter Scond.inter_mem: ∀ {α : Type ?u.2379} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ Sinter_mem h: T1 ∈ Sh hR: R ∈ ShR, α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1: Set αa✝¹: finiteInterClosure (insert A S) T1h: T1 ∈ SR: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ QbyGoals accomplished! 🐙 α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1: Set αa✝¹: finiteInterClosure (insert A S) T1h: T1 ∈ SR: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)T1 ∩ (A ∩ R) = A ∩ (T1 ∩ R)simp only [← Set.inter_assoc: ∀ {α : Type ?u.2396} (a b c : Set α), a ∩ b ∩ c = a ∩ (b ∩ c)Set.inter_assoc, Set.inter_comm: ∀ {α : Type ?u.2416} (a b : Set α), a ∩ b = b ∩ aSet.inter_comm _: Set ?m.2417_ A: Set αA]Goals accomplished! 🐙⟩Goals accomplished! 🐙
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2Q: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)i: T2 ∈ Sinter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1 α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2Q: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)i: T2 ∈ Sinter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inr.intro.intro.inr.intro.introA ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1exact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr ⟨Q: Set αQ ∩ T2: Set ?m.1865T2, cond: FiniteInter Scond.inter_mem: ∀ {α : Type ?u.2537} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ Sinter_mem hQ: Q ∈ ShQ i: T2 ∈ Si, α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2Q: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)i: T2 ∈ Sinter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1byGoals accomplished! 🐙 α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T2: Set αa✝¹: finiteInterClosure (insert A S) T2Q: Set αhQ: Q ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ Q)i: T2 ∈ SA ∩ Q ∩ T2 = A ∩ (Q ∩ T2)simp only [Set.inter_assoc: ∀ {α : Type ?u.2566} (a b c : Set α), a ∩ b ∩ c = a ∩ (b ∩ c)Set.inter_assoc]Goals accomplished! 🐙⟩Goals accomplished! 🐙
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, T1, T2: Set αa✝¹: finiteInterClosure (insert A S) T1a✝: finiteInterClosure (insert A S) T2h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Qh2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ QinterT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inr.intro.intro.inr.intro.introA ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1 α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inr.intro.intro.inr.intro.introA ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1exact
Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr
⟨Q: Set αQ ∩ R: Set αR, cond: FiniteInter Scond.inter_mem: ∀ {α : Type ?u.2624} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ Sinter_mem hQ: Q ∈ ShQ hR: R ∈ ShR, α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)inter.inr.intro.intro.inr.intro.introA ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1byGoals accomplished! 🐙
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)ext x: ?αxα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)x: αhx ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)constructorα: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)x: αh.mpx ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)x: αh.mprx ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R) α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)x: αhx ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)<;>α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)x: αh.mpx ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)x: αh.mprx ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R) α: Type u_1S: Set (Set α)A: Set αcond: FiniteInter SP, Q: Set αhQ: Q ∈ Sa✝¹: finiteInterClosure (insert A S) (A ∩ Q)R: Set αhR: R ∈ Sa✝: finiteInterClosure (insert A S) (A ∩ R)x: αhx ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)simp (config := { contextual := true: Booltrue })Goals accomplished! 🐙⟩Goals accomplished! 🐙
#align has_finite_inter.finite_inter_closure_insert FiniteInter.finiteInterClosure_insert: ∀ {α : Type u_1} {S : Set (Set α)} {A : Set α},
FiniteInter S → ∀ (P : Set α), P ∈ finiteInterClosure (insert A S) → P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ QFiniteInter.finiteInterClosure_insert

end FiniteInter
```