-- 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:
α : 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)
⊢ k + (n - k) = n

Tactic:
omega

Result:
no goals

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

Tactic:
simp

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

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' = #[]
⊢ c = ({ toArray := c ++ c', size_toArray := ⋯ } ++ Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }).toArray ∧
    b = (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ } ++ { toArray := c' ++ b, size_toArray := ⋯ }).toArray

Tactic:
simp_all

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
rcases c with ⟨c, rfl⟩

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

Proof state:
α : Type u_1
a d a' : Array α
w : (a ++ a').size + d.size = a.size + (a' ++ d).size
⊢ a ++ a' = ({ toArray := a, size_toArray := ⋯ } ++ Vector.cast ⋯ a'.toVector).toArray ∧
    a' ++ d = (Vector.cast ⋯ a'.toVector ++ { toArray := d, size_toArray := ⋯ }).toArray

Tactic:
simp

Result:
no goals

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

Tactic:
rcases d with ⟨d, rfl⟩

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

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

Tactic:
simp only [mk_append_mk, Array.append_eq_append_iff, mk_eq, toArray_cast]

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

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

Tactic:
rintro (⟨a', rfl, rfl⟩ | ⟨c', rfl, rfl⟩)

Result:
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
⊢ if h : a.size ≤ (a ++ a').size then
    ∃ a'_1,
      a ++ a' = ({ toArray := a, size_toArray := ⋯ } ++ a'_1).toArray ∧
        a' ++ d = (a'_1 ++ { toArray := d, size_toArray := ⋯ }).toArray
  else
    ∃ c',
      a = ({ toArray := a ++ a', size_toArray := ⋯ } ++ c').toArray ∧
        d = (c' ++ { toArray := a' ++ d, size_toArray := ⋯ }).toArray

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

Proof state:
case mk.mk.mk.mk.mp.inr.intro.intro.isFalse
α : 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'_1,
    c ++ c' = ({ toArray := c, size_toArray := ⋯ } ++ c'_1).toArray ∧
      c' ++ b = (c'_1 ++ { toArray := b, size_toArray := ⋯ }).toArray

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

Result:
no goals