n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = filter (fun x => decide (x < n + 1)) (Ico n m)
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = [n]
rw [← filter_lt_of_succ_bot hnm]
no goals
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = filter (fun x => decide (x < n + 1)) (Ico n m)
exact filter_congr' fun _ _ => by
  rw [decide_eq_true_eq, decide_eq_true_eq]
  exact lt_succ_iff.symm
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ x✝¹ ≤ n ↔ x✝¹ < n + 1
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ decide (x✝¹ ≤ n) = true ↔ decide (x✝¹ < n + 1) = true
rw [decide_eq_true_eq, decide_eq_true_eq]
no goals
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ x✝¹ ≤ n ↔ x✝¹ < n + 1
exact lt_succ_iff.symm