[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
⊢ ∀ (s : Set (Tropical R)), ¬BddAbove s → sSup s = sSup Set.univ
[PROOFSTEP]
intro s hs
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
⊢ sSup s = sSup Set.univ
[PROOFSTEP]
have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ sSup s = sSup Set.univ
[PROOFSTEP]
simp [sSup, this]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ sSup (untrop '' s) = sSup Set.univ
[PROOFSTEP]
apply csSup_of_not_bddAbove
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ ¬BddAbove (untrop '' s)
[PROOFSTEP]
contrapose! hs
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddAbove (untrop '' s)
⊢ BddAbove s
[PROOFSTEP]
change BddAbove (tropOrderIso.symm '' s) at hs 
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddAbove (↑(OrderIso.symm tropOrderIso) '' s)
⊢ BddAbove s
[PROOFSTEP]
exact tropOrderIso.symm.bddAbove_image.1 hs
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
⊢ ∀ (s : Set (Tropical R)), ¬BddBelow s → sInf s = sInf Set.univ
[PROOFSTEP]
intro s hs
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
⊢ sInf s = sInf Set.univ
[PROOFSTEP]
have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ sInf s = sInf Set.univ
[PROOFSTEP]
simp [sInf, this]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ sInf (untrop '' s) = sInf Set.univ
[PROOFSTEP]
apply csInf_of_not_bddBelow
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ ¬BddBelow (untrop '' s)
[PROOFSTEP]
contrapose! hs
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddBelow (untrop '' s)
⊢ BddBelow s
[PROOFSTEP]
change BddBelow (tropOrderIso.symm '' s) at hs 
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddBelow (↑(OrderIso.symm tropOrderIso) '' s)
⊢ BddBelow s
[PROOFSTEP]
exact tropOrderIso.symm.bddBelow_image.1 hs
