case empty
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ (∀ (x : α), x ∈ ∅ → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup ∅ id ≤ x

case insert
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
⊢ (∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
t : Finset α
⊢ (∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup t id ≤ x
induction' t using Finset.induction_on with a r _ ih h
no goals
case empty
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ (∀ (x : α), x ∈ ∅ → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup ∅ id ≤ x
simpa only [forall_prop_of_true, and_true_iff, forall_prop_of_false, bot_le, not_false_iff,
  sup_empty, forall_true_iff, not_mem_empty]
case insert
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
case insert
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
⊢ (∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
intro h
case insert
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
case insert
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
have incs : (r : Set α) ⊆ ↑(insert a r) := by
  rw [Finset.coe_subset]
  apply Finset.subset_insert
case insert.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
case insert
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
case insert.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
case insert.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)
case insert.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
case insert.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
case insert.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ sup (insert a r) id ≤ z
case insert.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ x, x ∈ s ∧ sup (insert a r) id ≤ x
use z, hzs
case insert.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ sup r id ≤ z
case insert.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ sup (insert a r) id ≤ z
rw [sup_insert, id.def, sup_le_iff]
no goals
case insert.intro.intro.intro.intro.intro.intro.intro
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : sup r id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ sup r id ≤ z
exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ r ⊆ insert a r
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ ↑r ⊆ ↑(insert a r)
rw [Finset.coe_subset]
no goals
F : Type ?u.76603
α✝ : Type ?u.76606
β : Type ?u.76609
γ : Type ?u.76612
ι : Type ?u.76615
κ : Type ?u.76618
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
s✝ s₁ s₂ : Finset β
f g : β → α✝
a✝¹ : α✝
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
a : α
r : Finset α
a✝ : ¬a ∈ r
ih : (∀ (x : α), x ∈ r → ∃ y, y ∈ s ∧ x ≤ y) → ∃ x, x ∈ s ∧ sup r id ≤ x
h : ∀ (x : α), x ∈ insert a r → ∃ y, y ∈ s ∧ x ≤ y
⊢ r ⊆ insert a r
apply Finset.subset_insert