/-
Copyright (c) 2020 Adam Topaz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Topaz

! 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.500
Set (Set: Type ?u.180 → Type ?u.180
Set α: 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 α) → Prop
FiniteInter : Prop: Type
Prop where
  /-- `univ_mem` states that `Set.univ` is in `S`. -/
  univ_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ S
univ_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 ∈ S
inter_mem : ∀ ⦃s: ?m.54
s⦄, s: ?m.54
s ∈ S: Set (Set α)
S → ∀ ⦃t: ?m.86
t⦄, t: ?m.86
t ∈ S: Set (Set α)
S → s: ?m.54
s ∩ t: ?m.86
t ∈ S: Set (Set α)
S
#align has_finite_inter FiniteInter: {α : Type u_1} → Set (Set α) → Prop
FiniteInter

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.183
Set (Set: Type ?u.184 → Type ?u.184
Set α: Type ?u.176
α)
  | basic: ∀ {α : Type u_1} {S : Set (Set α)} {s : Set α}, s ∈ S → finiteInterClosure S s
basic {s: ?m.189
s} : s: ?m.189
s ∈ S: Set (Set α)
S → finiteInterClosure: Set (Set α)
finiteInterClosure s: ?m.189
s
  | univ: ∀ {α : Type u_1} {S : Set (Set α)}, finiteInterClosure S Set.univ
univ : 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.234
s t: ?m.237
t} : finiteInterClosure: Set (Set α)
finiteInterClosure s: ?m.234
s → finiteInterClosure: Set (Set α)
finiteInterClosure t: ?m.237
t → finiteInterClosure: Set (Set α)
finiteInterClosure (s: ?m.234
s ∩ t: ?m.237
t)
#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 α) → Prop
FiniteInter (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.univ
finiteInterClosure.univ
    inter_mem := fun _: ?m.532
_ h: ?m.535
h _: ?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.535
h }
#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.574
S}

theorem finiteInter_mem: ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ (F : Finset (Set α)), ↑F ⊆ S → ⋂₀ ↑F ∈ S
finiteInter_mem (cond: FiniteInter S
cond : FiniteInter: {α : Type ?u.584} → Set (Set α) → Prop
FiniteInter S: Set (Set α)
S) (F: Finset (Set α)
F : Finset: Type ?u.591 → Type ?u.591
Finset (Set: Type ?u.592 → Type ?u.592
Set α: Type ?u.577
α)) :
    ↑F: Finset (Set α)
F ⊆ S: Set (Set α)
S → ⋂₀ (↑F: Finset (Set α)
F : Set: Type ?u.636 → Type ?u.636
Set (Set: Type ?u.637 → Type ?u.637
Set α: Type ?u.577
α)) ∈ S: Set (Set α)
S := by
Goals accomplished! 🐙
  α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

↑F ⊆ S → ⋂₀ ↑F ∈ Sclassical
    α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: 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 s
Finset.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_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

x✝: ↑∅ ⊆ S

refine'_1⋂₀ ↑∅ ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: 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_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

↑F ⊆ S → ⋂₀ ↑F ∈ S·α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

x✝: ↑∅ ⊆ S

refine'_1⋂₀ ↑∅ ∈ S α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

x✝: ↑∅ ⊆ S

refine'_1⋂₀ ↑∅ ∈ S
α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: 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 S
cond.univ_mem: ∀ {α : Type ?u.977} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ S
univ_mem]
Goals accomplished! 🐙
    α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

↑F ⊆ S → ⋂₀ ↑F ∈ S·α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: 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_1

S: Set (Set α)

cond: FiniteInter S

F: 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 ∈ S
h1 h2: ↑(insert a s) ⊆ S
h2α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

a: Set α

s: Finset (Set α)

a✝: ¬a ∈ s

h1: ↑s ⊆ S → ⋂₀ ↑s ∈ S

h2: ↑(insert a s) ⊆ S

refine'_2⋂₀ ↑(insert a s) ∈ S
      α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: 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_1

S: Set (Set α)

cond: FiniteInter S

