case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c

case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c
cases' ha with ha ha
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b ≤ c

case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b ≈ c
⊢ a ⊔ b ≤ c
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c
cases' hb with hb hb
no goals
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b ≤ c
exact Or.inl (CauSeq.sup_lt ha hb)
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≤ c
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b ≈ c
⊢ a ⊔ b ≤ c
replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≈ b
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≤ c
refine' le_of_le_of_eq (Or.inr _) hb
no goals
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≈ b
exact CauSeq.sup_eq_right ha
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c
replace hb := le_of_le_of_eq hb (Setoid.symm ha)
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≈ a
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c
refine' le_of_le_of_eq (Or.inr _) ha
no goals
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≈ a
exact CauSeq.sup_eq_left hb