-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)

Proof state:
case succ.mpr.intro.intro.intro.succ
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s k : Nat
h : k + 1 ≤ n + 1
⊢ range' s (k + 1) = [] ∧ range' (s + (k + 1)) (n + 1 - (k + 1)) = s :: range' (s + 1) n ∨
    ∃ a', range' s (k + 1) = s :: a' ∧ range' (s + 1) n = a' ++ range' (s + (k + 1)) (n + 1 - (k + 1))

Tactic:
simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or]

Result:
case succ.mpr.intro.intro.intro.succ
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s k : Nat
h : k + 1 ≤ n + 1
⊢ ∃ k_1, k_1 ≤ n ∧ k = k_1 ∧ n + 1 - (k + 1) = n - k_1 ∧ (n + 1 - (k + 1) = 0 ∨ s + (k + 1) = s + 1 + k_1)

Proof state:
case succ.mp.inr.intro.intro.intro.intro.intro
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s k : Nat
h : k ≤ n
⊢ ∃ k_1,
    k_1 ≤ n + 1 ∧ s :: range' (s + 1) k = range' s k_1 ∧ range' (s + 1 + k) (n - k) = range' (s + k_1) (n + 1 - k_1)

Tactic:
refine ⟨k + 1, ?_⟩

Result:
case succ.mp.inr.intro.intro.intro.intro.intro
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s k : Nat
h : k ≤ n
⊢ k + 1 ≤ n + 1 ∧
    s :: range' (s + 1) k = range' s (k + 1) ∧ range' (s + 1 + k) (n - k) = range' (s + (k + 1)) (n + 1 - (k + 1))

Proof state:
case succ.mpr.intro.intro.intro
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s k : Nat
h : k ≤ n + 1
⊢ range' s k = [] ∧ range' (s + k) (n + 1 - k) = s :: range' (s + 1) n ∨
    ∃ a', range' s k = s :: a' ∧ range' (s + 1) n = a' ++ range' (s + k) (n + 1 - k)

Tactic:
cases k with
| zero => simp [range'_succ]
| succ k =>
  simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or]
  refine ⟨k, ?_⟩
  simp_all
  omega

Result:
no goals

Proof state:
case succ.mp.inr.intro.intro
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s : Nat
ys a : List Nat
h : ∃ k, k ≤ n ∧ a = range' (s + 1) k ∧ ys = range' (s + 1 + k) (n - k)
⊢ ∃ k, k ≤ n + 1 ∧ s :: a = range' s k ∧ ys = range' (s + k) (n + 1 - k)

Tactic:
obtain ⟨k, h, rfl, rfl⟩ := h

Result:
case succ.mp.inr.intro.intro.intro.intro.intro
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s k : Nat
h : k ≤ n
⊢ ∃ k_1,
    k_1 ≤ n + 1 ∧ s :: range' (s + 1) k = range' s k_1 ∧ range' (s + 1 + k) (n - k) = range' (s + k_1) (n + 1 - k_1)

Proof state:
case zero
s : Nat
xs ys : List Nat
⊢ range' s 0 = xs ++ ys ↔ ∃ k, k ≤ 0 ∧ xs = range' s k ∧ ys = range' (s + k) (0 - k)

Tactic:
simp

Result:
no goals

Proof state:
case succ.mp.inl.intro
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s : Nat
⊢ ∃ k, k ≤ n + 1 ∧ [] = range' s k ∧ s :: range' (s + 1) n = range' (s + k) (n + 1 - k)

Tactic:
exact ⟨0, by simp [range'_succ]⟩

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s : Nat
xs ys : List Nat
⊢ range' s (n + 1) = xs ++ ys ↔ ∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)

Tactic:
simp only [range'_succ]

Result:
case succ
n : Nat
ih : ∀ {s : Nat} {xs ys : List Nat}, range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
s : Nat
xs ys : List Nat
⊢ s :: range' (s + 1) n = xs ++ ys ↔ ∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)