case refine'_1
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
x✝ : ↑∅ ⊆ S
⊢ ⋂₀ ↑∅ ∈ S

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
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ↑F ⊆ S → ⋂₀ ↑F ∈ S
refine' Finset.induction_on F (fun _ => _) _
no goals
case refine'_1
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
x✝ : ↑∅ ⊆ S
⊢ ⋂₀ ↑∅ ∈ S
simp [cond.univ_mem]
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
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
intro a s _ h1 h2
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
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
suffices a ∩ ⋂₀ ↑s ∈ S by simpa
no goals
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
exact
  cond.inter_mem (h2 (Finset.mem_insert_self a s))
    (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)
no goals
α : 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
simpa