-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem iota_eq_cons_iff : iota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = iota (n - 1)

Proof state:
case mp.intro.intro.intro
n a k : Nat
h : k ≤ n
h' : 1 + k = a ∧ n - k = 1
⊢ n = a ∧ 0 < n ∧ k = n - 1

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro.intro
n a k : Nat
h : k ≤ n
h' : [a] = range' (1 + k) (n - k)
⊢ n = a ∧ 0 < n ∧ (range' 1 k).reverse = (range' 1 (n - 1)).reverse

Tactic:
rw [eq_comm, range'_eq_singleton] at h'

Result:
case mp.intro.intro.intro
n a k : Nat
h : k ≤ n
h' : 1 + k = a ∧ n - k = 1
⊢ n = a ∧ 0 < n ∧ (range' 1 k).reverse = (range' 1 (n - 1)).reverse

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

Tactic:
constructor

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

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

Proof state:
n a : Nat
xs : List Nat
⊢ iota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = iota (n - 1)

Tactic:
simp [iota_eq_reverse_range']

Result:
n a : Nat
xs : List Nat
⊢ range' 1 n = xs.reverse ++ [a] ↔ n = a ∧ 0 < n ∧ xs = (range' 1 (n - 1)).reverse

Proof state:
case mpr.intro.intro
n : Nat
h : 0 < n
⊢ [n] = range' (1 + (n - 1)) (n - (n - 1))

Tactic:
rw [eq_comm, range'_eq_singleton]

Result:
case mpr.intro.intro
n : Nat
h : 0 < n
⊢ 1 + (n - 1) = n ∧ n - (n - 1) = 1

Proof state:
n a : Nat
xs : List Nat
⊢ range' 1 n = xs.reverse ++ [a] ↔ n = a ∧ 0 < n ∧ xs = (range' 1 (n - 1)).reverse

Tactic:
simp [range'_eq_append_iff, reverse_eq_iff]

Result:
n a : Nat
xs : List Nat
⊢ (∃ k, k ≤ n ∧ xs = (range' 1 k).reverse ∧ [a] = range' (1 + k) (n - k)) ↔
    n = a ∧ 0 < n ∧ xs = (range' 1 (n - 1)).reverse

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

Tactic:
rintro ⟨rfl, h, rfl⟩

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

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

Tactic:
refine ⟨n - 1, by simp, rfl, ?_⟩

Result:
case mpr.intro.intro
n : Nat
h : 0 < n
⊢ [n] = range' (1 + (n - 1)) (n - (n - 1))

Proof state:
n : Nat
h : 0 < n
⊢ n - 1 ≤ n

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro.intro
n a k : Nat
h : k ≤ n
h' : 1 + k = a ∧ n - k = 1
⊢ n = a ∧ 0 < n ∧ (range' 1 k).reverse = (range' 1 (n - 1)).reverse

Tactic:
simp only [reverse_inj, range'_inj, or_true, and_true]

Result:
case mp.intro.intro.intro
n a k : Nat
h : k ≤ n
h' : 1 + k = a ∧ n - k = 1
⊢ n = a ∧ 0 < n ∧ k = n - 1

Proof state:
case mpr.intro.intro
n : Nat
h : 0 < n
⊢ 1 + (n - 1) = n ∧ n - (n - 1) = 1

Tactic:
omega

Result:
no goals

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

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

Result:
case mp.intro.intro.intro
n a k : Nat
h : k ≤ n
h' : [a] = range' (1 + k) (n - k)
⊢ n = a ∧ 0 < n ∧ (range' 1 k).reverse = (range' 1 (n - 1)).reverse