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

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

case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ a ≤ b ⊓ c
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a < b
⊢ a ≤ b ⊓ c
cases' hc with hc hc
no goals
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a ≤ b ⊓ c
exact Or.inl (CauSeq.lt_inf hb hc)
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a ≈ c
⊢ a ≤ b ⊓ c
replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c
refine' le_of_eq_of_le hc (Or.inr _)
no goals
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≈ c
hb : c ≤ b
⊢ c ≈ b ⊓ c
exact Setoid.symm (CauSeq.inf_eq_right hb)
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ a ≤ b ⊓ c
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ a ≤ b ⊓ c
replace hc := le_of_eq_of_le (Setoid.symm hb) hc
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ a ≤ b ⊓ c
refine' le_of_eq_of_le hb (Or.inr _)
no goals
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c
exact Setoid.symm (CauSeq.inf_eq_left hc)