-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_append_iff {a b c d : Array α} :
    a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Proof state:
case mk.mk.mk.mk.mpr.inr.intro.intro
α : Type u_1
b c : List α
c' : Array α
⊢ (∃ a', c = c ++ c'.toList ++ a' ∧ b = a' ++ (c'.toList ++ b)) ∨
    ∃ c'_1, c ++ c'.toList = c ++ c'_1 ∧ c'.toList ++ b = c'_1 ++ b

Tactic:
right

Result:
case mk.mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
b c : List α
c' : Array α
⊢ ∃ c'_1, c ++ c'.toList = c ++ c'_1 ∧ c'.toList ++ b = c'_1 ++ b

Proof state:
case mk.mk
α : Type u_1
c d : Array α
a b : List α
⊢ { toList := a } ++ { toList := b } = c ++ d ↔
    (∃ a', c = { toList := a } ++ a' ∧ { toList := b } = a' ++ d) ∨
      ∃ c', { toList := a } = c ++ c' ∧ d = c' ++ { toList := b }

Tactic:
rcases c with ⟨c⟩

Result:
case mk.mk.mk
α : Type u_1
d : Array α
a b c : List α
⊢ { toList := a } ++ { toList := b } = { toList := c } ++ d ↔
    (∃ a', { toList := c } = { toList := a } ++ a' ∧ { toList := b } = a' ++ d) ∨
      ∃ c', { toList := a } = { toList := c } ++ c' ∧ d = c' ++ { toList := b }

Proof state:
case mk.mk.mk.mk.mp.inr.intro.intro
α : Type u_1
b c c' : List α
⊢ (∃ a', c = c ++ c' ++ a'.toList ∧ b = a'.toList ++ (c' ++ b)) ∨
    ∃ c'_1, c ++ c' = c ++ c'_1.toList ∧ c' ++ b = c'_1.toList ++ b

Tactic:
right

Result:
case mk.mk.mk.mk.mp.inr.intro.intro.h
α : Type u_1
b c c' : List α
⊢ ∃ c'_1, c ++ c' = c ++ c'_1.toList ∧ c' ++ b = c'_1.toList ++ b

Proof state:
case mk.mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
b c : List α
c' : Array α
⊢ ∃ c'_1, c ++ c'.toList = c ++ c'_1 ∧ c'.toList ++ b = c'_1 ++ b

Tactic:
exact ⟨c'.toList, by simp⟩

Result:
no goals

Proof state:
case mk.mk.mk.mk.mpr.inl.intro.intro.h
α : Type u_1
a d : List α
a' : Array α
⊢ ∃ a'_1, a ++ a'.toList = a ++ a'_1 ∧ a'.toList ++ d = a'_1 ++ d

Tactic:
exact ⟨a'.toList, by simp⟩

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
a b c d : List α
⊢ { toList := a } ++ { toList := b } = { toList := c } ++ { toList := d } ↔
    (∃ a', { toList := c } = { toList := a } ++ a' ∧ { toList := b } = a' ++ { toList := d }) ∨
      ∃ c', { toList := a } = { toList := c } ++ c' ∧ { toList := d } = c' ++ { toList := b }

Tactic:
simp only [List.append_toArray, mk.injEq, List.append_eq_append_iff, toArray_eq_append_iff]

Result:
case mk.mk.mk.mk
α : Type u_1
a b c d : List α
⊢ ((∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b) ↔
    (∃ a', c = a ++ a'.toList ∧ b = a'.toList ++ d) ∨ ∃ c', a = c ++ c'.toList ∧ d = c'.toList ++ b

Proof state:
case mk.mk.mk.mk.mpr
α : Type u_1
a b c d : List α
⊢ ((∃ a', c = a ++ a'.toList ∧ b = a'.toList ++ d) ∨ ∃ c', a = c ++ c'.toList ∧ d = c'.toList ++ b) →
    (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

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

Result:
case mk.mk.mk.mk.mpr.inl.intro.intro
α : Type u_1
a d : List α
a' : Array α
⊢ (∃ a'_1, a ++ a'.toList = a ++ a'_1 ∧ a'.toList ++ d = a'_1 ++ d) ∨
    ∃ c', a = a ++ a'.toList ++ c' ∧ d = c' ++ (a'.toList ++ d)

case mk.mk.mk.mk.mpr.inr.intro.intro
α : Type u_1
b c : List α
c' : Array α
⊢ (∃ a', c = c ++ c'.toList ++ a' ∧ b = a' ++ (c'.toList ++ b)) ∨
    ∃ c'_1, c ++ c'.toList = c ++ c'_1 ∧ c'.toList ++ b = c'_1 ++ b

Proof state:
case mk.mk.mk.mk.mp.inl.intro.intro.h
α : Type u_1
a d a' : List α
⊢ ∃ a'_1, a ++ a' = a ++ a'_1.toList ∧ a' ++ d = a'_1.toList ++ d

Tactic:
exact ⟨⟨a'⟩, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
a b c d : Array α
⊢ a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Tactic:
rcases a with ⟨a⟩

Result:
case mk
α : Type u_1
b c d : Array α
a : List α
⊢ { toList := a } ++ b = c ++ d ↔
    (∃ a', c = { toList := a } ++ a' ∧ b = a' ++ d) ∨ ∃ c', { toList := a } = c ++ c' ∧ d = c' ++ b

Proof state:
α : Type u_1
a d a' : List α
⊢ a ++ a' = a ++ { toList := a' }.toList ∧ a' ++ d = { toList := a' }.toList ++ d

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
a b c d : List α
⊢ ((∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b) ↔
    (∃ a', c = a ++ a'.toList ∧ b = a'.toList ++ d) ∨ ∃ c', a = c ++ c'.toList ∧ d = c'.toList ++ b

Tactic:
constructor

Result:
case mk.mk.mk.mk.mp
α : Type u_1
a b c d : List α
⊢ ((∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b) →
    (∃ a', c = a ++ a'.toList ∧ b = a'.toList ++ d) ∨ ∃ c', a = c ++ c'.toList ∧ d = c'.toList ++ b

case mk.mk.mk.mk.mpr
α : Type u_1
a b c d : List α
⊢ ((∃ a', c = a ++ a'.toList ∧ b = a'.toList ++ d) ∨ ∃ c', a = c ++ c'.toList ∧ d = c'.toList ++ b) →
    (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Proof state:
α : Type u_1
b c : List α
c' : Array α
⊢ c ++ c'.toList = c ++ c'.toList ∧ c'.toList ++ b = c'.toList ++ b

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
b c d : Array α
a : List α
⊢ { toList := a } ++ b = c ++ d ↔
    (∃ a', c = { toList := a } ++ a' ∧ b = a' ++ d) ∨ ∃ c', { toList := a } = c ++ c' ∧ d = c' ++ b

Tactic:
rcases b with ⟨b⟩

Result:
case mk.mk
α : Type u_1
c d : Array α
a b : List α
⊢ { toList := a } ++ { toList := b } = c ++ d ↔
    (∃ a', c = { toList := a } ++ a' ∧ { toList := b } = a' ++ d) ∨
      ∃ c', { toList := a } = c ++ c' ∧ d = c' ++ { toList := b }

Proof state:
α : Type u_1
b c c' : List α
⊢ c ++ c' = c ++ { toList := c' }.toList ∧ c' ++ b = { toList := c' }.toList ++ b

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mk.mp
α : Type u_1
a b c d : List α
⊢ ((∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b) →
    (∃ a', c = a ++ a'.toList ∧ b = a'.toList ++ d) ∨ ∃ c', a = c ++ c'.toList ∧ d = c'.toList ++ b

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

Result:
case mk.mk.mk.mk.mp.inl.intro.intro
α : Type u_1
a d a' : List α
⊢ (∃ a'_1, a ++ a' = a ++ a'_1.toList ∧ a' ++ d = a'_1.toList ++ d) ∨
    ∃ c', a = a ++ a' ++ c'.toList ∧ d = c'.toList ++ (a' ++ d)

case mk.mk.mk.mk.mp.inr.intro.intro
α : Type u_1
b c c' : List α
⊢ (∃ a', c = c ++ c' ++ a'.toList ∧ b = a'.toList ++ (c' ++ b)) ∨
    ∃ c'_1, c ++ c' = c ++ c'_1.toList ∧ c' ++ b = c'_1.toList ++ b

Proof state:
case mk.mk.mk.mk.mpr.inl.intro.intro
α : Type u_1
a d : List α
a' : Array α
⊢ (∃ a'_1, a ++ a'.toList = a ++ a'_1 ∧ a'.toList ++ d = a'_1 ++ d) ∨
    ∃ c', a = a ++ a'.toList ++ c' ∧ d = c' ++ (a'.toList ++ d)

Tactic:
left

Result:
case mk.mk.mk.mk.mpr.inl.intro.intro.h
α : Type u_1
a d : List α
a' : Array α
⊢ ∃ a'_1, a ++ a'.toList = a ++ a'_1 ∧ a'.toList ++ d = a'_1 ++ d

Proof state:
case mk.mk.mk.mk.mp.inl.intro.intro
α : Type u_1
a d a' : List α
⊢ (∃ a'_1, a ++ a' = a ++ a'_1.toList ∧ a' ++ d = a'_1.toList ++ d) ∨
    ∃ c', a = a ++ a' ++ c'.toList ∧ d = c'.toList ++ (a' ++ d)

Tactic:
left

Result:
case mk.mk.mk.mk.mp.inl.intro.intro.h
α : Type u_1
a d a' : List α
⊢ ∃ a'_1, a ++ a' = a ++ a'_1.toList ∧ a' ++ d = a'_1.toList ++ d

Proof state:
case mk.mk.mk
α : Type u_1
d : Array α
a b c : List α
⊢ { toList := a } ++ { toList := b } = { toList := c } ++ d ↔
    (∃ a', { toList := c } = { toList := a } ++ a' ∧ { toList := b } = a' ++ d) ∨
      ∃ c', { toList := a } = { toList := c } ++ c' ∧ d = c' ++ { toList := b }

Tactic:
rcases d with ⟨d⟩

Result:
case mk.mk.mk.mk
α : Type u_1
a b c d : List α
⊢ { toList := a } ++ { toList := b } = { toList := c } ++ { toList := d } ↔
    (∃ a', { toList := c } = { toList := a } ++ a' ∧ { toList := b } = a' ++ { toList := d }) ∨
      ∃ c', { toList := a } = { toList := c } ++ c' ∧ { toList := d } = c' ++ { toList := b }

Proof state:
case mk.mk.mk.mk.mp.inr.intro.intro.h
α : Type u_1
b c c' : List α
⊢ ∃ c'_1, c ++ c' = c ++ c'_1.toList ∧ c' ++ b = c'_1.toList ++ b

Tactic:
exact ⟨⟨c'⟩, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
a d : List α
a' : Array α
⊢ a ++ a'.toList = a ++ a'.toList ∧ a'.toList ++ d = a'.toList ++ d

Tactic:
simp

Result:
no goals