[GOAL]
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ↑F ⊆ S → ⋂₀ ↑F ∈ S
[PROOFSTEP]
classical
refine' Finset.induction_on F (fun _ => _) _
· simp [cond.univ_mem]
· intro a s _ h1 h2
  suffices a ∩ ⋂₀ ↑s ∈ S by simpa
  exact cond.inter_mem (h2 (Finset.mem_insert_self a s)) (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)
[GOAL]
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ↑F ⊆ S → ⋂₀ ↑F ∈ S
[PROOFSTEP]
refine' Finset.induction_on F (fun _ => _) _
[GOAL]
case refine'_1
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
x✝ : ↑∅ ⊆ S
⊢ ⋂₀ ↑∅ ∈ S
[PROOFSTEP]
simp [cond.univ_mem]
[GOAL]
case refine'_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ∀ ⦃a : Set α⦄ {s : Finset (Set α)}, ¬a ∈ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
[PROOFSTEP]
intro a s _ h1 h2
[GOAL]
case refine'_2
α : 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
⊢ ⋂₀ ↑(insert a s) ∈ S
[PROOFSTEP]
suffices a ∩ ⋂₀ ↑s ∈ S by simpa
[GOAL]
α : 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
this : a ∩ ⋂₀ ↑s ∈ S
⊢ ⋂₀ ↑(insert a s) ∈ S
[PROOFSTEP]
simpa
[GOAL]
case refine'_2
α : 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
⊢ a ∩ ⋂₀ ↑s ∈ S
[PROOFSTEP]
exact cond.inter_mem (h2 (Finset.mem_insert_self a s)) (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)
[GOAL]
α : 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
[PROOFSTEP]
induction' H with S h T1 T2 _ _ h1 h2
[GOAL]
case basic
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h : S ∈ insert A S✝
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
[PROOFSTEP]
cases h
[GOAL]
case basic.inl
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S = A
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
[PROOFSTEP]
exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
[GOAL]
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S = A
⊢ S = A ∩ Set.univ
[PROOFSTEP]
simpa
[GOAL]
case basic.inr
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S ∈ S✝
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
[PROOFSTEP]
exact Or.inl (by assumption)
[GOAL]
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S ∈ S✝
⊢ S ∈ S✝
[PROOFSTEP]
assumption
[GOAL]
case univ
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
⊢ Set.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
[PROOFSTEP]
exact Or.inl cond.univ_mem
[GOAL]
case inter
α : 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
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
[PROOFSTEP]
rcases h1 with (h | ⟨Q, hQ, rfl⟩)
[GOAL]
case inter.inl
α : 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
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
[PROOFSTEP]
rcases h2 with (i | ⟨R, hR, rfl⟩)
[GOAL]
case inter.inr.intro.intro
α : 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)
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
[PROOFSTEP]
rcases h2 with (i | ⟨R, hR, rfl⟩)
[GOAL]
case inter.inl.inl
α : 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
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
[PROOFSTEP]
exact Or.inl (cond.inter_mem h i)
[GOAL]
case inter.inl.inr.intro.intro
α : 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) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
[PROOFSTEP]
exact Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
[GOAL]
α : 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)
[PROOFSTEP]
simp only [← Set.inter_assoc, Set.inter_comm _ A]
[GOAL]
case inter.inr.intro.intro.inl
α : 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 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
[PROOFSTEP]
exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
[GOAL]
α : 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)
[PROOFSTEP]
simp only [Set.inter_assoc]
[GOAL]
case inter.inr.intro.intro.inr.intro.intro
α : 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) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
[PROOFSTEP]
exact
  Or.inr
    ⟨Q ∩ R, cond.inter_mem hQ hR, by
      ext x
      constructor <;> simp (config := { contextual := true })⟩
[GOAL]
α : 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)
[PROOFSTEP]
ext x
[GOAL]
case h
α : 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 : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : 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 : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case h.mpr
α : 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 : α
⊢ x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)
[PROOFSTEP]
simp (config := { contextual := true })
