[GOAL]
n : ℕ
⊢ Ico 0 n = range n
[PROOFSTEP]
rw [Ico, tsub_zero, range_eq_range']
[GOAL]
n m : ℕ
⊢ List.length (Ico n m) = m - n
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n m : ℕ
⊢ List.length (range' n (m - n)) = m - n
[PROOFSTEP]
simp only [length_range']
[GOAL]
n m : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (Ico n m)
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n m : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (range' n (m - n))
[PROOFSTEP]
simp only [pairwise_lt_range']
[GOAL]
n m : ℕ
⊢ Nodup (Ico n m)
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n m : ℕ
⊢ Nodup (range' n (m - n))
[PROOFSTEP]
simp only [nodup_range']
[GOAL]
n m l : ℕ
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m
[PROOFSTEP]
suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]
[GOAL]
n m l : ℕ
this : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m
[PROOFSTEP]
simp [Ico, this]
[GOAL]
n m l : ℕ
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
[PROOFSTEP]
cases' le_total n m with hnm hmn
[GOAL]
case inl
n m l : ℕ
hnm : n ≤ m
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
[PROOFSTEP]
rw [add_tsub_cancel_of_le hnm]
[GOAL]
case inr
n m l : ℕ
hmn : m ≤ n
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr hmn, add_zero]
[GOAL]
case inr
n m l : ℕ
hmn : m ≤ n
⊢ n ≤ l ∧ l < n ↔ n ≤ l ∧ l < m
[PROOFSTEP]
exact and_congr_right fun hnl => Iff.intro (fun hln => (not_le_of_gt hln hnl).elim) fun hlm => lt_of_lt_of_le hlm hmn
[GOAL]
n m : ℕ
h : m ≤ n
⊢ Ico n m = []
[PROOFSTEP]
simp [Ico, tsub_eq_zero_iff_le.mpr h]
[GOAL]
n m k : ℕ
⊢ map ((fun x x_1 => x + x_1) k) (Ico n m) = Ico (n + k) (m + k)
[PROOFSTEP]
rw [Ico, Ico, map_add_range', add_tsub_add_eq_tsub_right m k, add_comm n k]
[GOAL]
n m k : ℕ
h₁ : k ≤ n
⊢ map (fun x => x - k) (Ico n m) = Ico (n - k) (m - k)
[PROOFSTEP]
rw [Ico, Ico, tsub_tsub_tsub_cancel_right h₁, map_sub_range' _ _ _ h₁]
[GOAL]
n m : ℕ
h : Ico n m = []
⊢ m - n = 0
[PROOFSTEP]
rw [← length, h, List.length]
[GOAL]
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ Ico n m ++ Ico m l = Ico n l
[PROOFSTEP]
dsimp only [Ico]
[GOAL]
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)
[PROOFSTEP]
convert range'_append n (m - n) (l - m) 1 using 2
[GOAL]
case h.e'_2.h.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
[PROOFSTEP]
rw [one_mul, add_tsub_cancel_of_le hnm]
[GOAL]
case h.e'_3.h.e'_2
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = l - m + (m - n)
[PROOFSTEP]
rw [tsub_add_tsub_cancel hml hnm]
[GOAL]
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []
[PROOFSTEP]
apply eq_nil_iff_forall_not_mem.2
[GOAL]
n m l : ℕ
⊢ ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l
[PROOFSTEP]
intro a
[GOAL]
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l
[PROOFSTEP]
simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]
[GOAL]
n m l a : ℕ
⊢ n ≤ a → a < m → m ≤ a → l ≤ a
[PROOFSTEP]
intro _ h₂ h₃
[GOAL]
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ l ≤ a
[PROOFSTEP]
exfalso
[GOAL]
case h
n m l a : ℕ
a✝ : n ≤ a
h₂ : a < m
h₃ : m ≤ a
⊢ False
[PROOFSTEP]
exact not_lt_of_ge h₃ h₂
[GOAL]
n : ℕ
⊢ Ico n (n + 1) = [n]
[PROOFSTEP]
dsimp [Ico]
[GOAL]
n : ℕ
⊢ range' n (n + 1 - n) = [n]
[PROOFSTEP]
simp [range', add_tsub_cancel_left]
[GOAL]
n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]
[PROOFSTEP]
rwa [← succ_singleton, append_consecutive]
[GOAL]
case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1
[PROOFSTEP]
exact Nat.le_succ _
[GOAL]
n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m
[PROOFSTEP]
rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]
[GOAL]
n m : ℕ
h : n < m
⊢ [n] ++ Ico (succ n) m = n :: Ico (n + 1) m
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]
[PROOFSTEP]
dsimp [Ico]
[GOAL]
m : ℕ
h : 0 < m
⊢ range' (m - 1) (m - (m - 1)) = [m - 1]
[PROOFSTEP]
rw [tsub_tsub_cancel_of_le (succ_le_of_lt h)]
[GOAL]
m : ℕ
h : 0 < m
⊢ range' (m - 1) (succ 0) = [m - 1]
[PROOFSTEP]
simp [← Nat.one_eq_succ_zero]
[GOAL]
n m : ℕ
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
by_cases n < m
[GOAL]
n m : ℕ
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
by_cases n < m
[GOAL]
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
rw [eq_cons h]
[GOAL]
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (n :: Ico (n + 1) m)
[PROOFSTEP]
exact chain_succ_range' _ _ 1
[GOAL]
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)
[PROOFSTEP]
rw [eq_nil_of_le (le_of_not_gt h)]
[GOAL]
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) []
[PROOFSTEP]
trivial
[GOAL]
n m : ℕ
⊢ ¬m ∈ Ico n m
[PROOFSTEP]
simp
[GOAL]
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ decide (k < l) = true
[PROOFSTEP]
simp only [(lt_of_lt_of_le (mem.1 hk).2 hml), decide_True]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true
[PROOFSTEP]
simp only [decide_eq_true_eq, not_lt]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
[PROOFSTEP]
apply le_trans hln
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k
[PROOFSTEP]
exact (mem.1 hk).1
[GOAL]
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
[PROOFSTEP]
cases' le_total n l with hnl hln
[GOAL]
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
[PROOFSTEP]
rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l), filter_lt_of_le_bot (le_refl l),
  append_nil]
