-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem sSupIndep_iUnion_of_directed {η : Type*} {s : η → Set α}
    (hs : Directed (· ⊆ ·) s) (h : ∀ i, sSupIndep (s i)) :
    sSupIndep (⋃ i, s i)

Proof state:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
⊢ sSupIndep (⋃ i, s i)

Tactic:
rw [sSupIndep_iff_finite]

Result:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
⊢ ∀ (t : Finset α), ↑t ⊆ ⋃ i, s i → sSupIndep ↑t

Proof state:
case neg.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ False

Tactic:
exact hη ⟨i⟩

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
I : Set η
fi : I.Finite
hI : ↑t ⊆ ⋃ i ∈ I, s i
⊢ sSupIndep ↑t

Tactic:
obtain ⟨i, hi⟩ := hs.finset_le fi.toFinset

Result:
case pos.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
I : Set η
fi : I.Finite
hI : ↑t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ sSupIndep ↑t

Proof state:
case neg.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ Disjoint a (sSup ((⋃ i, s i) \ {a}))

Tactic:
exfalso

Result:
case neg.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ False

Proof state:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
⊢ sSupIndep ↑t

Tactic:
obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht

Result:
case pos.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
I : Set η
fi : I.Finite
hI : ↑t ⊆ ⋃ i ∈ I, s i
⊢ sSupIndep ↑t

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
⊢ sSupIndep (⋃ i, s i)

Tactic:
by_cases hη : Nonempty η

Result:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
⊢ sSupIndep (⋃ i, s i)

case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
⊢ sSupIndep (⋃ i, s i)

Proof state:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
⊢ ∀ (t : Finset α), ↑t ⊆ ⋃ i, s i → sSupIndep ↑t

Tactic:
intro t ht

Result:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
⊢ sSupIndep ↑t

Proof state:
case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
⊢ sSupIndep (⋃ i, s i)

Tactic:
rintro a ⟨_, ⟨i, _⟩, _⟩

Result:
case neg.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ Disjoint a (sSup ((⋃ i, s i) \ {a}))

Proof state:
case pos.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
I : Set η
fi : I.Finite
hI : ↑t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ sSupIndep ↑t

Tactic:
exact (h i).mono
    (Set.Subset.trans hI <| Set.iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Result:
no goals