α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ (↑s ⊆ ⋃ (i : ι), f i) → ∃ i, ↑s ⊆ f i
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
hs : ↑s ⊆ ⋃ (i : ι), f i
⊢ ∃ i, ↑s ⊆ f i
revert hs
case refine'_1
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ (↑∅ ⊆ ⋃ (i : ι), f i) → ∃ i, ↑∅ ⊆ f i

case refine'_2
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s → ((↑s ⊆ ⋃ (i : ι), f i) → ∃ i, ↑s ⊆ f i) → (↑(insert a s) ⊆ ⋃ (i : ι), f i) → ∃ i, ↑(insert a s) ⊆ f i
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ (↑s ⊆ ⋃ (i : ι), f i) → ∃ i, ↑s ⊆ f i
refine' s.induction_on _ _
case refine'_1
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
x✝ : ↑∅ ⊆ ⋃ (i : ι), f i
⊢ ↑∅ ⊆ f (Nonempty.some hn)
case refine'_1
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ (↑∅ ⊆ ⋃ (i : ι), f i) → ∃ i, ↑∅ ⊆ f i
refine' fun _ => ⟨hn.some, _⟩
no goals
case refine'_1
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
x✝ : ↑∅ ⊆ ⋃ (i : ι), f i
⊢ ↑∅ ⊆ f (Nonempty.some hn)
simp only [coe_empty, Set.empty_subset]
case refine'_2
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
⊢ ∃ i, ↑(insert b t) ⊆ f i
case refine'_2
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s → ((↑s ⊆ ⋃ (i : ι), f i) → ∃ i, ↑s ⊆ f i) → (↑(insert a s) ⊆ ⋃ (i : ι), f i) → ∃ i, ↑(insert a s) ⊆ f i
intro b t _hbt htc hbtc
case refine'_2.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
⊢ ∃ i, ↑(insert b t) ⊆ f i
case refine'_2
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
⊢ ∃ i, ↑(insert b t) ⊆ f i
obtain ⟨i : ι, hti : (t : Set α) ⊆ f i⟩ := htc (Set.Subset.trans (t.subset_insert b) hbtc)
case refine'_2.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
⊢ ∃ i, ↑(insert b t) ⊆ f i
case refine'_2.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
⊢ ∃ i, ↑(insert b t) ⊆ f i
obtain ⟨j, hbj⟩ : ∃ j, b ∈ f j := by simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)
case refine'_2.intro.intro.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ ∃ i, ↑(insert b t) ⊆ f i
case refine'_2.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
⊢ ∃ i, ↑(insert b t) ⊆ f i
rcases h j i with ⟨k, hk, hk'⟩
case refine'_2.intro.intro.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ ↑(insert b t) ⊆ f k
case refine'_2.intro.intro.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ ∃ i, ↑(insert b t) ⊆ f i
use k
case refine'_2.intro.intro.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ b ∈ f k ∧ ↑t ⊆ f k
case refine'_2.intro.intro.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ ↑(insert b t) ⊆ f k
rw [coe_insert, Set.insert_subset]
no goals
case refine'_2.intro.intro.intro.intro
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ b ∈ f k ∧ ↑t ⊆ f k
exact ⟨hk hbj, _root_.trans hti hk'⟩
no goals
α✝ : Type ?u.168635
β : Type ?u.168638
γ : Type ?u.168641
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_1
ι : Type u_2
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : (↑t ⊆ ⋃ (i : ι), f i) → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
⊢ ∃ j, b ∈ f j
simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)