ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
⊢ map Subtype.val atTop = atTop
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
⊢ map Subtype.val atTop = atTop
haveI : Nonempty s := ⟨⟨a, h le_rfl⟩⟩
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ (∀ (i : α), Ici i ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)) ∧ ∀ (i : ↑s), Subtype.val '' Ici i ∈ ⨅ (a : α), 𝓟 (Ici a)
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ map Subtype.val atTop = atTop
simp only [le_antisymm_iff, atTop, le_iInf_iff, le_principal_iff, mem_map, mem_setOf_eq,
  map_iInf_eq this, map_principal]
case left
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ ∀ (i : α), Ici i ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)

case right
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ ∀ (i : ↑s), Subtype.val '' Ici i ∈ ⨅ (a : α), 𝓟 (Ici a)
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ (∀ (i : α), Ici i ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)) ∧ ∀ (i : ↑s), Subtype.val '' Ici i ∈ ⨅ (a : α), 𝓟 (Ici a)
constructor
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) x) ((fun x => 𝓟 (Ici x)) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) y) ((fun x => 𝓟 (Ici x)) z)
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
⊢ Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
intro x y
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) x)
      ((fun x => 𝓟 (Ici x)) { val := ↑x ⊔ ↑y ⊔ a, property := (_ : ↑x ⊔ ↑y ⊔ a ∈ s) }) ∧
    (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) y)
      ((fun x => 𝓟 (Ici x)) { val := ↑x ⊔ ↑y ⊔ a, property := (_ : ↑x ⊔ ↑y ⊔ a ∈ s) })
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) x) ((fun x => 𝓟 (Ici x)) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) y) ((fun x => 𝓟 (Ici x)) z)
use ⟨x ⊔ y ⊔ a, h le_sup_right⟩
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ ↑x ≤ ↑x ⊔ ↑y ⊔ a ∧ ↑y ≤ ↑x ⊔ ↑y ⊔ a
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) x)
      ((fun x => 𝓟 (Ici x)) { val := ↑x ⊔ ↑y ⊔ a, property := (_ : ↑x ⊔ ↑y ⊔ a ∈ s) }) ∧
    (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) y)
      ((fun x => 𝓟 (Ici x)) { val := ↑x ⊔ ↑y ⊔ a, property := (_ : ↑x ⊔ ↑y ⊔ a ∈ s) })
simp only [ge_iff_le, principal_mono, Ici_subset_Ici, ← Subtype.coe_le_coe, Subtype.coe_mk]
no goals
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ ↑x ≤ ↑x ⊔ ↑y ⊔ a ∧ ↑y ≤ ↑x ⊔ ↑y ⊔ a
exact ⟨le_sup_left.trans le_sup_left, le_sup_right.trans le_sup_left⟩
case left
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
⊢ Ici x ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)
case left
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ ∀ (i : α), Ici i ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)
intro x
case left
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
⊢ Subtype.val '' Ici { val := x ⊔ a, property := (_ : x ⊔ a ∈ s) } ⊆ Ici x
case left
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
⊢ Ici x ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)
refine' mem_of_superset (mem_iInf_of_mem ⟨x ⊔ a, h le_sup_right⟩ (mem_principal_self _)) _
case left.intro.intro
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
y : ↑s
hy : y ∈ Ici { val := x ⊔ a, property := (_ : x ⊔ a ∈ s) }
⊢ ↑y ∈ Ici x
case left
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
⊢ Subtype.val '' Ici { val := x ⊔ a, property := (_ : x ⊔ a ∈ s) } ⊆ Ici x
rintro _ ⟨y, hy, rfl⟩
no goals
case left.intro.intro
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
y : ↑s
hy : y ∈ Ici { val := x ⊔ a, property := (_ : x ⊔ a ∈ s) }
⊢ ↑y ∈ Ici x
exact le_trans le_sup_left (Subtype.coe_le_coe.2 hy)
case right
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : ↑s
⊢ Subtype.val '' Ici x ∈ ⨅ (a : α), 𝓟 (Ici a)
case right
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ ∀ (i : ↑s), Subtype.val '' Ici i ∈ ⨅ (a : α), 𝓟 (Ici a)
intro x
case h
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : ↑s
b : α
hb : ↑x ⊔ a ≤ b
⊢ b ∈ Subtype.val '' Ici x
case right
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : ↑s
⊢ Subtype.val '' Ici x ∈ ⨅ (a : α), 𝓟 (Ici a)
filter_upwards [mem_atTop (↑x ⊔ a)]with b hb
no goals
case h
ι : Type ?u.314713
ι' : Type ?u.314716
α : Type u_1
β : Type ?u.314722
γ : Type ?u.314725
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : ↑s
b : α
hb : ↑x ⊔ a ≤ b
⊢ b ∈ Subtype.val '' Ici x
exact ⟨⟨b, h <| le_sup_right.trans hb⟩, Subtype.coe_le_coe.1 (le_sup_left.trans hb), rfl⟩