[GOAL]
m n r : ℤ
⊢ r ∈ range m n ↔ m ≤ r ∧ r < n
[PROOFSTEP]
simp only [range, List.mem_map, List.mem_range, lt_toNat, lt_sub_iff_add_lt, add_comm]
[GOAL]
m n r : ℤ
⊢ (∃ a, m + ↑a < n ∧ m + ↑a = r) ↔ m ≤ r ∧ r < n
[PROOFSTEP]
exact
  ⟨fun ⟨a, ha⟩ => ha.2 ▸ ⟨le_add_of_nonneg_right (Int.coe_nat_nonneg _), ha.1⟩, fun h =>
    ⟨toNat (r - m), by simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]⟩⟩
[GOAL]
m n r : ℤ
h : m ≤ r ∧ r < n
⊢ m + ↑(toNat (r - m)) < n ∧ m + ↑(toNat (r - m)) = r
[PROOFSTEP]
simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ range m n → P r) ↔ ∀ (r : ℤ), m ≤ r → r < n → P r
[PROOFSTEP]
simp only [mem_range_iff, and_imp]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ Decidable (∀ (r : ℤ), m ≤ r → r ≤ n → P r)
[PROOFSTEP]
apply decidable_of_iff (∀ r ∈ range m (n + 1), P r)
[GOAL]
case h
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ range m (n + 1) → P r) ↔ ∀ (r : ℤ), m ≤ r → r ≤ n → P r
[PROOFSTEP]
apply Iff.intro
[GOAL]
case h.mp
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ range m (n + 1) → P r) → ∀ (r : ℤ), m ≤ r → r ≤ n → P r
[PROOFSTEP]
intros h _ _
[GOAL]
case h.mpr
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), m ≤ r → r ≤ n → P r) → ∀ (r : ℤ), r ∈ range m (n + 1) → P r
[PROOFSTEP]
intros h _ _
[GOAL]
case h.mp
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), r ∈ range m (n + 1) → P r
r✝ : ℤ
a✝ : m ≤ r✝
⊢ r✝ ≤ n → P r✝
[PROOFSTEP]
intro _
[GOAL]
case h.mp
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), r ∈ range m (n + 1) → P r
r✝ : ℤ
a✝¹ : m ≤ r✝
a✝ : r✝ ≤ n
⊢ P r✝
[PROOFSTEP]
apply h
[GOAL]
case h.mp.a
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), r ∈ range m (n + 1) → P r
r✝ : ℤ
a✝¹ : m ≤ r✝
a✝ : r✝ ≤ n
⊢ r✝ ∈ range m (n + 1)
[PROOFSTEP]
simp_all only [mem_range_iff, and_imp, lt_add_one_iff]
[GOAL]
case h.mpr
P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
h : ∀ (r : ℤ), m ≤ r → r ≤ n → P r
r✝ : ℤ
a✝ : r✝ ∈ range m (n + 1)
⊢ P r✝
[PROOFSTEP]
simp_all only [mem_range_iff, and_imp, lt_add_one_iff]
