[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Finset.Nonempty (Icc a b) ↔ a ≤ b
[PROOFSTEP]
rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Finset.Nonempty (Ico a b) ↔ a < b
[PROOFSTEP]
rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Finset.Nonempty (Ioc a b) ↔ a < b
[PROOFSTEP]
rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Finset.Nonempty (Ioo a b) ↔ a < b
[PROOFSTEP]
rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Icc a b = ∅ ↔ ¬a ≤ b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ico a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioc a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp only [mem_Icc, true_and_iff, le_rfl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ico a b ↔ a < b
[PROOFSTEP]
simp only [mem_Ico, true_and_iff, le_refl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp only [mem_Icc, and_true_iff, le_rfl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ioc a b ↔ a < b
[PROOFSTEP]
simp only [mem_Ioc, and_true_iff, le_rfl]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Icc_subset_Icc ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Ico_subset_Ico ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioc_subset_Ioc ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ⊆ Ioo a₂ b₂
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioo_subset_Ioo ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b
[PROOFSTEP]
rw [← coe_subset, coe_Ico, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b
[PROOFSTEP]
exact Set.Ico_subset_Ioo_left h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂
[PROOFSTEP]
rw [← coe_subset, coe_Ioc, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ Set.Ioo a b₂
[PROOFSTEP]
exact Set.Ioc_subset_Ioo_right h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂
[PROOFSTEP]
exact Set.Icc_subset_Ico_right h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioo a b ⊆ Ico a b
[PROOFSTEP]
rw [← coe_subset, coe_Ioo, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ioo a b ⊆ Set.Ico a b
[PROOFSTEP]
exact Set.Ioo_subset_Ico_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioo a b ⊆ Ioc a b
[PROOFSTEP]
rw [← coe_subset, coe_Ioo, coe_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ioo a b ⊆ Set.Ioc a b
[PROOFSTEP]
exact Set.Ioo_subset_Ioc_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ico a b ⊆ Icc a b
[PROOFSTEP]
rw [← coe_subset, coe_Ico, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ico a b ⊆ Set.Icc a b
[PROOFSTEP]
exact Set.Ico_subset_Icc_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioc a b ⊆ Icc a b
[PROOFSTEP]
rw [← coe_subset, coe_Ioc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.Ioc a b ⊆ Set.Icc a b
[PROOFSTEP]
exact Set.Ioc_subset_Icc_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
[PROOFSTEP]
rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂
[PROOFSTEP]
rw [← coe_ssubset, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
[PROOFSTEP]
exact Set.Icc_ssubset_Icc_left hI ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂
[PROOFSTEP]
rw [← coe_ssubset, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
[PROOFSTEP]
exact Set.Icc_ssubset_Icc_right hI ha hb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
⊢ Set.Finite s
[PROOFSTEP]
let ⟨a, ha⟩ := h₀
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
a : α
ha : a ∈ lowerBounds s
⊢ Set.Finite s
[PROOFSTEP]
let ⟨b, hb⟩ := h₁
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
a : α
ha : a ∈ lowerBounds s
b : α
hb : b ∈ upperBounds s
⊢ Set.Finite s
[PROOFSTEP]
classical exact ⟨Set.fintypeOfMemBounds ha hb⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
s : Set α
h₀ : BddBelow s
h₁ : BddAbove s
a : α
ha : a ∈ lowerBounds s
b : α
hb : b ∈ upperBounds s
⊢ Set.Finite s
[PROOFSTEP]
exact ⟨Set.fintypeOfMemBounds ha hb⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a c
[PROOFSTEP]
ext x
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x✝ : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ x ∈ filter (fun x => x < c) (Ico a b) ↔ x ∈ Ico a c
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_Ico, and_right_comm]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x✝ : α
inst✝ : DecidablePred fun x => x < c
hcb : c ≤ b
x : α
⊢ (a ≤ x ∧ x < c) ∧ x < b ↔ a ≤ x ∧ x < c
[PROOFSTEP]
exact and_iff_left_of_imp fun h => h.2.trans_le hcb
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
⊢ filter ((fun x x_1 => x ≤ x_1) c) (Ico a b) = Ico c b
[PROOFSTEP]
ext x
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x✝ a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
x : α
⊢ x ∈ filter ((fun x x_1 => x ≤ x_1) c) (Ico a b) ↔ x ∈ Ico c b
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_Ico, and_comm, and_left_comm]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x✝ a b c : α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) c)
hac : a ≤ c
x : α
⊢ a ≤ x ∧ (fun x x_1 => x ≤ x_1) c x ∧ x < b ↔ c ≤ x ∧ x < b
[PROOFSTEP]
exact and_iff_right_of_imp fun h => hac.trans h.1
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j < b
⊢ filter (fun j => a < j ∧ j < b) univ = Ioo a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j < b) univ ↔ a✝ ∈ Ioo a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j ≤ b
⊢ filter (fun j => a < j ∧ j ≤ b) univ = Ioc a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j ≤ b) univ ↔ a✝ ∈ Ioc a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j < b
⊢ filter (fun j => a ≤ j ∧ j < b) univ = Ico a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j < b) univ ↔ a✝ ∈ Ico a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j ≤ b
⊢ filter (fun j => a ≤ j ∧ j ≤ b) univ = Icc a b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j ≤ b) univ ↔ a✝ ∈ Icc a b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Icc a b ⊆ Ici a
[PROOFSTEP]
simpa [← coe_subset] using Set.Icc_subset_Ici_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Ico a b ⊆ Ici a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ico_subset_Ici_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioc a b ⊆ Ioi a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioc_subset_Ioi_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioo a b ⊆ Ioi a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioo_subset_Ioi_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Icc a b ⊆ Iic b
[PROOFSTEP]
simpa [← coe_subset] using Set.Icc_subset_Iic_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Ioc a b ⊆ Iic b
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioc_subset_Iic_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Ico a b ⊆ Iio b
[PROOFSTEP]
simpa [← coe_subset] using Set.Ico_subset_Iio_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderBot α
⊢ Ioo a b ⊆ Iio b
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioo_subset_Iio_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ioi a ⊆ Ici a
[PROOFSTEP]
simpa [← coe_subset] using Set.Ioi_subset_Ici_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x < x_1) a)
⊢ filter ((fun x x_1 => x < x_1) a) univ = Ioi a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x < x_1) a)
a✝ : α
⊢ a✝ ∈ filter ((fun x x_1 => x < x_1) a) univ ↔ a✝ ∈ Ioi a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) a)
⊢ filter ((fun x x_1 => x ≤ x_1) a) univ = Ici a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred ((fun x x_1 => x ≤ x_1) a)
a✝ : α
⊢ a✝ ∈ filter ((fun x x_1 => x ≤ x_1) a) univ ↔ a✝ ∈ Ici a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ Iio a ⊆ Iic a
[PROOFSTEP]
simpa [← coe_subset] using Set.Iio_subset_Iic_self
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x < a
⊢ filter (fun x => x < a) univ = Iio a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x < a
a✝ : α
⊢ a✝ ∈ filter (fun x => x < a) univ ↔ a✝ ∈ Iio a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x ≤ a
⊢ filter (fun x => x ≤ a) univ = Iic a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x ≤ a
a✝ : α
⊢ a✝ ∈ filter (fun x => x ≤ a) univ ↔ a✝ ∈ Iic a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b c a : α
⊢ Icc a a = {a}
[PROOFSTEP]
rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c
[PROOFSTEP]
rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Icc a b) a = Ioc a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Icc a b) b = Ico a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Ico a b) a = Ioo a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ erase (Ioc a b) b = Ioo a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c : α
inst✝ : DecidableEq α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b
[PROOFSTEP]
simp [← coe_inj]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Ioo a b) = Ico a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioc a b = {a}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ Ico a b \ Ioo a b = {a}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}
[PROOFSTEP]
simp [← coe_inj, h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) (_ : ¬b ∈ Ico a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ico_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) (_ : ¬b ∈ Ico a b)
[PROOFSTEP]
rw [cons_eq_insert, Ico_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) (_ : ¬a ∈ Ioc a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioc_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) (_ : ¬a ∈ Ioc a b)
[PROOFSTEP]
rw [cons_eq_insert, Ioc_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) (_ : ¬b ∈ Ioo a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioo_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) (_ : ¬b ∈ Ioo a b)
[PROOFSTEP]
rw [cons_eq_insert, Ioo_insert_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) (_ : ¬a ∈ Ioo a b)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioo_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) (_ : ¬a ∈ Ioo a b)
[PROOFSTEP]
rw [cons_eq_insert, Ioo_insert_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}
[PROOFSTEP]
ext x
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x ∈ filter (fun x => x ≤ a) (Ico a b) ↔ x ∈ {a}
[PROOFSTEP]
rw [mem_filter, mem_Ico, mem_singleton, and_right_comm, ← le_antisymm_iff, eq_comm]
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a✝ b✝ c a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x = a ∧ x < b ↔ x = a
[PROOFSTEP]
exact and_iff_left_of_imp fun h => h.le.trans_lt hab
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
classical
by_cases h : a ≤ b
· rw [Icc_eq_cons_Ico h, card_cons]
  exact (Nat.add_sub_cancel _ _).symm
· rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
by_cases h : a ≤ b
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
rw [Icc_eq_cons_Ico h, card_cons]
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Ico a b) + 1 - 1
[PROOFSTEP]
exact (Nat.add_sub_cancel _ _).symm
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : ¬a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1
[PROOFSTEP]
rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
classical
by_cases h : a < b
· rw [Ico_eq_cons_Ioo h, card_cons]
  exact (Nat.add_sub_cancel _ _).symm
· rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
by_cases h : a < b
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a < b
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
rw [Ico_eq_cons_Ioo h, card_cons]
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a < b
⊢ card (Ioo a b) = card (Ioo a b) + 1 - 1
[PROOFSTEP]
exact (Nat.add_sub_cancel _ _).symm
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : ¬a < b
⊢ card (Ioo a b) = card (Ico a b) - 1
[PROOFSTEP]
rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, zero_tsub]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ioo a b) = card (Icc a b) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Icc a b) - 1 - 1 = card (Icc a b) - 2
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ erase (Ici a) a = Ioi a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ erase (Ici a) a ↔ a✝ ∈ Ioi a
[PROOFSTEP]
simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a
[PROOFSTEP]
simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) (_ : ¬a ∈ Ioi a)
[PROOFSTEP]
classical rw [cons_eq_insert, Ioi_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) (_ : ¬a ∈ Ioi a)
[PROOFSTEP]
rw [cons_eq_insert, Ioi_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ card (Ioi a) = card (Ici a) - 1
[PROOFSTEP]
rw [Ici_eq_cons_Ioi, card_cons, add_tsub_cancel_right]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ erase (Iic b) b = Iio b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ erase (Iic b) b ↔ a✝ ∈ Iio b
[PROOFSTEP]
simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b
[PROOFSTEP]
simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) (_ : ¬b ∈ Iio b)
[PROOFSTEP]
classical rw [cons_eq_insert, Iio_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) (_ : ¬b ∈ Iio b)
[PROOFSTEP]
rw [cons_eq_insert, Iio_insert]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ card (Iio a) = card (Iic a) - 1
[PROOFSTEP]
rw [Iic_eq_cons_Iio, card_cons, add_tsub_cancel_right]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b ∪ Ico b c = Ico a c
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c
[PROOFSTEP]
rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
[PROOFSTEP]
exact Set.Ico_subset_Ico_union_Ico
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
[PROOFSTEP]
rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, ← inf_eq_min, ← sup_eq_max, Set.Ico_inter_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : b ≤ c ∨ c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]

| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
rw [Ico_filter_lt_of_right_le h, min_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]

| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (min b c)
[PROOFSTEP]
rw [Ico_filter_lt_of_le_right h, min_eq_right h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : a ≤ c ∨ c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]

| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
rw [Ico_filter_le_of_left_le h, max_eq_right h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]

| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (max a c) b
[PROOFSTEP]
rw [Ico_filter_le_of_le_left h, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ filter (fun x => x < c) (Ioo a b) = Ioo a (min b c)
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝¹ b✝ a b c a✝ : α
⊢ a✝ ∈ filter (fun x => x < c) (Ioo a b) ↔ a✝ ∈ Ioo a (min b c)
[PROOFSTEP]
simp [and_assoc]
[GOAL]
ι : Type u_1
α✝ : Type u_2
inst✝³ : LinearOrder α✝
inst✝² : LocallyFiniteOrder α✝
a✝ b✝ : α✝
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ filter (fun x => x < b) (Iio a) = Iio (min a b)
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α✝ : Type u_2
inst✝³ : LinearOrder α✝
inst✝² : LocallyFiniteOrder α✝
a✝¹ b✝ : α✝
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b a✝ : α
⊢ a✝ ∈ filter (fun x => x < b) (Iio a) ↔ a✝ ∈ Iio (min a b)
[PROOFSTEP]
simp [and_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
  exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
| inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : a ≤ c ∨ c ≤ a
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
cases le_total a c with
| inl h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
  exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
| inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]

| inl h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
  exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
ext x
[GOAL]
case inl.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
x : α
⊢ x ∈ Ico a b \ Ico a c ↔ x ∈ Ico (max a c) b
[PROOFSTEP]
rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
[GOAL]
case inl.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : a ≤ c
x : α
⊢ (a ≤ x ∧ (a ≤ x → c ≤ x)) ∧ x < b ↔ c ≤ x ∧ x < b
[PROOFSTEP]
exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]

| inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ a
⊢ Ico a b \ Ico a c = Ico (max a c) b
[PROOFSTEP]
rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
| inr h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
  exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
x✝ : b ≤ c ∨ c ≤ b
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
cases le_total b c with
| inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
| inr h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
  exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]

| inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : b ≤ c
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]

| inr h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
  exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
⊢ Ico a b \ Ico c b = Ico a (min b c)
[PROOFSTEP]
ext x
[GOAL]
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
x : α
⊢ x ∈ Ico a b \ Ico c b ↔ x ∈ Ico a (min b c)
[PROOFSTEP]
rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
[GOAL]
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ a b c : α
h : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∧ (x < b → x < c) ↔ a ≤ x ∧ x < c
[PROOFSTEP]
exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ disjUnion (Ioi a) (Iio a) (_ : Disjoint (Ioi a) (Iio a)) = {a}ᶜ
[PROOFSTEP]
ext
[GOAL]
case a
ι : Type u_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a a✝ : α
⊢ a✝ ∈ disjUnion (Ioi a) (Iio a) (_ : Disjoint (Ioi a) (Iio a)) ↔ a✝ ∈ {a}ᶜ
[PROOFSTEP]
simp [eq_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : a ≤ b
⊢ [[a, b]] = Icc a b
[PROOFSTEP]
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h : b ≤ a
⊢ [[a, b]] = Icc b a
[PROOFSTEP]
rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α
⊢ [[a, b]] = [[b, a]]
[PROOFSTEP]
rw [uIcc, uIcc, inf_comm, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, a]] = {a}
[PROOFSTEP]
simp [uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]
[PROOFSTEP]
rw [mem_uIcc] at h₁ h₂ 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]
[PROOFSTEP]
exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
[PROOFSTEP]
rw [mem_Icc] at ha hb 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
[PROOFSTEP]
exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b
[PROOFSTEP]
simp_rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b
[PROOFSTEP]
exact Set.eq_of_mem_uIcc_of_mem_uIcc
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c
[PROOFSTEP]
simp_rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c
[PROOFSTEP]
exact Set.eq_of_mem_uIcc_of_mem_uIcc'
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
rw [ext_iff] at h 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (a_1 : α), a_1 ∈ (fun b => [[b, a]]) b ↔ a_1 ∈ (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective (uIcc a)
[PROOFSTEP]
simpa only [uIcc_comm] using uIcc_injective_right a
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ↑[[a, b]] = ↑(Icc a b ∪ Icc b a)
[PROOFSTEP]
push_cast
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
[PROOFSTEP]
exact Set.uIcc_eq_union
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
[PROOFSTEP]
simp [uIcc_eq_union]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ c < a → c < b → ¬c ∈ [[a, b]]
[PROOFSTEP]
rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ c < a → c < b → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
[PROOFSTEP]
exact Set.not_mem_uIcc_of_lt
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a < c → b < c → ¬c ∈ [[a, b]]
[PROOFSTEP]
rw [mem_uIcc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a < c → b < c → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
[PROOFSTEP]
exact Set.not_mem_uIcc_of_gt
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ↑[[a, c]] ⊆ ↑([[a, b]] ∪ [[b, c]])
[PROOFSTEP]
push_cast
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
[PROOFSTEP]
exact Set.uIcc_subset_uIcc_union_uIcc
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Icc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Icc a b = Set.Icc (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Icc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Ico a b = Set.Ico (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Ico _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ico a b = Set.Ico (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Ico _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Ioc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Ioc _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addLeftEmbedding c) '' Set.Ioo a b = Set.Ioo (c + a) (c + b)
[PROOFSTEP]
exact Set.image_const_add_Ioo _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)
[PROOFSTEP]
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑(addRightEmbedding c) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)
[PROOFSTEP]
exact Set.image_add_const_Ioo _ _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Icc a b) = Icc (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Icc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Icc a b) = image (↑(addLeftEmbedding c)) (Icc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ico a b) = Ico (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Ico, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ico a b) = image (↑(addLeftEmbedding c)) (Ico a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioc a b) = Ioc (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Ioc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioc a b) = image (↑(addLeftEmbedding c)) (Ioc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioo a b) = Ioo (c + a) (c + b)
[PROOFSTEP]
rw [← map_add_left_Ioo, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image ((fun x x_1 => x + x_1) c) (Ioo a b) = image (↑(addLeftEmbedding c)) (Ioo a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Icc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Icc a b) = image (↑(addRightEmbedding c)) (Icc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Ico, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ico a b) = image (↑(addRightEmbedding c)) (Ico a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Ioc, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioc a b) = image (↑(addRightEmbedding c)) (Ioc a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)
[PROOFSTEP]
rw [← map_add_right_Ioo, map_eq_image]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioo a b) = image (↑(addRightEmbedding c)) (Ioo a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∏ i : ι, ∏ j in Ioi i, f j i * f i j = ∏ i : ι, ∏ j in {i}ᶜ, f j i
[PROOFSTEP]
simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ (∏ x : ι, ∏ x_1 in Ioi x, f x_1 x) * ∏ x : ι, ∏ x_1 in Ioi x, f x x_1 =
    (∏ x : ι, ∏ x_1 in Ioi x, f x_1 x) * ∏ x : ι, ∏ x_1 in Iio x, f x_1 x
[PROOFSTEP]
congr 1
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∏ x : ι, ∏ x_1 in Ioi x, f x x_1 = ∏ x : ι, ∏ x_1 in Iio x, f x_1 x
[PROOFSTEP]
rw [prod_sigma', prod_sigma']
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∏ x in Finset.sigma univ fun x => Ioi x, f x.fst x.snd = ∏ x in Finset.sigma univ fun x => Iio x, f x.snd x.fst
[PROOFSTEP]
refine' prod_bij' (fun i _ => ⟨i.2, i.1⟩) _ _ (fun i _ => ⟨i.2, i.1⟩) _ _ _
[GOAL]
case e_a.refine'_1
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Ioi x),
    (fun i x => { fst := i.snd, snd := i.fst }) a ha ∈ Finset.sigma univ fun x => Iio x
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_2
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Ioi x),
    f a.fst a.snd =
      f ((fun i x => { fst := i.snd, snd := i.fst }) a ha).snd ((fun i x => { fst := i.snd, snd := i.fst }) a ha).fst
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_3
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Iio x),
    (fun i x => { fst := i.snd, snd := i.fst }) a ha ∈ Finset.sigma univ fun x => Ioi x
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_4
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Ioi x),
    (fun i x => { fst := i.snd, snd := i.fst }) ((fun i x => { fst := i.snd, snd := i.fst }) a ha)
        (_ : { fst := a.snd, snd := a.fst } ∈ Finset.sigma univ fun x => Iio x) =
      a
[PROOFSTEP]
simp
[GOAL]
case e_a.refine'_5
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderTop ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CommMonoid α
f : ι → ι → α
⊢ ∀ (a : (_ : ι) × ι) (ha : a ∈ Finset.sigma univ fun x => Iio x),
    (fun i x => { fst := i.snd, snd := i.fst }) ((fun i x => { fst := i.snd, snd := i.fst }) a ha)
        (_ : { fst := a.snd, snd := a.fst } ∈ Finset.sigma univ fun x => Ioi x) =
      a
[PROOFSTEP]
simp
