[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : NoMaxOrder α
a : α
⊢ NoMaxOrder ↑(Ici a)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) = ↑⊥
[PROOFSTEP]
rw [bot_eq]
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) =
    ↑{ val := a, property := (_ : a ≤ a) }
[PROOFSTEP]
cases' h.lt_or_eq with h2 h2
[GOAL]
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
h2 : sSup ∅ < a
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) =
    ↑{ val := a, property := (_ : a ≤ a) }
[PROOFSTEP]
simp [h2.not_le]
[GOAL]
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
h : sSup ∅ ≤ a
src✝¹ : OrderBot { x // a ≤ x } := orderBot
src✝ : ConditionallyCompleteLinearOrder { x // a ≤ x } := Nonneg.conditionallyCompleteLinearOrder
h2 : sSup ∅ = a
⊢ ↑(if ht : sSup (Subtype.val '' ∅) ∈ Ici a then { val := sSup (Subtype.val '' ∅), property := ht } else default) =
    ↑{ val := a, property := (_ : a ≤ a) }
[PROOFSTEP]
simp [h2]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
src✝¹ : One { x // 0 ≤ x } := one
src✝ : OrderedAddCommMonoid { x // 0 ≤ x } := orderedAddCommMonoid
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
src✝¹ : One { x // 0 ≤ x } := one
src✝ : OrderedAddCommMonoid { x // 0 ≤ x } := orderedAddCommMonoid
x✝ : ℕ
⊢ NatCast.natCast (x✝ + 1) = NatCast.natCast x✝ + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
src✝¹ : One { x // 0 ≤ x } := one
src✝ : OrderedAddCommMonoid { x // 0 ≤ x } := orderedAddCommMonoid
x✝ : ℕ
⊢ { val := ↑x✝ + 1, property := (_ : (fun x => 0 ≤ x) (↑x✝ + 1)) } = { val := ↑x✝, property := (_ : 0 ≤ ↑x✝) } + 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
⊢ MonoidWithZero { x // 0 ≤ x }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : OrderedCommSemiring α
⊢ CommMonoidWithZero { x // 0 ≤ x }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝¹ : OrderedCommRing α
inst✝ : NoZeroDivisors α
src✝¹ : CanonicallyOrderedAddMonoid { x // 0 ≤ x } := canonicallyOrderedAddMonoid
src✝ : OrderedCommSemiring { x // 0 ≤ x } := orderedCommSemiring
⊢ ∀ {a b : { x // 0 ≤ x }}, a * b = 0 → a = 0 ∨ b = 0
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝¹ : OrderedCommRing α
inst✝ : NoZeroDivisors α
src✝¹ : CanonicallyOrderedAddMonoid { x // 0 ≤ x } := canonicallyOrderedAddMonoid
src✝ : OrderedCommSemiring { x // 0 ≤ x } := orderedCommSemiring
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
⊢ { val := a, property := ha } * { val := b, property := hb } = 0 →
    { val := a, property := ha } = 0 ∨ { val := b, property := hb } = 0
[PROOFSTEP]
simp only [mk_mul_mk, mk_eq_zero, mul_eq_zero, imp_self]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 ≤ a
⊢ toNonneg a = { val := a, property := h }
[PROOFSTEP]
simp [toNonneg, h]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
b : { x // 0 ≤ x }
⊢ toNonneg a ≤ b ↔ a ≤ ↑b
[PROOFSTEP]
cases' b with b hb
[GOAL]
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
hb : 0 ≤ b
⊢ toNonneg a ≤ { val := b, property := hb } ↔ a ≤ ↑{ val := b, property := hb }
[PROOFSTEP]
simp [toNonneg, hb]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : { x // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ ↑a < b
[PROOFSTEP]
cases' a with a ha
[GOAL]
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ { val := a, property := ha } < toNonneg b ↔ ↑{ val := a, property := ha } < b
[PROOFSTEP]
simp [toNonneg, ha.not_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ ∀ (a b c : { x // 0 ≤ x }), a - b ≤ c ↔ a ≤ c + b
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩
[GOAL]
case mk.mk.mk
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
c : α
hc : 0 ≤ c
⊢ { val := a, property := ha } - { val := b, property := hb } ≤ { val := c, property := hc } ↔
    { val := a, property := ha } ≤ { val := c, property := hc } + { val := b, property := hb }
[PROOFSTEP]
simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le, Subtype.coe_mk]
