no goals
m s step : Nat
⊢ m ∈ range' s 0 step ↔ ∃ i, i < 0 ∧ m = s + step * i
simp [range', Nat.not_lt_zero]
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i
m s step n : Nat
⊢ m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i
have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n := by cases i <;> simp [Nat.succ_le]
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a, (∃ j, a = succ j ∧ j < n) ∧ m = s + step * a
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i
simp [range', mem_range', Nat.lt_succ, h]
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a x, a = succ x ∧ x < n ∧ m = s + step * a
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a, (∃ j, a = succ j ∧ j < n) ∧ m = s + step * a
simp only [← exists_and_right, and_assoc]
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ b a, a = succ b ∧ b < n ∧ m = s + step * a
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a x, a = succ x ∧ x < n ∧ m = s + step * a
rw [exists_comm]
no goals
m s step n : Nat
h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
⊢ (m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ b a, a = succ b ∧ b < n ∧ m = s + step * a
simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
no goals
m s step n i : Nat
⊢ i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n
cases i <;> simp [Nat.succ_le]