-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_eq_append_iff : range' s (n + m) = xs ++ ys ↔ xs = range' s n ∧ ys = range' (s + n) m

Proof state:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
⊢ (∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)) ↔
    xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m

Tactic:
constructor

Result:
case mp
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
⊢ (∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)) →
    xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m

case mpr
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
⊢ xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m →
    ∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)

Proof state:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
h₁ : xs.toArray = Array.range' s n
h₂ : ys.toArray = Array.range' (s + n) m
⊢ m = n + m - n

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro.intro
s m : Nat
ys : Vector Nat m
k : Nat
xs : Vector Nat k
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (k + m - k)
⊢ k + m - k = m

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro.intro
s m : Nat
ys : Vector Nat m
k : Nat
xs : Vector Nat k
hk : k ≤ k + m
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (k + m - k)
⊢ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) m

Tactic:
simp_all

Result:
case mp.intro.intro.intro
s m : Nat
ys : Vector Nat m
k : Nat
xs : Vector Nat k
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (k + m - k)
⊢ k + m - k = m

Proof state:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
⊢ range' s (n + m) = xs ++ ys ↔ xs = range' s n ∧ ys = range' (s + n) m

Tactic:
simp only [← toArray_inj, toArray_range', toArray_append, Array.range'_eq_append_iff]

Result:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
⊢ (∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)) ↔
    xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m

Proof state:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
h₁ : xs.toArray = Array.range' s n
h₂ : ys.toArray = Array.range' (s + n) m
⊢ xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) (n + m - n)

Tactic:
simp_all

Result:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
h₁ : xs.toArray = Array.range' s n
h₂ : ys.toArray = Array.range' (s + n) m
⊢ m = n + m - n

Proof state:
case mpr
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
⊢ xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m →
    ∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
h₁ : xs.toArray = Array.range' s n
h₂ : ys.toArray = Array.range' (s + n) m
⊢ ∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)

Proof state:
case mp.intro.intro.intro
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
k : Nat
hk : k ≤ n + m
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (n + m - k)
⊢ xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m

Tactic:
have w : k = n := by
  replace h₁ := congrArg Array.size h₁
  simp_all

Result:
case mp.intro.intro.intro
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
k : Nat
hk : k ≤ n + m
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (n + m - k)
w : k = n
⊢ xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m

Proof state:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
k : Nat
hk : k ≤ n + m
h₂ : ys.toArray = Array.range' (s + k) (n + m - k)
h₁ : xs.size = (Array.range' s k).size
⊢ k = n

Tactic:
simp_all

Result:
no goals

Proof state:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
h₁ : xs.toArray = Array.range' s n
h₂ : ys.toArray = Array.range' (s + n) m
⊢ n ≤ n + m

Tactic:
omega

Result:
no goals

Proof state:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
k : Nat
hk : k ≤ n + m
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (n + m - k)
⊢ k = n

Tactic:
replace h₁ := congrArg Array.size h₁

Result:
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
k : Nat
hk : k ≤ n + m
h₂ : ys.toArray = Array.range' (s + k) (n + m - k)
h₁ : xs.size = (Array.range' s k).size
⊢ k = n

Proof state:
case mpr.intro
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
h₁ : xs.toArray = Array.range' s n
h₂ : ys.toArray = Array.range' (s + n) m
⊢ ∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)

Tactic:
exact ⟨n, by omega, by simp_all; omega⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
k : Nat
hk : k ≤ n + m
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (n + m - k)
w : k = n
⊢ xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m

Tactic:
subst w

Result:
case mp.intro.intro.intro
s m : Nat
ys : Vector Nat m
k : Nat
xs : Vector Nat k
hk : k ≤ k + m
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (k + m - k)
⊢ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) m

Proof state:
case mp
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
⊢ (∃ k, k ≤ n + m ∧ xs.toArray = Array.range' s k ∧ ys.toArray = Array.range' (s + k) (n + m - k)) →
    xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m

Tactic:
rintro ⟨k, hk, h₁, h₂⟩

Result:
case mp.intro.intro.intro
s n m : Nat
xs : Vector Nat n
ys : Vector Nat m
k : Nat
hk : k ≤ n + m
h₁ : xs.toArray = Array.range' s k
h₂ : ys.toArray = Array.range' (s + k) (n + m - k)
⊢ xs.toArray = Array.range' s n ∧ ys.toArray = Array.range' (s + n) m