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

Proof state:
case mp.intro.intro.intro
n k : Nat
h : k ≤ n
⊢ ∃ k_1,
    k_1 ≤ n ∧
      (range' (1 + k) (n - k)).reverse = (range' (k_1 + 1) (n - k_1)).reverse ∧
        (range' 1 k).reverse = (range' 1 k_1).reverse

Tactic:
simp

Result:
case mp.intro.intro.intro
n k : Nat
h : k ≤ n
⊢ k ≤ n ∧ (n - k = 0 ∨ 1 + k = k + 1)

Proof state:
n k : Nat
h : k ≤ n
⊢ k ≤ n ∧
    (range' 1 k).reverse = (range' 1 k).reverse ∧ (range' (k + 1) (n - k)).reverse = (range' (1 + k) (n - k)).reverse

Tactic:
simp

Result:
n k : Nat
h : k ≤ n
⊢ k ≤ n ∧ (n - k = 0 ∨ k + 1 = 1 + k)

Proof state:
case mpr.intro.intro.intro
n k : Nat
h : k ≤ n
⊢ ∃ k_1,
    k_1 ≤ n ∧
      (range' 1 k).reverse = (range' 1 k_1).reverse ∧
        (range' (k + 1) (n - k)).reverse = (range' (1 + k_1) (n - k_1)).reverse

Tactic:
exact ⟨k, by simp; omega⟩

Result:
no goals

Proof state:
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ ys = (range' 1 k).reverse ∧ xs = (range' (1 + k) (n - k)).reverse) ↔
    ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Tactic:
constructor

Result:
case mp
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ ys = (range' 1 k).reverse ∧ xs = (range' (1 + k) (n - k)).reverse) →
    ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

case mpr
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse) →
    ∃ k, k ≤ n ∧ ys = (range' 1 k).reverse ∧ xs = (range' (1 + k) (n - k)).reverse

Proof state:
case mp
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ ys = (range' 1 k).reverse ∧ xs = (range' (1 + k) (n - k)).reverse) →
    ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

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

Result:
case mp.intro.intro.intro
n k : Nat
h : k ≤ n
⊢ ∃ k_1,
    k_1 ≤ n ∧
      (range' (1 + k) (n - k)).reverse = (range' (k_1 + 1) (n - k_1)).reverse ∧
        (range' 1 k).reverse = (range' 1 k_1).reverse

Proof state:
n : Nat
xs ys : List Nat
⊢ (range' 1 n).reverse = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Tactic:
rw [reverse_eq_append_iff]

Result:
n : Nat
xs ys : List Nat
⊢ range' 1 n = ys.reverse ++ xs.reverse ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Proof state:
case mpr
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse) →
    ∃ k, k ≤ n ∧ ys = (range' 1 k).reverse ∧ xs = (range' (1 + k) (n - k)).reverse

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

Result:
case mpr.intro.intro.intro
n k : Nat
h : k ≤ n
⊢ ∃ k_1,
    k_1 ≤ n ∧
      (range' 1 k).reverse = (range' 1 k_1).reverse ∧
        (range' (k + 1) (n - k)).reverse = (range' (1 + k_1) (n - k_1)).reverse

Proof state:
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ ys.reverse = range' 1 k ∧ xs.reverse = range' (1 + k) (n - k)) ↔
    ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Tactic:
simp only [reverse_eq_iff]

Result:
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ ys = (range' 1 k).reverse ∧ xs = (range' (1 + k) (n - k)).reverse) ↔
    ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Proof state:
n : Nat
xs ys : List Nat
⊢ range' 1 n = ys.reverse ++ xs.reverse ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Tactic:
rw [range'_eq_append_iff]

Result:
n : Nat
xs ys : List Nat
⊢ (∃ k, k ≤ n ∧ ys.reverse = range' 1 k ∧ xs.reverse = range' (1 + k) (n - k)) ↔
    ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Proof state:
case mp.intro.intro.intro
n k : Nat
h : k ≤ n
⊢ k ≤ n ∧ (n - k = 0 ∨ 1 + k = k + 1)

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
xs ys : List Nat
⊢ iota n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = iota k

Tactic:
simp only [iota_eq_reverse_range']

Result:
n : Nat
xs ys : List Nat
⊢ (range' 1 n).reverse = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = (range' 1 k).reverse

Proof state:
n k : Nat
h : k ≤ n
⊢ k ≤ n ∧ (n - k = 0 ∨ k + 1 = 1 + k)

Tactic:
omega

Result:
no goals