F: Finset (Set α)

a: Set α

s: Finset (Set α)

a✝: ¬a ∈ s

h1: ↑s ⊆ S → ⋂₀ ↑s ∈ S

h2: ↑(insert a s) ⊆ S

refine'_2⋂₀ ↑(insert a s) ∈ Ssimpa
Goals accomplished! 🐙
      α: Type u_1

S: Set (Set α)

cond: FiniteInter S

F: 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 S
cond.inter_mem: ∀ {α : Type ?u.1565} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
inter_mem (h2: ↑(insert a s) ⊆ S
h2 (Finset.mem_insert_self: ∀ {α : Type ?u.1578} [inst : DecidableEq α] (a : α) (s : Finset α), a ∈ insert a s
Finset.mem_insert_self a: Set α
a s: Finset (Set α)
s))
          (h1: ↑s ⊆ S → ⋂₀ ↑s ∈ S
h1 fun x: ?m.1595
x hx: ?m.1598
hx => h2: ↑(insert a s) ⊆ S
h2 <| Finset.mem_insert_of_mem: ∀ {α : Type ?u.1601} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ s → a ∈ insert b s
Finset.mem_insert_of_mem hx: ?m.1598
hx)
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 ∈ S
FiniteInter.finiteInter_mem

theorem finiteInterClosure_insert: ∀ {A : Set α}, FiniteInter S → ∀ (P : Set α), P ∈ finiteInterClosure (insert A S) → P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
finiteInterClosure_insert {A: Set α
A : Set: Type ?u.1703 → Type ?u.1703
Set α: Type ?u.1696
α} (cond: FiniteInter S
cond : FiniteInter: {α : Type ?u.1706} → Set (Set α) → Prop
FiniteInter S: Set (Set α)
S) (P: Set α
P)
    (H: P ∈ finiteInterClosure (insert A S)
H : P: ?m.1713
P ∈ 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.1713
P ∈ S: Set (Set α)
S ∨ ∃ Q: ?m.1793
Q ∈ S: Set (Set α)
S, P: ?m.1713
P = A: Set α
A ∩ Q: ?m.1793
Q := by
Goals accomplished! 🐙
  α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: 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.1865
S h: S ∈ ?m.1866
h T1: Set ?m.1865
T1 T2: Set ?m.1865
T2 _ _ h1: ?m.1867 T1 a✝¹
h1 h2: ?m.1867 T2 a✝
h2α: Type u_1

S✝: 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_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

univSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
  α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

H: P ∈ finiteInterClosure (insert A S)

P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q·α: Type u_1

S✝: 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_1

S✝: 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_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

univSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qcases h: S ∈ ?m.1866
hα: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A

basic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝

basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
    α: Type u_1

S✝: 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_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A

basic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A

basic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
α: Type u_1

S✝: 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 ∨ b
Or.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 ∈ S
univ_mem, α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A

basic.inlS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qby
Goals accomplished! 🐙 α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S = A

S = A ∩ Set.univsimpa
Goals accomplished! 🐙⟩
Goals accomplished! 🐙
    α: Type u_1

S✝: 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_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝

basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q α: Type u_1

S✝: 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 ∨ b
Or.inl (α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝

basic.inrS ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Qby
Goals accomplished! 🐙 α: Type u_1

S✝: Set (Set α)

A: Set α

cond: FiniteInter S✝

P, S: Set α

h✝: S ∈ S✝

S ∈ S✝assumption
Goals accomplished! 🐙)
Goals accomplished! 🐙
  α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

H: P ∈ finiteInterClosure (insert A S)

P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q·α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

univSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

univSet.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Qexact Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl cond: FiniteInter S
cond.univ_mem: ∀ {α : Type ?u.2085} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ S
univ_mem
Goals accomplished! 🐙
  α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P: Set α

H: P ∈ finiteInterClosure (insert A S)

P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q·α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ 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 ∈ S
hh | ⟨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 ∈ S
hQ⟨Q, hQ, rfl⟩: ∃ Q, Q ∈ S ∧ T1 = A ∩ Q
, rfl: T1 = A ∩ Q
rfl⟨Q, hQ, rfl⟩: ∃ Q, Q ∈ S ∧ T1 = A ∩ Q
⟩(h | ⟨Q, hQ, rfl⟩): ?m.1867 T1 a✝¹
)α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

