-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_eq_append_iff {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m} :
    xs.reverse = ys ++ zs ↔ xs = (zs.reverse ++ ys.reverse).cast (by omega)

Proof state:
α : Type u_1
n m : Nat
xs : Vector α (n + m)
ys : Vector α n
zs : Vector α m
⊢ xs.reverse = ys ++ zs ↔ xs = Vector.cast ⋯ (zs.reverse ++ ys.reverse)

Tactic:
cases xs

Result:
case mk
α : Type u_1
n m : Nat
ys : Vector α n
zs : Vector α m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n + m
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse = ys ++ zs ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = Vector.cast ⋯ (zs.reverse ++ ys.reverse)

Proof state:
case mk.mk
α : Type u_1
n m : Nat
zs : Vector α m
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n + m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.reverse =
      { toArray := toArray✝, size_toArray := size_toArray✝ } ++ zs ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } =
      Vector.cast ⋯ (zs.reverse ++ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse)

Tactic:
cases zs

Result:
case mk.mk.mk
α : Type u_1
n m : Nat
toArray✝² : Array α
size_toArray✝² : toArray✝².size = n + m
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ { toArray := toArray✝², size_toArray := size_toArray✝² }.reverse =
      { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    { toArray := toArray✝², size_toArray := size_toArray✝² } =
      Vector.cast ⋯
        ({ toArray := toArray✝, size_toArray := size_toArray✝ }.reverse ++
          { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.reverse)

Proof state:
case mk.mk.mk
α : Type u_1
n m : Nat
toArray✝² : Array α
size_toArray✝² : toArray✝².size = n + m
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ { toArray := toArray✝², size_toArray := size_toArray✝² }.reverse =
      { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    { toArray := toArray✝², size_toArray := size_toArray✝² } =
      Vector.cast ⋯
        ({ toArray := toArray✝, size_toArray := size_toArray✝ }.reverse ++
          { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.reverse)

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
n m : Nat
ys : Vector α n
zs : Vector α m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n + m
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse = ys ++ zs ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = Vector.cast ⋯ (zs.reverse ++ ys.reverse)

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
n m : Nat
zs : Vector α m
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n + m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.reverse =
      { toArray := toArray✝, size_toArray := size_toArray✝ } ++ zs ↔
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } =
      Vector.cast ⋯ (zs.reverse ++ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse)

Proof state:
α : Type ?u.366302
n m : Nat
xs : Vector α (n + m)
ys : Vector α n
zs : Vector α m
⊢ m + n = n + m

Tactic:
omega

Result:
no goals