-- Mathlib/Data/Set/Finite/Lattice.lean
lemma Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} [Nonempty ι]
    {f : ι → Set α} (h : Directed (· ⊆ ·) f) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) :
    ∃ i, (s : Set α) ⊆ f i

Proof state:
case cons.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
i : ι
hi : b ∈ f i
j : ι
hj : ↑t ⊆ f j
k : ι
hik : f i ⊆ f k
hjk : f j ⊆ f k
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Tactic:
exact ⟨k, hik hi, hj.trans hjk⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Tactic:
rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩

Result:
case cons.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
i : ι
hi : b ∈ f i
j : ι
hj : ↑t ⊆ f j
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
s : Finset α
hs : ↑s ⊆ ⋃ i, f i
⊢ ∃ i, ↑s ⊆ f i

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons b t hbt iht =>
  simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
  rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
  rcases h i j with ⟨k, hik, hjk⟩
  exact ⟨k, hik hi, hj.trans hjk⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : ↑(Finset.cons b t hbt) ⊆ ⋃ i, f i
⊢ ∃ i, ↑(Finset.cons b t hbt) ⊆ f i

Tactic:
simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢

Result:
case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Proof state:
case cons.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
i : ι
hi : b ∈ f i
j : ι
hj : ↑t ⊆ f j
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Tactic:
rcases h i j with ⟨k, hik, hjk⟩

Result:
case cons.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
i : ι
hi : b ∈ f i
j : ι
hj : ↑t ⊆ f j
k : ι
hik : f i ⊆ f k
hjk : f j ⊆ f k
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i

Proof state:
case empty
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
hs : ↑∅ ⊆ ⋃ i, f i
⊢ ∃ i, ↑∅ ⊆ f i

Tactic:
simp

Result:
no goals