-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_eq_append_iff {a : Vector α n} {b : Vector α m} {c : Vector α k} {d : Vector α l}
    (w : k + l = n + m) :
    a ++ b = (c ++ d).cast w ↔
      if h : n ≤ k then
        ∃ a' : Vector α (k - n), c = (a ++ a').cast (by omega) ∧ b = (a' ++ d).cast (by omega)
      else
        ∃ c' : Vector α (n - k), a = (c ++ c').cast (by omega) ∧ d = (c' ++ b).cast (by omega)

Proof state:
case mk.mk.mk.mk.mpr.isFalse.intro.intro
α : Type u_1
a b c : Array α
h : ¬a.size ≤ c.size
c' : Vector α (a.size - c.size)
ha : a = ({ toArray := c, size_toArray := ⋯ } ++ c').toArray
w : c.size + (c' ++ { toArray := b, size_toArray := ⋯ }).size = a.size + b.size
⊢ (∃ a', c = a ++ a' ∧ b = a' ++ (c' ++ { toArray := b, size_toArray := ⋯ }).toArray) ∨
    ∃ c'_1, a = c ++ c'_1 ∧ (c' ++ { toArray := b, size_toArray := ⋯ }).toArray = c'_1 ++ b

Tactic:
right

Result:
case mk.mk.mk.mk.mpr.isFalse.intro.intro.h
α : Type u_1
a b c : Array α
h : ¬a.size ≤ c.size
c' : Vector α (a.size - c.size)
ha : a = ({ toArray := c, size_toArray := ⋯ } ++ c').toArray
w : c.size + (c' ++ { toArray := b, size_toArray := ⋯ }).size = a.size + b.size
⊢ ∃ c'_1, a = c ++ c'_1 ∧ (c' ++ { toArray := b, size_toArray := ⋯ }).toArray = c'_1 ++ b

Proof state:
α : Type u_1
a d a' : Array α
w : (a ++ a').size + d.size = a.size + (a' ++ d).size
⊢ a'.size = a.size + a'.size - a.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
⊢ c'.size = 0

Tactic:
simp at h

Result:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : c.size + c'.size ≤ c.size
⊢ c'.size = 0

Proof state:
case mk.mk.mk.mk.mpr.isFalse.intro.intro.h
α : Type u_1
a b c : Array α
h : ¬a.size ≤ c.size
c' : Vector α (a.size - c.size)
ha : a = ({ toArray := c, size_toArray := ⋯ } ++ c').toArray
w : c.size + (c' ++ { toArray := b, size_toArray := ⋯ }).size = a.size + b.size
⊢ ∃ c'_1, a = c ++ c'_1 ∧ (c' ++ { toArray := b, size_toArray := ⋯ }).toArray = c'_1 ++ b

Tactic:
refine ⟨c'.toArray, ha, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
hc : c' = #[]
⊢ 0 = c.size - (c ++ c').size

Tactic:
simp

Result:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
hc : c' = #[]
⊢ 0 = c.size - (c.size + c'.size)

Proof state:
case mk.mk.mk.mk.mp.inr.intro.intro.isTrue
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
⊢ ∃ a',
    c = ({ toArray := c ++ c', size_toArray := ⋯ } ++ a').toArray ∧
      b = (a' ++ { toArray := c' ++ b, size_toArray := ⋯ }).toArray

Tactic:
have hc : c'.size = 0 := by simp at h; omega

Result:
case mk.mk.mk.mk.mp.inr.intro.intro.isTrue
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
hc : c'.size = 0
⊢ ∃ a',
    c = ({ toArray := c ++ c', size_toArray := ⋯ } ++ a').toArray ∧
      b = (a' ++ { toArray := c' ++ b, size_toArray := ⋯ }).toArray

Proof state:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : ¬(c ++ c').size ≤ c.size
⊢ c'.size = c.size + c'.size - c.size

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.mk.mk.mp.inl.intro.intro
α : Type u_1
a d a' : Array α
w : (a ++ a').size + d.size = a.size + (a' ++ d).size
⊢ ∃ a'_1,
    a ++ a' = ({ toArray := a, size_toArray := ⋯ } ++ a'_1).toArray ∧
      a' ++ d = (a'_1 ++ { toArray := d, size_toArray := ⋯ }).toArray

Tactic:
exact ⟨a'.toVector.cast (by simp; omega), by simp⟩

Result:
no goals

Proof state:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : ¬(c ++ c').size ≤ c.size
⊢ c'.size = (c ++ c').size - c.size

Tactic:
simp

Result:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : ¬(c ++ c').size ≤ c.size
⊢ c'.size = c.size + c'.size - c.size

Proof state:
case mk.mk.mk.mk.mp.inr.intro.intro.isTrue
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
hc : c'.size = 0
⊢ ∃ a',
    c = ({ toArray := c ++ c', size_toArray := ⋯ } ++ a').toArray ∧
      b = (a' ++ { toArray := c' ++ b, size_toArray := ⋯ }).toArray

Tactic:
simp at hc

Result:
case mk.mk.mk.mk.mp.inr.intro.intro.isTrue
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
hc : c' = #[]
⊢ ∃ a',
    c = ({ toArray := c ++ c', size_toArray := ⋯ } ++ a').toArray ∧
      b = (a' ++ { toArray := c' ++ b, size_toArray := ⋯ }).toArray

Proof state:
α : Type u_1
n m k l : Nat
a : Vector α n
b : Vector α m
c : Vector α k
d : Vector α l
w : k + l = n + m
⊢ a ++ b = Vector.cast w (c ++ d) ↔
    if h : n ≤ k then ∃ a', c = Vector.cast ⋯ (a ++ a') ∧ b = Vector.cast ⋯ (a' ++ d)
    else ∃ c', a = Vector.cast ⋯ (c ++ c') ∧ d = Vector.cast ⋯ (c' ++ b)

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
m k l : Nat
b : Vector α m
c : Vector α k
d : Vector α l
a : Array α
w : k + l = a.size + m
⊢ { toArray := a, size_toArray := ⋯ } ++ b = Vector.cast w (c ++ d) ↔
    if h : a.size ≤ k then
      ∃ a', c = Vector.cast ⋯ ({ toArray := a, size_toArray := ⋯ } ++ a') ∧ b = Vector.cast ⋯ (a' ++ d)
    else ∃ c', { toArray := a, size_toArray := ⋯ } = Vector.cast ⋯ (c ++ c') ∧ d = Vector.cast ⋯ (c' ++ b)

Proof state:
case mk.mk.mk.mk.mpr.isTrue
α : Type u_1
a b c d : Array α
w : c.size + d.size = a.size + b.size
h : a.size ≤ c.size
⊢ (∃ a',
      c = ({ toArray := a, size_toArray := ⋯ } ++ a').toArray ∧
        b = (a' ++ { toArray := d, size_toArray := ⋯ }).toArray) →
    (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Tactic:
rintro ⟨a', hc, rfl⟩

Result:
case mk.mk.mk.mk.mpr.isTrue.intro.intro
α : Type u_1
a c d : Array α
h : a.size ≤ c.size
a' : Vector α (c.size - a.size)
hc : c = ({ toArray := a, size_toArray := ⋯ } ++ a').toArray
w : c.size + d.size = a.size + (a' ++ { toArray := d, size_toArray := ⋯ }).size
⊢ (∃ a'_1, c = a ++ a'_1 ∧ (a' ++ { toArray := d, size_toArray := ⋯ }).toArray = a'_1 ++ d) ∨
    ∃ c', a = c ++ c' ∧ d = c' ++ (a' ++ { toArray := d, size_toArray := ⋯ }).toArray

Proof state:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
hc : c' = #[]
⊢ 0 = c.size - (c.size + c'.size)

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.mk.mk.mpr.isTrue.intro.intro.h
α : Type u_1
a c d : Array α
h : a.size ≤ c.size
a' : Vector α (c.size - a.size)
hc : c = ({ toArray := a, size_toArray := ⋯ } ++ a').toArray
w : c.size + d.size = a.size + (a' ++ { toArray := d, size_toArray := ⋯ }).size
⊢ ∃ a'_1, c = a ++ a'_1 ∧ (a' ++ { toArray := d, size_toArray := ⋯ }).toArray = a'_1 ++ d

Tactic:
refine ⟨a'.toArray, hc, rfl⟩

Result:
no goals

Proof state:
α : Type ?u.236079
n m k l : Nat
a : Vector α n
b : Vector α m
c : Vector α k
d : Vector α l
w : k + l = n + m
h : ¬n ≤ k
c' : Vector α (n - k)
⊢ n - k + m = l

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.mk.mk.mp.inr.intro.intro.isTrue
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : (c ++ c').size ≤ c.size
hc : c' = #[]
⊢ ∃ a',
    c = ({ toArray := c ++ c', size_toArray := ⋯ } ++ a').toArray ∧
      b = (a' ++ { toArray := c' ++ b, size_toArray := ⋯ }).toArray

Tactic:
exact ⟨#v[].cast (by simp; omega), by simp_all⟩

Result:
no goals

Proof state:
α : Type u_1
b c c' : Array α
w : c.size + (c' ++ b).size = (c ++ c').size + b.size
h : ¬(c ++ c').size ≤ c.size
⊢ c ++ c' = ({ toArray := c, size_toArray := ⋯ } ++ Vector.cast ⋯ c'.toVector).toArray ∧
    c' ++ b = (Vector.cast ⋯ c'.toVector ++ { toArray := b, size_toArray := ⋯ }).toArray

Tactic:
simp

Result:
no goals