[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
b : β
⊢ b ∈ upperBounds (l '' s) ↔ b ∈ u ⁻¹' upperBounds s
[PROOFSTEP]
simp [upperBounds, gc _ _]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
x✝ : BddAbove (l '' s)
x : β
hx : x ∈ upperBounds (l '' s)
⊢ u x ∈ upperBounds s
[PROOFSTEP]
rwa [gc.upperBounds_l_image] at hx 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
⊢ u b ∈ upperBounds s
[PROOFSTEP]
rwa [gc.upperBounds_l_image] at hb 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y
[PROOFSTEP]
rintro rfl x
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y
[PROOFSTEP]
exact (gc x y).symm
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z
[PROOFSTEP]
exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
⊢ l x = z ↔ ∀ (y : β), z ≤ y ↔ x ≤ u y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
⊢ l x = z → ∀ (y : β), z ≤ y ↔ x ≤ u y
[PROOFSTEP]
rintro rfl y
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
y : β
⊢ l x ≤ y ↔ x ≤ u y
[PROOFSTEP]
exact gc x y
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
⊢ (∀ (y : β), z ≤ y ↔ x ≤ u y) → l x = z
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
x : α
z : β
H : ∀ (y : β), z ≤ y ↔ x ≤ u y
⊢ l x = z
[PROOFSTEP]
exact ((gc _ _).mpr <| (H z).mp le_rfl).antisymm ((H <| l x).mpr (gc.le_u_l x))
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ IsLUB (l '' {a₁, a₂}) (l a₁ ⊔ l a₂)
[PROOFSTEP]
simp only [image_pair, isLUB_pair]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))
[PROOFSTEP]
rw [range_comp, ← sSup_range]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))
[PROOFSTEP]
exact gc.isLUB_l_image (isLUB_sSup _)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), l (f i j)
[PROOFSTEP]
simp_rw [gc.l_iSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
⊢ l (sSup s) = ⨆ (a : α) (_ : a ∈ s), l a
[PROOFSTEP]
simp only [sSup_eq_iSup, gc.l_iSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
l1 : α → β
u1 : β → α
l2 : β → γ
u2 : γ → β
gc1 : GaloisConnection l1 u1
gc2 : GaloisConnection l2 u2
⊢ GaloisConnection (l2 ∘ l1) (u1 ∘ u2)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
l1 : α → β
u1 : β → α
l2 : β → γ
u2 : γ → β
gc1 : GaloisConnection l1 u1
gc2 : GaloisConnection l2 u2
a : α
b : γ
⊢ (l2 ∘ l1) a ≤ b ↔ a ≤ (u1 ∘ u2) b
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
l1 : α → β
u1 : β → α
l2 : β → γ
u2 : γ → β
gc1 : GaloisConnection l1 u1
gc2 : GaloisConnection l2 u2
a : α
b : γ
⊢ l2 (l1 a) ≤ b ↔ a ≤ u1 (u2 b)
[PROOFSTEP]
rw [gc2, gc1]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (compl ∘ u ∘ compl) a ≤ b ↔ a ≤ (compl ∘ l ∘ compl) b
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
[PROOFSTEP]
rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
⊢ sSup (image2 l s t) = l (sSup s) (sSup t)
[PROOFSTEP]
simp_rw [sSup_image2, ← (h₂ _).l_sSup, ← (h₁ _).l_sSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (l₁ b) (swap u b)
h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)
⊢ sInf (image2 u s t) = u (sInf s) (sInf t)
[PROOFSTEP]
simp_rw [sInf_image2, ← (h₂ _).u_sInf, ← (h₁ _).u_sInf]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (↑e ⁻¹' s) ↔ BddAbove s
[PROOFSTEP]
rw [← e.bddAbove_image, e.image_preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddBelow (↑e ⁻¹' s) ↔ BddBelow s
[PROOFSTEP]
rw [← e.bddBelow_image, e.image_preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
gi : GaloisInsertion l u
a b : β
⊢ l (u a) ⊔ l (u b) = a ⊔ b
[PROOFSTEP]
simp only [gi.l_u_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨆ (i : ι) (hi : p i), u (f i hi)) = ⨆ (i : ι) (hi : p i), f i hi
[PROOFSTEP]
simp only [iSup_subtype', gi.l_iSup_u]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sSup (u '' s)) = sSup s
[PROOFSTEP]
rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
gi : GaloisInsertion l u
a b : β
⊢ l (u (a ⊓ b)) = a ⊓ b
[PROOFSTEP]
simp only [gi.l_u_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨅ (i : ι) (hi : p i), u (f i hi)) = ⨅ (i : ι) (hi : p i), f i hi
[PROOFSTEP]
simp only [iInf_subtype', gi.l_iInf_u]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s
[PROOFSTEP]
rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
f : ι → α
hf : ∀ (i : ι), u (l (f i)) = f i
⊢ l (⨅ (i : ι), f i) = l (⨅ (i : ι), u (l (f i)))
[PROOFSTEP]
simp [hf]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (i : ι) (hi : p i), f i hi) = ⨅ (i : ι) (hi : p i), l (f i hi)
[PROOFSTEP]
rw [iInf_subtype', iInf_subtype']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (x : { i // p i }), f ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), l (f ↑x (_ : p ↑x))
[PROOFSTEP]
exact gi.l_iInf_of_ul_eq_self _ fun _ => hf _ _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), a ⊓ b ≤ a
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ a
[PROOFSTEP]
exact fun a b => gi.gc.l_le inf_le_left
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), a ⊓ b ≤ b
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ b
[PROOFSTEP]
exact fun a b => gi.gc.l_le inf_le_right
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
src✝ : PartialOrder β := inst✝¹
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)
[PROOFSTEP]
exact fun a b c hac hbc =>
  (gi.le_l_u a).trans <| gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ ⊤
[PROOFSTEP]
simp only [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝² : PartialOrder β
inst✝¹ : Preorder α
inst✝ : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ l ⊤
[PROOFSTEP]
exact fun b => (gi.le_l_u b).trans (gi.gc.monotone_l le_top)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), a ∈ s → sInf s ≤ a
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), a ∈ s → choice gi (sInf (u '' s)) (_ : u (l (sInf (u '' s))) ≤ sInf (u '' s)) ≤ a
[PROOFSTEP]
rw [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), a ∈ s → l (sInf (u '' s)) ≤ a
[PROOFSTEP]
exact (gi.isGLB_of_u_image (isGLB_sInf _)).1
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), (∀ (b : β), b ∈ s → a ≤ b) → a ≤ sInf s
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), (∀ (b : β), b ∈ s → a ≤ b) → a ≤ choice gi (sInf (u '' s)) (_ : u (l (sInf (u '' s))) ≤ sInf (u '' s))
[PROOFSTEP]
rw [gi.choice_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
src✝¹ : BoundedOrder β := liftBoundedOrder gi
src✝ : Lattice β := liftLattice gi
s : Set β
⊢ ∀ (a : β), (∀ (b : β), b ∈ s → a ≤ b) → a ≤ l (sInf (u '' s))
[PROOFSTEP]
exact (gi.isGLB_of_u_image (isGLB_sInf _)).2
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeInf β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ a ⊓ b ≤ a
[PROOFSTEP]
exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_left a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeInf β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ a ⊓ b ≤ b
[PROOFSTEP]
exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_right a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeInf β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b c : α
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
exact (@OrderDual.semilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).le_inf a b c
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeSup β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ a ≤ a ⊔ b
[PROOFSTEP]
exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_left a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeSup β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b : α
⊢ b ≤ a ⊔ b
[PROOFSTEP]
exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_right a b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder α
inst✝ : SemilatticeSup β
gi : GaloisCoinsertion l u
src✝ : PartialOrder α := inst✝¹
a b c : α
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c
[PROOFSTEP]
exact (@OrderDual.semilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).sup_le a b c
