[GOAL]
α : Type u_1
s : Set α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h : sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) = ↑(sSup t)
[PROOFSTEP]
simp [dif_pos h]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h : sInf (Subtype.val '' t) ∈ s
⊢ sInf (Subtype.val '' t) = ↑(sInf t)
[PROOFSTEP]
simp [dif_pos h]
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = sSup univ
[PROOFSTEP]
have A : ∀ (u : Set s), ¬BddAbove u → BddAbove (Subtype.val '' u) → sSup ((↑) '' u : Set α) ∉ s :=
  by
  intro u hu Hu
  contrapose! hu
  refine ⟨⟨_, hu⟩, ?_⟩
  rintro ⟨x, xs⟩ hx
  simp only [Subtype.mk_le_mk]
  apply le_csSup Hu
  exact ⟨⟨x, xs⟩, hx, rfl⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
[PROOFSTEP]
intro u hu Hu
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
hu : ¬BddAbove u
Hu : BddAbove (Subtype.val '' u)
⊢ ¬sSup (Subtype.val '' u) ∈ s
[PROOFSTEP]
contrapose! hu
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
⊢ BddAbove u
[PROOFSTEP]
refine ⟨⟨_, hu⟩, ?_⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
⊢ { val := sSup (Subtype.val '' u), property := hu } ∈ upperBounds u
[PROOFSTEP]
rintro ⟨x, xs⟩ hx
[GOAL]
case mk
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
x : α
xs : x ∈ s
hx : { val := x, property := xs } ∈ u
⊢ { val := x, property := xs } ≤ { val := sSup (Subtype.val '' u), property := hu }
[PROOFSTEP]
simp only [Subtype.mk_le_mk]
[GOAL]
case mk
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
x : α
xs : x ∈ s
hx : { val := x, property := xs } ∈ u
⊢ x ≤ sSup (Subtype.val '' u)
[PROOFSTEP]
apply le_csSup Hu
[GOAL]
case mk
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
x : α
xs : x ∈ s
hx : { val := x, property := xs } ∈ u
⊢ x ∈ Subtype.val '' u
[PROOFSTEP]
exact ⟨⟨x, xs⟩, hx, rfl⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
⊢ sSup t = sSup univ
[PROOFSTEP]
by_cases Ht : BddAbove ((↑) '' t : Set α)
[GOAL]
case pos
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
⊢ sSup t = sSup univ
[PROOFSTEP]
have I1 : sSup ((↑) '' t : Set α) ∉ s := A t ht Ht
[GOAL]
case pos
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ sSup t = sSup univ
[PROOFSTEP]
have I2 : sSup ((↑) '' (univ : Set s) : Set α) ∉ s := by
  apply A
  · contrapose! ht; exact ht.mono (subset_univ _)
  · refine ⟨sSup ((↑) '' t : Set α), ?_⟩
    rintro - ⟨⟨x, hx⟩, -, rfl⟩
    simp [BddAbove, not_nonempty_iff_eq_empty] at ht 
    have : ⟨x, hx⟩ ∉ upperBounds t := by simp [ht]
    obtain ⟨⟨y, ys⟩, yt, hy⟩ : ∃ y, y ∈ t ∧ { val := x, property := hx } < y := by
      simpa only [Subtype.mk_le_mk, not_forall, not_le, exists_prop, exists_and_right, mem_upperBounds]
    refine le_trans (le_of_lt hy) ?_
    exact le_csSup Ht ⟨⟨y, ys⟩, yt, rfl⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ ¬sSup (Subtype.val '' univ) ∈ s