h: T1 ∈ S

inter.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

Q: Set α

hQ: Q ∈ S

a✝: 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_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q<;>α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

h: T1 ∈ S

inter.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

Q: Set α

hQ: Q ∈ S

a✝: 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_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ 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 ∈ S
ii | ⟨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 ∈ S
hR⟨R, hR, rfl⟩: ∃ Q, Q ∈ S ∧ T2 = A ∩ Q
, rfl: T2 = A ∩ R
rfl⟨R, hR, rfl⟩: ∃ Q, Q ∈ S ∧ T2 = A ∩ Q
⟩(i | ⟨R, hR, rfl⟩): ?m.1867 T2 a✝¹
)α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h: T1 ∈ S

i: T2 ∈ S

inter.inl.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
    α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h: T1 ∈ S

i: T2 ∈ S

inter.inl.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h: T1 ∈ S

i: T2 ∈ S

inter.inl.inlT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S

inter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: 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 ∨ b
Or.inl (cond: FiniteInter S
cond.inter_mem: ∀ {α : Type ?u.2330} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
inter_mem h: T1 ∈ S
h i: T2 ∈ S
i)
Goals accomplished! 🐙
    α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S

inter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: 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 ∨ b
Or.inr ⟨T1: Set ?m.1865
T1 ∩ R: Set α
R, cond: FiniteInter S
cond.inter_mem: ∀ {α : Type ?u.2379} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
inter_mem h: T1 ∈ S
h hR: R ∈ S
hR, α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

inter.inl.inr.intro.introT1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Qby
Goals accomplished! 🐙 α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1: Set α

a✝¹: finiteInterClosure (insert A S) T1

h: T1 ∈ S

R: Set α

hR: R ∈ S

a✝: 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 ∩ a
Set.inter_comm _: Set ?m.2417
_ A: Set α
A]
Goals accomplished! 🐙⟩
Goals accomplished! 🐙
    α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S

inter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1 α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S

inter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: 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 ∨ b
Or.inr ⟨Q: Set α
Q ∩ T2: Set ?m.1865
T2, cond: FiniteInter S
cond.inter_mem: ∀ {α : Type ?u.2537} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
inter_mem hQ: Q ∈ S
hQ i: T2 ∈ S
i, α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S

inter.inr.intro.intro.inlA ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1by
Goals accomplished! 🐙 α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T2: Set α

a✝¹: finiteInterClosure (insert A S) T2

Q: Set α

hQ: Q ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ Q)

i: T2 ∈ S

A ∩ 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_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, T1, T2: Set α

a✝¹: finiteInterClosure (insert A S) T1

a✝: finiteInterClosure (insert A S) T2

h1: T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q

h2: T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q

interT1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q·α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: 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_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: 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 ∨ b
Or.inr
          ⟨Q: Set α
Q ∩ R: Set α
R, cond: FiniteInter S
cond.inter_mem: ∀ {α : Type ?u.2624} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
inter_mem hQ: Q ∈ S
hQ hR: R ∈ S
hR, α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: 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_1by
Goals accomplished! 🐙
            α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)ext x: ?α
xα: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α

hx ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
            α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)constructorα: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α

h.mpx ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α

h.mprx ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R) α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α

hx ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)<;>α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α

h.mpx ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α

h.mprx ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R) α: Type u_1

S: Set (Set α)

A: Set α

cond: FiniteInter S

P, Q: Set α

hQ: Q ∈ S

a✝¹: finiteInterClosure (insert A S) (A ∩ Q)

R: Set α

hR: R ∈ S

a✝: finiteInterClosure (insert A S) (A ∩ R)

x: α

hx ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)simp (config := { contextual := true: Bool
true })
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 ∩ Q
FiniteInter.finiteInterClosure_insert

end FiniteInter