case a
ι : Type ?u.32776
α : Type u_1
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
ι : Type ?u.32776
α : Type u_1
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
ext x
case a
ι : Type ?u.32776
α : Type u_1
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
case a
ι : Type ?u.32776
α : Type u_1
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
rw [mem_filter, mem_Ico, mem_Ico, and_comm, and_left_comm]
no goals
case a
ι : Type ?u.32776
α : Type u_1
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
exact and_iff_right_of_imp fun h => hac.trans h.1