[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = 0 ↔ ¬a ≤ b
[PROOFSTEP]
rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b = 0 ↔ ¬a < b
[PROOFSTEP]
rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ioc a b = 0 ↔ ¬a < b
[PROOFSTEP]
rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = 0 ↔ ¬a < b
[PROOFSTEP]
rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a a = 0
[PROOFSTEP]
rw [Ico, Finset.Ico_self, Finset.empty_val]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ioc a a = 0
[PROOFSTEP]
rw [Ioc, Finset.Ioc_self, Finset.empty_val]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ioo a a = 0
[PROOFSTEP]
rw [Ioo, Finset.Ioo_self, Finset.empty_val]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hca : c ≤ a
⊢ filter (fun x => x < c) (Ico a b) = ∅
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hca : c ≤ a
⊢ ∅.val = ∅
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hbc : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a b
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a c
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ (Finset.Ico a c).val = Ico a c
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hca : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico a b
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) b)
⊢ filter (fun x => b ≤ x) (Ico a b) = ∅
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) b)
⊢ ∅.val = ∅
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico c b
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
⊢ (Finset.Ico c b).val = Ico c b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b a : α
⊢ Icc a a = {a}
[PROOFSTEP]
rw [Icc, Finset.Icc_self, Finset.singleton_val]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b
[PROOFSTEP]
classical
rw [Ico, ← Finset.insert_val_of_not_mem right_not_mem_Ico, Finset.Ico_insert_right h]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b
[PROOFSTEP]
rw [Ico, ← Finset.insert_val_of_not_mem right_not_mem_Ico, Finset.Ico_insert_right h]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ (Finset.Icc a b).val = Icc a b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b
[PROOFSTEP]
classical
rw [Ioo, ← Finset.insert_val_of_not_mem left_not_mem_Ioo, Finset.Ioo_insert_left h]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b
[PROOFSTEP]
rw [Ioo, ← Finset.insert_val_of_not_mem left_not_mem_Ioo, Finset.Ioo_insert_left h]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ (Finset.Ico a b).val = Ico a b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h : b ≤ c
x : α
hab : x ∈ Ico a b
hbc : x ∈ Ico c d
⊢ False
[PROOFSTEP]
rw [mem_Ico] at hab hbc 
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h : b ≤ c
x : α
hab : a ≤ x ∧ x < b
hbc : c ≤ x ∧ x < d
⊢ False
[PROOFSTEP]
exact hab.2.not_le (h.trans hbc.1)
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}
[PROOFSTEP]
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ {a}.val = {a}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c
[PROOFSTEP]
rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
  Finset.Ico_union_Ico_eq_Ico hab hbc]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
[PROOFSTEP]
rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ Ico a b - Ico a c = Ico (max a c) b
[PROOFSTEP]
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c✝ d a b c : α
⊢ Ico a b - Ico c b = Ico a (min b c)
[PROOFSTEP]
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
classical rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
classical rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
  ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map ((fun x x_1 => x + x_1) c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val, ((Finset.nodup _).map <| add_right_injective c).dedup]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Icc _ _ _
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Ico _ _ _
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Ioc _ _ _
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)
[PROOFSTEP]
simp_rw [add_comm _ c]
[GOAL]
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
exact map_add_left_Ioo _ _ _
