-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem size_eq (r : Std.Range) (h : i < r.stop) :
    (r.stop - i + r.step - 1) / r.step =
      (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
this✝ : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤ r.stop - (i + r.step) + r.step - 1
this : r.stop - (i + r.step) + r.step - 1 - r.step < (r.stop - (i + r.step) + r.step - 1) / r.step * r.step
⊢ r.stop - i + r.step - 1 ≤ (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step + r.step - 1 ∧
    (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step ≤ r.stop - i + r.step - 1

Tactic:
omega

Result:
no goals

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
⊢ r.stop - i + r.step - 1 ≤ r.step + r.step - 1 ∧ r.step ≤ r.stop - i + r.step - 1

Tactic:
omega

Result:
no goals

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Tactic:
rw [Nat.div_eq_iff w, Nat.add_one_mul]

Result:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
⊢ r.stop - i + r.step - 1 ≤ (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step + r.step - 1 ∧
    (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step ≤ r.stop - i + r.step - 1

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
this : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤ r.stop - (i + r.step) + r.step - 1
⊢ r.step ≤ r.stop - (i + r.step) + r.step - 1

Tactic:
omega

Result:
no goals

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
⊢ r.stop - i + r.step - 1 ≤ (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step + r.step - 1 ∧
    (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step ≤ r.stop - i + r.step - 1

Tactic:
have : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤
    (r.stop - (i + r.step) + r.step - 1) := Nat.div_mul_le_self _ _

Result:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
this : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤ r.stop - (i + r.step) + r.step - 1
⊢ r.stop - i + r.step - 1 ≤ (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step + r.step - 1 ∧
    (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step ≤ r.stop - i + r.step - 1

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
this : (r.stop - i + r.step - 1) / r.step = 1
⊢ (r.stop - (i + r.step) + r.step - 1) / r.step = 0

Tactic:
rw [Nat.div_eq_iff] <;> omega

Result:
no goals

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Tactic:
if i + r.step < r.stop then rw [Nat.div_eq_iff w, Nat.add_one_mul]
  have : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤
      (r.stop - (i + r.step) + r.step - 1) := Nat.div_mul_le_self _ _
  have : r.stop - (i + r.step) + r.step - 1 - r.step <
      (r.stop - (i + r.step) + r.step - 1) / r.step * r.step :=
    Nat.lt_div_mul_self w (by omega)
  omega
else
  have : (r.stop - i + r.step - 1) / r.step = 1 := by
    rw [Nat.div_eq_iff w, Nat.one_mul]
    omega
  have : (r.stop - (i + r.step) + r.step - 1) / r.step = 0 := by
    rw [Nat.div_eq_iff] <;> omega
  omega

Result:
no goals

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
this✝ : (r.stop - i + r.step - 1) / r.step = 1
this : (r.stop - (i + r.step) + r.step - 1) / r.step = 0
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Tactic:
omega

Result:
no goals

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Tactic:
have : (r.stop - i + r.step - 1) / r.step = 1 := by
  rw [Nat.div_eq_iff w, Nat.one_mul]
  omega

Result:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
this : (r.stop - i + r.step - 1) / r.step = 1
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
⊢ (r.stop - i + r.step - 1) / r.step = 1

Tactic:
rw [Nat.div_eq_iff w, Nat.one_mul]

Result:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
⊢ r.stop - i + r.step - 1 ≤ r.step + r.step - 1 ∧ r.step ≤ r.stop - i + r.step - 1

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
this : (r.stop - i + r.step - 1) / r.step = 1
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Tactic:
have : (r.stop - (i + r.step) + r.step - 1) / r.step = 0 := by
  rw [Nat.div_eq_iff] <;> omega

Result:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : ¬i + r.step < r.stop
this✝ : (r.stop - i + r.step - 1) / r.step = 1
this : (r.stop - (i + r.step) + r.step - 1) / r.step = 0
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Proof state:
i : Nat
r : Range
h : i < r.stop
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Tactic:
have w := r.step_pos

Result:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
⊢ (r.stop - i + r.step - 1) / r.step = (r.stop - (i + r.step) + r.step - 1) / r.step + 1

Proof state:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
this : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤ r.stop - (i + r.step) + r.step - 1
⊢ r.stop - i + r.step - 1 ≤ (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step + r.step - 1 ∧
    (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step ≤ r.stop - i + r.step - 1

Tactic:
have : r.stop - (i + r.step) + r.step - 1 - r.step <
    (r.stop - (i + r.step) + r.step - 1) / r.step * r.step :=
  Nat.lt_div_mul_self w (by omega)

Result:
i : Nat
r : Range
h : i < r.stop
w : 0 < r.step
h✝ : i + r.step < r.stop
this✝ : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤ r.stop - (i + r.step) + r.step - 1
this : r.stop - (i + r.step) + r.step - 1 - r.step < (r.stop - (i + r.step) + r.step - 1) / r.step * r.step
⊢ r.stop - i + r.step - 1 ≤ (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step + r.step - 1 ∧
    (r.stop - (i + r.step) + r.step - 1) / r.step * r.step + r.step ≤ r.stop - i + r.step - 1