[PROOFSTEP]
apply A
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ ¬BddAbove univ
[PROOFSTEP]
contrapose! ht
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
ht : BddAbove univ
⊢ BddAbove t
[PROOFSTEP]
exact ht.mono (subset_univ _)
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ BddAbove (Subtype.val '' univ)
[PROOFSTEP]
refine ⟨sSup ((↑) '' t : Set α), ?_⟩
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) ∈ upperBounds (Subtype.val '' univ)
[PROOFSTEP]
rintro - ⟨⟨x, hx⟩, -, rfl⟩
[GOAL]
case a.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
simp [BddAbove, not_nonempty_iff_eq_empty] at ht 
[GOAL]
case a.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
have : ⟨x, hx⟩ ∉ upperBounds t := by simp [ht]
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
⊢ ¬{ val := x, property := hx } ∈ upperBounds t
[PROOFSTEP]
simp [ht]
[GOAL]
case a.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
obtain ⟨⟨y, ys⟩, yt, hy⟩ : ∃ y, y ∈ t ∧ { val := x, property := hx } < y := by
  simpa only [Subtype.mk_le_mk, not_forall, not_le, exists_prop, exists_and_right, mem_upperBounds]
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
⊢ ∃ y, y ∈ t ∧ { val := x, property := hx } < y
[PROOFSTEP]
simpa only [Subtype.mk_le_mk, not_forall, not_le, exists_prop, exists_and_right, mem_upperBounds]
[GOAL]
case a.intro.mk.intro.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
y : α
ys : y ∈ s
yt : { val := y, property := ys } ∈ t
hy : { val := x, property := hx } < { val := y, property := ys }
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
refine le_trans (le_of_lt hy) ?_
[GOAL]
case a.intro.mk.intro.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
y : α
ys : y ∈ s
yt : { val := y, property := ys } ∈ t
hy : { val := x, property := hx } < { val := y, property := ys }
⊢ ↑{ val := y, property := ys } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
exact le_csSup Ht ⟨⟨y, ys⟩, yt, rfl⟩
[GOAL]
case pos
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
I2 : ¬sSup (Subtype.val '' univ) ∈ s
⊢ sSup t = sSup univ
[PROOFSTEP]
simp only [sSup, I1, I2, dite_false]
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
⊢ sSup t = sSup univ
[PROOFSTEP]
have I : ¬BddAbove ((↑) '' (univ : Set s) : Set α) := by contrapose! Ht;
  exact Ht.mono (image_subset Subtype.val (subset_univ _))
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
⊢ ¬BddAbove (Subtype.val '' univ)
[PROOFSTEP]
contrapose! Ht
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' univ)
⊢ BddAbove (Subtype.val '' t)
[PROOFSTEP]
exact Ht.mono (image_subset Subtype.val (subset_univ _))
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
I : ¬BddAbove (Subtype.val '' univ)
⊢ sSup t = sSup univ
[PROOFSTEP]
have X : sSup ((↑) '' t : Set α) = sSup (univ : Set α) := ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ Ht
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
I : ¬BddAbove (Subtype.val '' univ)
X : sSup (Subtype.val '' t) = sSup univ
⊢ sSup t = sSup univ
[PROOFSTEP]
have Y : sSup ((↑) '' (univ : Set s) : Set α) = sSup (univ : Set α) :=
  ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ I
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
I : ¬BddAbove (Subtype.val '' univ)
X : sSup (Subtype.val '' t) = sSup univ
Y : sSup (Subtype.val '' univ) = sSup univ
⊢ sSup t = sSup univ
[PROOFSTEP]
simp only [sSup, X, Y]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), BddAbove s_1 → a ∈ s_1 → a ≤ sSup s_1
[PROOFSTEP]
rintro t c h_bdd hct
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddAbove t
hct : c ∈ t
⊢ c ≤ sSup t
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s (h_Sup ⟨c, hct⟩ h_bdd)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddAbove t
hct : c ∈ t
⊢ ↑c ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe _).le_csSup_image hct h_bdd
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), Set.Nonempty s_1 → a ∈ upperBounds s_1 → sSup s_1 ≤ a
[PROOFSTEP]
rintro t B ht hB
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ upperBounds t
⊢ sSup t ≤ B
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s (h_Sup ht ⟨B, hB⟩)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
[PROOFSTEP]
exact (Subtype.mono_coe s).csSup_image_le ht hB
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), BddBelow s_1 → a ∈ s_1 → sInf s_1 ≤ a
[PROOFSTEP]
rintro t c h_bdd hct
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddBelow t
hct : c ∈ t
⊢ sInf t ≤ c
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s (h_Inf ⟨c, hct⟩ h_bdd)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddBelow t
hct : c ∈ t
⊢ sInf (Subtype.val '' t) ≤ ↑c
[PROOFSTEP]
exact (Subtype.mono_coe s).csInf_image_le hct h_bdd
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), Set.Nonempty s_1 → a ∈ lowerBounds s_1 → a ≤ sInf s_1
[PROOFSTEP]
intro t B ht hB
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ lowerBounds t
⊢ B ≤ sInf t
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s (h_Inf ht ⟨B, hB⟩)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ lowerBounds t
⊢ ↑B ≤ sInf (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe s).le_csInf_image ht hB
[GOAL]
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
ht : Set.Nonempty t
h_bdd : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
[GOAL]
case intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd
[GOAL]
case intro.intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s
[PROOFSTEP]
refine' hs.out c.2 B.2 ⟨_, _⟩
[GOAL]
case intro.intro.refine'_1
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe s).le_csSup_image hct ⟨B, hB⟩
[GOAL]
case intro.intro.refine'_2
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
[PROOFSTEP]
exact (Subtype.mono_coe s).csSup_image_le ⟨c, hct⟩ hB
[GOAL]
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
ht : Set.Nonempty t
h_bdd : BddBelow t
⊢ sInf (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
[GOAL]
case intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
h_bdd : BddBelow t
c : ↑s
hct : c ∈ t
⊢ sInf (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd
[GOAL]
case intro.intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ∈ s
[PROOFSTEP]
refine' hs.out B.2 c.2 ⟨_, _⟩
[GOAL]
case intro.intro.refine'_1
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ ↑B ≤ sInf (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe s).le_csInf_image ⟨c, hct⟩ hB
[GOAL]
case intro.intro.refine'_2
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ≤ ↑c
[PROOFSTEP]
exact (Subtype.mono_coe s).csInf_image_le hct ⟨B, hB⟩
