[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
⊢ ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨅ (a : ↑(range fun x => range (f x))), ⨆ (b : ↑↑a), ↑b
[PROOFSTEP]
simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : (a : ↑(range fun x => range (f x))) → ↑↑a
⊢ ⨅ (a : ↑(range fun x => range (f x))), ↑(g a) ≤ ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
[PROOFSTEP]
refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : (a : ↑(range fun x => range (f x))) → ↑↑a
⊢ ⨅ (a : ↑(range fun x => range (f x))), ↑(g a) ≤
    ⨅ (a : ι),
      f a
        ((fun a =>
            Classical.choose
              (_ :
                ↑(g
                      { val := (fun x => range (f x)) a,
                        property := (_ : ∃ y, (fun x => range (f x)) y = (fun x => range (f x)) a) }) ∈
                  ↑{ val := (fun x => range (f x)) a,
                      property := (_ : ∃ y, (fun x => range (f x)) y = (fun x => range (f x)) a) }))
          a)
[PROOFSTEP]
refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : (a : ↑(range fun x => range (f x))) → ↑↑a
a : ι
⊢ ↑(g { val := range (f a), property := (_ : ∃ y, (fun x => range (f x)) y = range (f a)) }) ≤
    f a
      ((fun a =>
          Classical.choose
            (_ :
              ↑(g
                    { val := (fun x => range (f x)) a,
                      property := (_ : ∃ y, (fun x => range (f x)) y = (fun x => range (f x)) a) }) ∈
                ↑{ val := (fun x => range (f x)) a,
                    property := (_ : ∃ y, (fun x => range (f x)) y = (fun x => range (f x)) a) }))
        a)
[PROOFSTEP]
rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
⊢ ⨆ (a : ι), ⨅ (b : κ a), f a b = ⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a)
[PROOFSTEP]
refine le_antisymm iSup_iInf_le ?_
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
⊢ ⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a) ≤ ⨆ (a : ι), ⨅ (b : κ a), f a b
[PROOFSTEP]
rw [iInf_iSup_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
⊢ ⨆ (g : ((a : ι) → κ a) → ι), ⨅ (a : (a : ι) → κ a), f (g a) (a (g a)) ≤ ⨆ (a : ι), ⨅ (b : κ a), f a b
[PROOFSTEP]
refine iSup_le fun g => ?_
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
⊢ ⨅ (a : (a : ι) → κ a), f (g a) (a (g a)) ≤ ⨆ (a : ι), ⨅ (b : κ a), f a b
[PROOFSTEP]
have ⟨a, ha⟩ : ∃ a, ∀ b, ∃ f, ∃ h : a = g f, h ▸ b = f (g f) :=
  of_not_not fun h => by
    push_neg at h
    choose h hh using h
    have := hh _ h rfl
    contradiction
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
h : ¬∃ a, ∀ (b : κ a), ∃ f h, h ▸ b = f (g f)
⊢ False
[PROOFSTEP]
push_neg at h
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
h : ∀ (a : ι), ∃ b, ∀ (f : (a : ι) → κ a) (h : a = g f), h ▸ b ≠ f (g f)
⊢ False
[PROOFSTEP]
choose h hh using h
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
h : (a : ι) → κ a
hh : ∀ (a : ι) (f : (a : ι) → κ a) (h_1 : a = g f), h_1 ▸ h a ≠ f (g f)
⊢ False
[PROOFSTEP]
have := hh _ h rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
h : (a : ι) → κ a
hh : ∀ (a : ι) (f : (a : ι) → κ a) (h_1 : a = g f), h_1 ▸ h a ≠ f (g f)
this : (_ : g h = g h) ▸ h (g h) ≠ h (g h)
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
a : ι
ha : ∀ (b : κ a), ∃ f h, h ▸ b = f (g f)
⊢ ⨅ (a : (a : ι) → κ a), f (g a) (a (g a)) ≤ ⨆ (a : ι), ⨅ (b : κ a), f a b
[PROOFSTEP]
refine le_trans ?_ (le_iSup _ a)
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
a : ι
ha : ∀ (b : κ a), ∃ f h, h ▸ b = f (g f)
⊢ ⨅ (a : (a : ι) → κ a), f (g a) (a (g a)) ≤ ⨅ (b : κ a), f a b
[PROOFSTEP]
refine le_iInf fun b => ?_
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
a : ι
ha : ∀ (b : κ a), ∃ f h, h ▸ b = f (g f)
b : κ a
⊢ ⨅ (a : (a : ι) → κ a), f (g a) (a (g a)) ≤ f a b
[PROOFSTEP]
obtain ⟨h, rfl, rfl⟩ := ha b
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
f : (a : ι) → κ a → α
g : ((a : ι) → κ a) → ι
h : (a : ι) → κ a
ha : ∀ (b : κ (g h)), ∃ f h_1, h_1 ▸ b = f (g f)
⊢ ⨅ (a : (a : ι) → κ a), f (g a) (a (g a)) ≤ f (g h) (h (g h))
[PROOFSTEP]
refine iInf_le _ _
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
⊢ a ⊓ sSup s =
    ⨅ (x : Bool),
      ⨆ (y : bif x then PUnit else ↑s),
        match x, y with
        | true, y => a
        | false, y => ↑y
[PROOFSTEP]
simp_rw [iInf_bool_eq, cond, iSup_const, iSup_subtype, sSup_eq_iSup]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
⊢ (⨆ (g : (a : Bool) → bif a then PUnit else ↑s),
      ⨅ (a_1 : Bool),
        match a_1, g a_1 with
        | true, y => a
        | false, y => ↑y) ≤
    ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
simp_rw [iInf_bool_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
⊢ ⨆ (g : (a : Bool) → bif a then PUnit else ↑s), a ⊓ ↑(g false) ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
refine iSup_le fun g => le_trans ?_ (le_iSup _ (g false).1)
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
g : (a : Bool) → bif a then PUnit else ↑s
⊢ a ⊓ ↑(g false) ≤ ⨆ (_ : ↑(g false) ∈ s), a ⊓ ↑(g false)
[PROOFSTEP]
refine le_trans ?_ (le_iSup _ (g false).2)
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
g : (a : Bool) → bif a then PUnit else ↑s
⊢ a ⊓ ↑(g false) ≤ a ⊓ ↑(g false)
[PROOFSTEP]
rfl
  -- See note [lower instance priority]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (b : ↑s), ⨆ (x : Bool), bif x then a else ↑b
[PROOFSTEP]
simp_rw [iInf_subtype, iSup_bool_eq, cond]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
by_cases ∀ i, f i = false
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
by_cases ∀ i, f i = false
[GOAL]
case pos
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ∀ (i : ↑s), f i = false
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
case neg
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ¬∀ (i : ↑s), f i = false
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
case pos => simp [h, iInf_subtype, ← sInf_eq_iInf]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ∀ (i : ↑s), f i = false
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
case pos => simp [h, iInf_subtype, ← sInf_eq_iInf]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ∀ (i : ↑s), f i = false
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
simp [h, iInf_subtype, ← sInf_eq_iInf]
[GOAL]
case neg
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ¬∀ (i : ↑s), f i = false
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
case neg =>
  have ⟨i, h⟩ : ∃ i, f i = true := by simpa using h
  refine le_trans (iInf_le _ i) ?_
  simp [h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ¬∀ (i : ↑s), f i = false
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
case neg =>
  have ⟨i, h⟩ : ∃ i, f i = true := by simpa using h
  refine le_trans (iInf_le _ i) ?_
  simp [h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ¬∀ (i : ↑s), f i = false
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
have ⟨i, h⟩ : ∃ i, f i = true := by simpa using h
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h : ¬∀ (i : ↑s), f i = false
⊢ ∃ i, f i = true
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h✝ : ¬∀ (i : ↑s), f i = false
i : ↑s
h : f i = true
⊢ (⨅ (a_1 : ↑s), bif f a_1 then a else ↑a_1) ≤ a ⊔ sInf s
[PROOFSTEP]
refine le_trans (iInf_le _ i) ?_
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompletelyDistribLattice α
a : α
s : Set α
f : ↑s → Bool
h✝ : ¬∀ (i : ↑s), f i = false
i : ↑s
h : f i = true
⊢ (bif f i then a else ↑i) ≤ a ⊔ sInf s
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
⊢ ⨅ (a : α), ⨆ (b : β a), g a b = ⨆ (g_1 : (a : α) → β a), ⨅ (a : α), g a (g_1 a)
[PROOFSTEP]
let lhs := ⨅ a, ⨆ b, g a b
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
⊢ ⨅ (a : α), ⨆ (b : β a), g a b = ⨆ (g_1 : (a : α) → β a), ⨅ (a : α), g a (g_1 a)
[PROOFSTEP]
let rhs := ⨆ h : ∀ a, β a, ⨅ a, g a (h a)
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
⊢ ⨅ (a : α), ⨆ (b : β a), g a b = ⨆ (g_1 : (a : α) → β a), ⨅ (a : α), g a (g_1 a)
[PROOFSTEP]
suffices lhs ≤ rhs from le_antisymm this le_iInf_iSup
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
⊢ lhs ≤ rhs
[PROOFSTEP]
by_cases ∃ x, rhs < x ∧ x < lhs
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
⊢ lhs ≤ rhs
[PROOFSTEP]
by_cases ∃ x, rhs < x ∧ x < lhs
[GOAL]
case pos
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
case neg
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
case pos =>
  rcases h with ⟨x, hr, hl⟩
  suffices rhs ≥ x from nomatch not_lt.2 this hr
  have : ∀ a, ∃ b, x < g a b := fun a =>
    lt_iSup_iff.1 <| lt_of_not_le fun h => lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
  choose f hf using this
  refine le_trans ?_ (le_iSup _ f)
  refine le_iInf fun a => le_of_lt (hf a)
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
case pos =>
  rcases h with ⟨x, hr, hl⟩
  suffices rhs ≥ x from nomatch not_lt.2 this hr
  have : ∀ a, ∃ b, x < g a b := fun a =>
    lt_iSup_iff.1 <| lt_of_not_le fun h => lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
  choose f hf using this
  refine le_trans ?_ (le_iSup _ f)
  refine le_iInf fun a => le_of_lt (hf a)
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
rcases h with ⟨x, hr, hl⟩
[GOAL]
case intro.intro
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
suffices rhs ≥ x from nomatch not_lt.2 this hr
[GOAL]
case intro.intro
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
⊢ rhs ≥ x
[PROOFSTEP]
have : ∀ a, ∃ b, x < g a b := fun a =>
  lt_iSup_iff.1 <| lt_of_not_le fun h => lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
[GOAL]
case intro.intro
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
this : ∀ (a : α), ∃ b, x < g a b
⊢ rhs ≥ x
[PROOFSTEP]
choose f hf using this
[GOAL]
case intro.intro
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ rhs ≥ x
[PROOFSTEP]
refine le_trans ?_ (le_iSup _ f)
[GOAL]
case intro.intro
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ x ≤ ⨅ (a : α), g a (f a)
[PROOFSTEP]
refine le_iInf fun a => le_of_lt (hf a)
[GOAL]
case neg
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
case neg =>
  refine le_of_not_lt fun hrl : rhs < lhs => not_le_of_lt hrl ?_
  replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by simpa only [not_exists, not_and_or, not_or, not_lt] using h
  have : ∀ a, ∃ b, rhs < g a b := fun a => lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
  choose f hf using this
  have : ∀ a, lhs ≤ g a (f a) := fun a => (h (g a (f a))).resolve_left (by simpa using hf a)
  refine le_trans ?_ (le_iSup _ f)
  refine le_iInf fun a => this _
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
case neg =>
  refine le_of_not_lt fun hrl : rhs < lhs => not_le_of_lt hrl ?_
  replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by simpa only [not_exists, not_and_or, not_or, not_lt] using h
  have : ∀ a, ∃ b, rhs < g a b := fun a => lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
  choose f hf using this
  have : ∀ a, lhs ≤ g a (f a) := fun a => (h (g a (f a))).resolve_left (by simpa using hf a)
  refine le_trans ?_ (le_iSup _ f)
  refine le_iInf fun a => this _
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
refine le_of_not_lt fun hrl : rhs < lhs => not_le_of_lt hrl ?_
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ lhs ≤ rhs
[PROOFSTEP]
replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by simpa only [not_exists, not_and_or, not_or, not_lt] using h
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
[PROOFSTEP]
simpa only [not_exists, not_and_or, not_or, not_lt] using h
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
⊢ lhs ≤ rhs
[PROOFSTEP]
have : ∀ a, ∃ b, rhs < g a b := fun a => lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
this : ∀ (a : α), ∃ b, rhs < g a b
⊢ lhs ≤ rhs
[PROOFSTEP]
choose f hf using this
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
⊢ lhs ≤ rhs
[PROOFSTEP]
have : ∀ a, lhs ≤ g a (f a) := fun a => (h (g a (f a))).resolve_left (by simpa using hf a)
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
a : α
⊢ ¬g a (f a) ≤ rhs
[PROOFSTEP]
simpa using hf a
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ rhs
[PROOFSTEP]
refine le_trans ?_ (le_iSup _ f)
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α✝ := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ ⨅ (a : α), g a (f a)
[PROOFSTEP]
refine le_iInf fun a => this _
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a b : α
⊢ sSup s ⊓ b = ⨆ (a : α) (_ : a ∈ s), a ⊓ b
[PROOFSTEP]
simpa only [inf_comm] using @inf_sSup_eq α _ s b
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b : α
f : ι → α
a : α
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
[PROOFSTEP]
rw [iSup, sSup_inf_eq, iSup_range]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b a : α
f : ι → α
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i
[PROOFSTEP]
simpa only [inf_comm] using iSup_inf_eq f a
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝² : Frame α✝
s✝ t : Set α✝
a✝ b : α✝
α : Type ?u.26817
β : Type ?u.26820
inst✝¹ : Frame α
inst✝ : Frame β
src✝ : CompleteLattice (α × β) := completeLattice α β
a : α × β
s : Set (α × β)
⊢ a ⊓ sSup s ≤ ⨆ (b : α × β) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
simp [Prod.le_def, sSup_eq_iSup, fst_iSup, snd_iSup, fst_iInf, snd_iInf, inf_iSup_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b : α
f : (i : ι) → κ i → α
a : α
⊢ (⨆ (i : ι) (j : κ i), f i j) ⊓ a = ⨆ (i : ι) (j : κ i), f i j ⊓ a
[PROOFSTEP]
simp only [iSup_inf_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b : α
f : (i : ι) → κ i → α
a : α
⊢ a ⊓ ⨆ (i : ι) (j : κ i), f i j = ⨆ (i : ι) (j : κ i), a ⊓ f i j
[PROOFSTEP]
simp only [inf_iSup_eq]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝ : Frame α
s t : Set α
a b : α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
⊢ (⨆ (i : ι), f i) ⊓ ⨆ (j : ι'), g j = ⨆ (i : ι × ι'), f i.fst ⊓ g i.snd
[PROOFSTEP]
simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝ : Frame α
s✝ t✝ : Set α
a b : α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ (⨆ (i : ι) (_ : i ∈ s), f i) ⊓ ⨆ (j : ι') (_ : j ∈ t), g j = ⨆ (p : ι × ι') (_ : p ∈ s ×ˢ t), f p.fst ⊓ g p.snd
[PROOFSTEP]
simp only [iSup_subtype', iSup_inf_iSup]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝ : Frame α
s✝ t✝ : Set α
a b : α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ ⨆ (i : { i // i ∈ s } × { i // i ∈ t }), f ↑i.fst ⊓ g ↑i.snd = ⨆ (x : { i // i ∈ s ×ˢ t }), f (↑x).fst ⊓ g (↑x).snd
[PROOFSTEP]
exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a b : α
⊢ sSup s ⊓ sSup t = ⨆ (p : α × α) (_ : p ∈ s ×ˢ t), p.fst ⊓ p.snd
[PROOFSTEP]
simp only [sSup_eq_iSup, biSup_inf_biSup]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a b : α
f : ι → α
⊢ Disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), Disjoint (f i) a
[PROOFSTEP]
simp only [disjoint_iff, iSup_inf_eq, iSup_eq_bot]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a b : α
f : ι → α
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)
[PROOFSTEP]
simpa only [disjoint_comm] using @iSup_disjoint_iff
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a b : α
f : (i : ι) → κ i → α
⊢ Disjoint (⨆ (i : ι) (j : κ i), f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a
[PROOFSTEP]
simp_rw [iSup_disjoint_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a b : α
f : (i : ι) → κ i → α
⊢ Disjoint a (⨆ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)
[PROOFSTEP]
simp_rw [disjoint_iSup_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s✝ t : Set α
a b : α
s : Set α
⊢ Disjoint (sSup s) a ↔ ∀ (b : α), b ∈ s → Disjoint b a
[PROOFSTEP]
simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s✝ t : Set α
a b : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ (b : α), b ∈ s → Disjoint a b
[PROOFSTEP]
simpa only [disjoint_comm] using @sSup_disjoint_iff
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ⨆ (i : ι), f i ⊓ g i = (⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i
[PROOFSTEP]
refine' (le_iSup_inf_iSup f g).antisymm _
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ (⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i ≤ ⨆ (i : ι), f i ⊓ g i
[PROOFSTEP]
rw [iSup_inf_iSup]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ⨆ (i : ι × ι), f i.fst ⊓ g i.snd ≤ ⨆ (i : ι), f i ⊓ g i
[PROOFSTEP]
refine' iSup_mono' fun i => _
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
⊢ ∃ i', f i.fst ⊓ g i.snd ≤ f i' ⊓ g i'
[PROOFSTEP]
rcases directed_of (· ≤ ·) i.1 i.2 with ⟨j, h₁, h₂⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
j : ι
h₁ : i.fst ≤ j
h₂ : i.snd ≤ j
⊢ ∃ i', f i.fst ⊓ g i.snd ≤ f i' ⊓ g i'
[PROOFSTEP]
exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝¹ : Frame α
s✝ t : Set α
a✝ b : α
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → Frame (π i)
src✝ : CompleteLattice ((i : ι) → π i) := completeLattice
a : (i : ι) → π i
s : Set ((i : ι) → π i)
i : ι
⊢ (a ⊓ sSup s) i ≤ iSup (fun b => ⨆ (_ : b ∈ s), a ⊓ b) i
[PROOFSTEP]
simp only [sSup_apply, iSup_apply, inf_apply, inf_iSup_eq, ← iSup_subtype'']
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝¹ : Frame α
s✝ t : Set α
a✝ b : α
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → Frame (π i)
src✝ : CompleteLattice ((i : ι) → π i) := completeLattice
a : (i : ι) → π i
s : Set ((i : ι) → π i)
i : ι
⊢ ⨆ (i_1 : ↑s), a i ⊓ ↑i_1 i ≤ ⨆ (i_1 : ↑s), a i ⊓ ↑i_1 i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
[PROOFSTEP]
rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝² : Coframe α✝
s✝ t : Set α✝
a✝ b : α✝
α : Type ?u.87146
β : Type ?u.87149
inst✝¹ : Coframe α
inst✝ : Coframe β
src✝ : CompleteLattice (α × β) := completeLattice α β
a : α × β
s : Set (α × β)
⊢ ⨅ (b : α × β) (_ : b ∈ s), a ⊔ b ≤ a ⊔ sInf s
[PROOFSTEP]
simp [Prod.le_def, sInf_eq_iInf, fst_iSup, snd_iSup, fst_iInf, snd_iInf, sup_iInf_eq]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝¹ : Coframe α
s✝ t : Set α
a✝ b : α
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → Coframe (π i)
src✝ : CompleteLattice ((i : ι) → π i) := completeLattice
a : (i : ι) → π i
s : Set ((i : ι) → π i)
i : ι
⊢ iInf (fun b => ⨅ (_ : b ∈ s), a ⊔ b) i ≤ (a ⊔ sInf s) i
[PROOFSTEP]
simp only [sInf_apply, iInf_apply, sup_apply, sup_iInf_eq, ← iInf_subtype'']
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort w'
inst✝¹ : Coframe α
s✝ t : Set α
a✝ b : α
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → Coframe (π i)
src✝ : CompleteLattice ((i : ι) → π i) := completeLattice
a : (i : ι) → π i
s : Set ((i : ι) → π i)
i : ι
⊢ ⨅ (i_1 : ↑s), a i ⊔ ↑i_1 i ≤ ⨅ (i_1 : ↑s), a i ⊔ ↑i_1 i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Coframe α
s t : Set α
a✝ b✝ : α
src✝ : Coframe α := inst✝
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
[PROOFSTEP]
rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]
[GOAL]
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
α : Type ?u.137509
β : Type ?u.137512
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
src✝ : CompleteLattice (α × β) := completeLattice α β
ι✝ : Type (max ?u.137509 ?u.137512)
κ✝ : ι✝ → Type (max ?u.137509 ?u.137512)
f : (a : ι✝) → κ✝ a → α × β
⊢ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b = ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)
[PROOFSTEP]
ext
[GOAL]
case h₁
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
α : Type ?u.137509
β : Type ?u.137512
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
src✝ : CompleteLattice (α × β) := completeLattice α β
ι✝ : Type (max ?u.137509 ?u.137512)
κ✝ : ι✝ → Type (max ?u.137509 ?u.137512)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b).fst = (⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)).fst
[PROOFSTEP]
simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]
[GOAL]
case h₂
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
α : Type ?u.137509
β : Type ?u.137512
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
src✝ : CompleteLattice (α × β) := completeLattice α β
ι✝ : Type (max ?u.137509 ?u.137512)
κ✝ : ι✝ → Type (max ?u.137509 ?u.137512)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b).snd = (⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)).snd
[PROOFSTEP]
simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]
[GOAL]
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
src✝ : CompleteLattice ((i : ι) → π i) := completeLattice
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
⊢ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b = ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
src✝ : CompleteLattice ((i : ι) → π i) := completeLattice
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
i : ι
⊢ iInf (fun a => ⨆ (b : κ✝ a), f a b) i = iSup (fun g => ⨅ (a : ι✝), f a (g a)) i
[PROOFSTEP]
simp only [iInf_apply, iSup_apply, iInf_iSup_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteBooleanAlgebra α
a b : α
s : Set α
f : ι → α
⊢ (iSup f)ᶜᶜ = (⨅ (i : ι), (f i)ᶜ)ᶜ
[PROOFSTEP]
simp [compl_iInf]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteBooleanAlgebra α
a b : α
s : Set α
f : ι → α
⊢ (sInf s)ᶜ = ⨆ (i : α) (_ : i ∈ s), iᶜ
[PROOFSTEP]
simp only [sInf_eq_iInf, compl_iInf]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteBooleanAlgebra α
a b : α
s : Set α
f : ι → α
⊢ (sSup s)ᶜ = ⨅ (i : α) (_ : i ∈ s), iᶜ
[PROOFSTEP]
simp only [sSup_eq_iSup, compl_iSup]
[GOAL]
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
src✝ : CompleteBooleanAlgebra ((i : ι) → π i) := completeBooleanAlgebra
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
⊢ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b = ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
src✝ : CompleteBooleanAlgebra ((i : ι) → π i) := completeBooleanAlgebra
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ iInf (fun a => ⨆ (b : κ✝ a), f a b) x✝ = iSup (fun g => ⨅ (a : ι✝), f a (g a)) x✝
[PROOFSTEP]
rw [iInf_iSup_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
src✝¹ : CompleteLattice Prop := completeLattice
src✝ : BooleanAlgebra Prop := booleanAlgebra
ι✝ : Type
κ✝ : ι✝ → Type
f : (a : ι✝) → κ✝ a → Prop
⊢ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f a b = ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f a (g a)
[PROOFSTEP]
simp [Classical.skolem]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Frame β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
change f (a ⊓ sSup s) ≤ f _
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Frame β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ f (a ⊓ sSup s) ≤ f (⨆ (b : α) (_ : b ∈ s), a ⊓ b)
[PROOFSTEP]
rw [← sSup_image, map_inf, map_sSup s, inf_iSup₂_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Frame β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ ⨆ (i : α) (_ : i ∈ s), f a ⊓ f i ≤ f (sSup ((fun b => a ⊓ b) '' s))
[PROOFSTEP]
simp_rw [← map_inf]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Frame β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ ⨆ (i : α) (_ : i ∈ s), f (a ⊓ i) ≤ f (sSup ((fun a_1 => a ⊓ a_1) '' s))
[PROOFSTEP]
exact ((map_sSup _).trans iSup_image).ge
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Coframe β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b ≤ a ⊔ sInf s
[PROOFSTEP]
change f _ ≤ f (a ⊔ sInf s)
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Coframe β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ f (⨅ (b : α) (_ : b ∈ s), a ⊔ b) ≤ f (a ⊔ sInf s)
[PROOFSTEP]
rw [← sInf_image, map_sup, map_sInf s, sup_iInf₂_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Coframe β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ f (sInf ((fun b => a ⊔ b) '' s)) ≤ ⨅ (i : α) (_ : i ∈ s), f a ⊔ f i
[PROOFSTEP]
simp_rw [← map_sup]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : Coframe β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
a : α
s : Set α
⊢ f (sInf ((fun a_1 => a ⊔ a_1) '' s)) ≤ ⨅ (i : α) (_ : i ∈ s), f (a ⊔ i)
[PROOFSTEP]
exact ((map_sInf _).trans iInf_image).le
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompletelyDistribLattice β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
src✝ : CompleteLattice α := Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ (a : ι✝), ⨆ (b : κ✝ a), g a b) = f (⨆ (g_1 : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), g a (g_1 a))
[PROOFSTEP]
simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range, iInf_iSup_eq]
  -- See note [reducible non-instances]
[GOAL]
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
⊢ CompleteAtomicBooleanAlgebra PUnit
[PROOFSTEP]
refine'
  { PUnit.booleanAlgebra with
    sSup := fun _ => unit
    sInf := fun _ => unit .. }
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
⊢ ∀ (s : Set PUnit) (a : PUnit), a ∈ s → a ≤ sSup s
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
s✝ : Set PUnit
a✝¹ : PUnit
a✝ : a✝¹ ∈ s✝
⊢ a✝¹ ≤ sSup s✝
[PROOFSTEP]
trivial
[GOAL]
case refine'_2
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
⊢ ∀ (s : Set PUnit) (a : PUnit), (∀ (b : PUnit), b ∈ s → b ≤ a) → sSup s ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
s✝ : Set PUnit
a✝¹ : PUnit
a✝ : ∀ (b : PUnit), b ∈ s✝ → b ≤ a✝¹
⊢ sSup s✝ ≤ a✝¹
[PROOFSTEP]
trivial
[GOAL]
case refine'_3
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
⊢ ∀ (s : Set PUnit) (a : PUnit), a ∈ s → sInf s ≤ a
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
s✝ : Set PUnit
a✝¹ : PUnit
a✝ : a✝¹ ∈ s✝
⊢ sInf s✝ ≤ a✝¹
[PROOFSTEP]
trivial
[GOAL]
case refine'_4
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
⊢ ∀ (s : Set PUnit) (a : PUnit), (∀ (b : PUnit), b ∈ s → a ≤ b) → a ≤ sInf s
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
s✝ : Set PUnit
a✝¹ : PUnit
a✝ : ∀ (b : PUnit), b ∈ s✝ → a✝¹ ≤ b
⊢ a✝¹ ≤ sInf s✝
[PROOFSTEP]
trivial
[GOAL]
case refine'_5
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
⊢ ∀ {ι : Type ?u.176306} {κ : ι → Type ?u.176306} (f : (a : ι) → κ a → PUnit),
    ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
ι✝ : Type ?u.176306
κ✝ : ι✝ → Type ?u.176306
f✝ : (a : ι✝) → κ✝ a → PUnit
⊢ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f✝ a b = ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f✝ a (g a)
[PROOFSTEP]
trivial
[GOAL]
case refine'_6
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
⊢ ∀ (a : PUnit) (s : Set PUnit), a ⊓ sSup s ≤ ⨆ (b : PUnit) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
a✝ : PUnit
s✝ : Set PUnit
⊢ a✝ ⊓ sSup s✝ ≤ ⨆ (b : PUnit) (_ : b ∈ s✝), a✝ ⊓ b
[PROOFSTEP]
trivial
[GOAL]
case refine'_7
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
⊢ ∀ (a : PUnit) (s : Set PUnit), ⨅ (b : PUnit) (_ : b ∈ s), a ⊔ b ≤ a ⊔ sInf s
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
s : Set PUnit
x y : PUnit
src✝ : BooleanAlgebra PUnit := booleanAlgebra
a✝ : PUnit
s✝ : Set PUnit
⊢ ⨅ (b : PUnit) (_ : b ∈ s✝), a✝ ⊔ b ≤ a✝ ⊔ sInf s✝
[PROOFSTEP]
trivial