[GOAL]
case inr
n m l : ℕ
hlm : l ≤ m
hln : l ≤ n
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n l
[PROOFSTEP]
rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]
[GOAL]
n m l : ℕ
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
[PROOFSTEP]
cases' le_total m l with hml hlm
[GOAL]
case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
[PROOFSTEP]
rw [min_eq_left hml, filter_lt_of_top_le hml]
[GOAL]
case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (min m l)
[PROOFSTEP]
rw [min_eq_right hlm, filter_lt_of_ge hlm]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true
[PROOFSTEP]
rw [decide_eq_true_eq]
[GOAL]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
[PROOFSTEP]
exact le_trans hln (mem.1 hk).1
[GOAL]
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true
[PROOFSTEP]
rw [decide_eq_true_eq]
[GOAL]
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k
[PROOFSTEP]
exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)
[GOAL]
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
[PROOFSTEP]
cases' le_total l m with hlm hml
[GOAL]
case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
[PROOFSTEP]
rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l), filter_le_of_le_bot (le_refl l),
  nil_append]
[GOAL]
case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
[PROOFSTEP]
rw [eq_nil_of_le hml, filter_le_of_top_le hml]
[GOAL]
n m l : ℕ
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
[PROOFSTEP]
cases' le_total n l with hnl hln
[GOAL]
case inl
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
[PROOFSTEP]
rw [max_eq_right hnl, filter_le_of_le hnl]
[GOAL]
case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
[PROOFSTEP]
rw [max_eq_left hln, filter_le_of_le_bot hln]
[GOAL]
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
[PROOFSTEP]
have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm
[GOAL]
n m : ℕ
hnm : n < m
r : min m (n + 1) = n + 1
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
[PROOFSTEP]
simp [filter_lt n m (n + 1), r]
[GOAL]
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = [n]
[PROOFSTEP]
rw [← filter_lt_of_succ_bot hnm]
[GOAL]
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = filter (fun x => decide (x < n + 1)) (Ico n m)
[PROOFSTEP]
exact
  filter_congr' fun _ _ => by
    rw [decide_eq_true_eq, decide_eq_true_eq]
    exact lt_succ_iff.symm
[GOAL]
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ decide (x✝¹ ≤ n) = true ↔ decide (x✝¹ < n + 1) = true
[PROOFSTEP]
rw [decide_eq_true_eq, decide_eq_true_eq]
[GOAL]
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ x✝¹ ≤ n ↔ x✝¹ < n + 1
[PROOFSTEP]
exact lt_succ_iff.symm
[GOAL]
n a b : ℕ
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
by_cases h₁ : n < a
[GOAL]
case pos
n a b : ℕ
h₁ : n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
left
[GOAL]
case pos.h
n a b : ℕ
h₁ : n < a
⊢ n < a
[PROOFSTEP]
exact h₁
[GOAL]
case neg
n a b : ℕ
h₁ : ¬n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
right
[GOAL]
case neg.h
n a b : ℕ
h₁ : ¬n < a
⊢ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
by_cases h₂ : n ∈ Ico a b
[GOAL]
case pos
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
right
[GOAL]
case pos.h
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ n ∈ Ico a b
[PROOFSTEP]
exact h₂
[GOAL]
case neg
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b
[PROOFSTEP]
left
[GOAL]
case neg.h
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n
[PROOFSTEP]
simp only [Ico.mem, not_and, not_lt] at *
[GOAL]
case neg.h
n a b : ℕ
h₁ : a ≤ n
h₂ : a ≤ n → b ≤ n
⊢ b ≤ n
[PROOFSTEP]
exact h₂ h₁
