-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_inj {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m} (h : s₁ ++ t₁ = s₂ ++ t₂) :
    s₁ = s₂ ∧ t₁ = t₂

Proof state:
α : Type u_1
n m : Nat
s₁ s₂ : Vector α n
t₁ t₂ : Vector α m
h : s₁ ++ t₁ = s₂ ++ t₂
⊢ s₁ = s₂ ∧ t₁ = t₂

Tactic:
rcases s₁ with ⟨s₁, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
t₁ t₂ : Vector α m
s₁ : Array α
s₂ : Vector α s₁.size
h : { toArray := s₁, size_toArray := ⋯ } ++ t₁ = s₂ ++ t₂
⊢ { toArray := s₁, size_toArray := ⋯ } = s₂ ∧ t₁ = t₂

Proof state:
α : Type u_1
s₁ s₂ : Array α
hs : s₂.size = s₁.size
t₁ t₂ : Array α
ht : t₂.size = t₁.size
h :
  { toArray := s₁, size_toArray := ⋯ } ++ { toArray := t₁, size_toArray := ⋯ } =
    { toArray := s₂, size_toArray := hs } ++ { toArray := t₂, size_toArray := ht }
⊢ s₁.size = s₂.size

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
s₁ s₂ : Array α
hs : s₂.size = s₁.size
t₁ t₂ : Array α
ht : t₂.size = t₁.size
h :
  { toArray := s₁, size_toArray := ⋯ } ++ { toArray := t₁, size_toArray := ⋯ } =
    { toArray := s₂, size_toArray := hs } ++ { toArray := t₂, size_toArray := ht }
⊢ { toArray := s₁, size_toArray := ⋯ } = { toArray := s₂, size_toArray := hs } ∧
    { toArray := t₁, size_toArray := ⋯ } = { toArray := t₂, size_toArray := ht }

Tactic:
simpa using Array.append_inj (by simpa using h) (by omega)

Result:
no goals

Proof state:
α : Type u_1
s₁ s₂ : Array α
hs : s₂.size = s₁.size
t₁ t₂ : Array α
ht : t₂.size = t₁.size
h :
  { toArray := s₁, size_toArray := ⋯ } ++ { toArray := t₁, size_toArray := ⋯ } =
    { toArray := s₂, size_toArray := hs } ++ { toArray := t₂, size_toArray := ht }
⊢ s₁ ++ t₁ = s₂ ++ t₂

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
m : Nat
t₁ t₂ : Vector α m
s₁ : Array α
s₂ : Vector α s₁.size
h : { toArray := s₁, size_toArray := ⋯ } ++ t₁ = s₂ ++ t₂
⊢ { toArray := s₁, size_toArray := ⋯ } = s₂ ∧ t₁ = t₂

Tactic:
rcases s₂ with ⟨s₂, hs⟩

Result:
case mk.mk
α : Type u_1
m : Nat
t₁ t₂ : Vector α m
s₁ s₂ : Array α
hs : s₂.size = s₁.size
h : { toArray := s₁, size_toArray := ⋯ } ++ t₁ = { toArray := s₂, size_toArray := hs } ++ t₂
⊢ { toArray := s₁, size_toArray := ⋯ } = { toArray := s₂, size_toArray := hs } ∧ t₁ = t₂

Proof state:
case mk.mk
α : Type u_1
m : Nat
t₁ t₂ : Vector α m
s₁ s₂ : Array α
hs : s₂.size = s₁.size
h : { toArray := s₁, size_toArray := ⋯ } ++ t₁ = { toArray := s₂, size_toArray := hs } ++ t₂
⊢ { toArray := s₁, size_toArray := ⋯ } = { toArray := s₂, size_toArray := hs } ∧ t₁ = t₂

Tactic:
rcases t₁ with ⟨t₁, rfl⟩

Result:
case mk.mk.mk
α : Type u_1
s₁ s₂ : Array α
hs : s₂.size = s₁.size
t₁ : Array α
t₂ : Vector α t₁.size
h :
  { toArray := s₁, size_toArray := ⋯ } ++ { toArray := t₁, size_toArray := ⋯ } =
    { toArray := s₂, size_toArray := hs } ++ t₂
⊢ { toArray := s₁, size_toArray := ⋯ } = { toArray := s₂, size_toArray := hs } ∧
    { toArray := t₁, size_toArray := ⋯ } = t₂

Proof state:
case mk.mk.mk
α : Type u_1
s₁ s₂ : Array α
hs : s₂.size = s₁.size
t₁ : Array α
t₂ : Vector α t₁.size
h :
  { toArray := s₁, size_toArray := ⋯ } ++ { toArray := t₁, size_toArray := ⋯ } =
    { toArray := s₂, size_toArray := hs } ++ t₂
⊢ { toArray := s₁, size_toArray := ⋯ } = { toArray := s₂, size_toArray := hs } ∧
    { toArray := t₁, size_toArray := ⋯ } = t₂

Tactic:
rcases t₂ with ⟨t₂, ht⟩

Result:
case mk.mk.mk.mk
α : Type u_1
s₁ s₂ : Array α
hs : s₂.size = s₁.size
t₁ t₂ : Array α
ht : t₂.size = t₁.size
h :
  { toArray := s₁, size_toArray := ⋯ } ++ { toArray := t₁, size_toArray := ⋯ } =
    { toArray := s₂, size_toArray := hs } ++ { toArray := t₂, size_toArray := ht }
⊢ { toArray := s₁, size_toArray := ⋯ } = { toArray := s₂, size_toArray := hs } ∧
    { toArray := t₁, size_toArray := ⋯ } = { toArray := t₂, size_toArray := ht }