-- 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.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

Tactic:
split <;> rename_i h

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
⊢ ∃ a',
    c = ({ toArray := c ++ c', size_toArray := ⋯ } ++ a').toArray ∧
      b = (a' ++ { toArray := c' ++ b, size_toArray := ⋯ }).toArray

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

Proof state:
case mk.mk.mk.mk.mpr
α : Type u_1
a b c d : Array α
w : c.size + d.size = a.size + b.size
⊢ (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) →
    (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Tactic:
split <;> rename_i h

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

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

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
⊢ 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

Tactic:
rw [dif_pos (by simp)]

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
⊢ ∃ a'_1,
    a ++ a' = ({ toArray := a, size_toArray := ⋯ } ++ a'_1).toArray ∧
      a' ++ d = (a'_1 ++ { toArray := d, size_toArray := ⋯ }).toArray

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

Tactic:
omega

Result:
no goals

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

Tactic:
rintro ⟨c', ha, rfl⟩

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

Proof state:
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)

Tactic:
rcases b with ⟨b, rfl⟩

Result:
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 := ⋯ })

Proof state:
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

Tactic:
constructor

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

case mk.mk.mk.mk.mpr
α : Type u_1
a b c d : Array α
w : c.size + d.size = a.size + b.size
⊢ (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) →
    (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Proof state:
α : 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

Tactic:
omega

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
a' : Vector α (k - n)
⊢ k - n + l = m

Tactic:
omega

Result:
no goals