-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_append (s m n step : Nat) :
    range' s m step ++ range' (s + step * m) n step = range' s (m + n) step

Proof state:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
h : m ≤ i
⊢ s + step * m + (step * i - step * m) = s + step * i

Tactic:
have : step * m ≤ step * i := by exact mul_le_mul_left step h

Result:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
h : m ≤ i
this : step * m ≤ step * i
⊢ s + step * m + (step * i - step * m) = s + step * i

Proof state:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
h : m ≤ i
this : step * m ≤ step * i
⊢ s + step * m + (step * i - step * m) = s + step * i

Tactic:
omega

Result:
no goals

Proof state:
case h₁
s m n step : Nat
⊢ (range' s m step ++ range' (s + step * m) n step).size = (range' s (m + n) step).size

Tactic:
simp

Result:
no goals

Proof state:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
⊢ m ≤ i → s + step * m + (step * i - step * m) = s + step * i

Tactic:
intro h

Result:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
h : m ≤ i
⊢ s + step * m + (step * i - step * m) = s + step * i

Proof state:
case h₂
s m n step i : Nat
h₁ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂ : i < (range' s (m + n) step).size
⊢ (range' s m step ++ range' (s + step * m) n step)[i] = (range' s (m + n) step)[i]

Tactic:
simp only [size_append, size_range'] at h₁ h₂

Result:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
⊢ (range' s m step ++ range' (s + step * m) n step)[i] = (range' s (m + n) step)[i]

Proof state:
s m n step : Nat
⊢ range' s m step ++ range' (s + step * m) n step = range' s (m + n) step

Tactic:
ext i h₁ h₂

Result:
case h₁
s m n step : Nat
⊢ (range' s m step ++ range' (s + step * m) n step).size = (range' s (m + n) step).size

case h₂
s m n step i : Nat
h₁ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂ : i < (range' s (m + n) step).size
⊢ (range' s m step ++ range' (s + step * m) n step)[i] = (range' s (m + n) step)[i]

Proof state:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
⊢ (range' s m step ++ range' (s + step * m) n step)[i] = (range' s (m + n) step)[i]

Tactic:
simp only [getElem_append, size_range', getElem_range', Nat.mul_sub_left_distrib, dite_eq_ite,
  ite_eq_left_iff, Nat.not_lt]

Result:
case h₂
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
⊢ m ≤ i → s + step * m + (step * i - step * m) = s + step * i

Proof state:
s m n step i : Nat
h₁✝ : i < (range' s m step ++ range' (s + step * m) n step).size
h₂✝ : i < (range' s (m + n) step).size
h₁ h₂ : i < m + n
h : m ≤ i
⊢ step * m ≤ step * i

Tactic:
exact mul_le_mul_left step h

Result:
no goals