-- 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.zero
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
h : 0 ≤ n + 1
⊢ range' s 0 = [] ∧ range' (s + 0) (n + 1 - 0) = s :: range' (s + 1) n ∨
    ∃ a', range' s 0 = s :: a' ∧ range' (s + 1) n = a' ++ range' (s + 0) (n + 1 - 0)

Tactic:
simp [range'_succ]

Result:
no goals

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
⊢ n - k = n + 1 - (k + 1) ∧ (n - k = 0 ∨ s + 1 + k = s + (k + 1))

Tactic:
omega

Result:
no goals

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 ≤ 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:
simp_all [range'_succ]

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
⊢ n - k = n + 1 - (k + 1) ∧ (n - k = 0 ∨ s + 1 + k = s + (k + 1))

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 : range' (s + 1) n = a ++ ys
⊢ ∃ k, k ≤ n + 1 ∧ s :: a = range' s k ∧ ys = range' (s + k) (n + 1 - k)

Tactic:
simp only [ih] at h

Result:
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)

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
⊢ s :: range' (s + 1) n = xs ++ ys ↔ ∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)

Tactic:
rw [cons_eq_append_iff]

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
⊢ (xs = [] ∧ ys = s :: range' (s + 1) n ∨ ∃ a', xs = s :: a' ∧ range' (s + 1) n = a' ++ ys) ↔
    ∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - 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
⊢ ∃ 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)

Tactic:
refine ⟨k, ?_⟩

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 ≤ n ∧ k = k ∧ n + 1 - (k + 1) = n - k ∧ (n + 1 - (k + 1) = 0 ∨ s + (k + 1) = s + 1 + k)

Proof state:
case succ.mp
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
⊢ (xs = [] ∧ ys = s :: range' (s + 1) n ∨ ∃ a', xs = s :: a' ∧ range' (s + 1) n = a' ++ ys) →
    ∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨a, rfl, h⟩)

Result:
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)

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 : range' (s + 1) n = a ++ ys
⊢ ∃ k, k ≤ n + 1 ∧ s :: a = range' s k ∧ ys = range' (s + k) (n + 1 - k)

Proof state:
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
⊢ 0 ≤ n + 1 ∧ [] = range' s 0 ∧ s :: range' (s + 1) n = range' (s + 0) (n + 1 - 0)

Tactic:
simp [range'_succ]

Result:
no goals

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 ≤ n
⊢ n + 1 - (k + 1) = n - k ∧ (n + 1 - (k + 1) = 0 ∨ s + (k + 1) = s + 1 + k)

Tactic:
omega

Result:
no goals

Proof state:
case succ.mpr
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
⊢ (∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)) →
    xs = [] ∧ ys = s :: range' (s + 1) n ∨ ∃ a', xs = s :: a' ∧ range' (s + 1) n = a' ++ ys

Tactic:
rintro ⟨k, h, rfl, rfl⟩

Result:
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)

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
⊢ k ≤ n ∧ k = k ∧ n + 1 - (k + 1) = n - k ∧ (n + 1 - (k + 1) = 0 ∨ s + (k + 1) = s + 1 + k)

Tactic:
simp_all

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 ≤ n
⊢ n + 1 - (k + 1) = n - k ∧ (n + 1 - (k + 1) = 0 ∨ s + (k + 1) = s + 1 + k)

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
⊢ (xs = [] ∧ ys = s :: range' (s + 1) n ∨ ∃ a', xs = s :: a' ∧ range' (s + 1) n = a' ++ ys) ↔
    ∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)

Tactic:
constructor

Result:
case succ.mp
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
⊢ (xs = [] ∧ ys = s :: range' (s + 1) n ∨ ∃ a', xs = s :: a' ∧ range' (s + 1) n = a' ++ ys) →
    ∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)

case succ.mpr
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
⊢ (∃ k, k ≤ n + 1 ∧ xs = range' s k ∧ ys = range' (s + k) (n + 1 - k)) →
    xs = [] ∧ ys = s :: range' (s + 1) n ∨ ∃ a', xs = s :: a' ∧ range' (s + 1) n = a' ++ ys