-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_push_iff {a b c : Array α} {x : α} :
    a ++ b = c.push x ↔ (b = #[] ∧ a = c.push x) ∨ (∃ b', b = b'.push x ∧ c = a ++ b')

Proof state:
case mk.mk.mk.mp.inl.intro.intro
α : Type u_1
x : α
a a' : List α
⊢ a' ++ [x] = [] ∧ a = a ++ a' ++ [x] ∨ ∃ b', { toList := a' ++ [x] } = b'.push x ∧ a ++ a' = a ++ b'.toList

Tactic:
right

Result:
case mk.mk.mk.mp.inl.intro.intro.h
α : Type u_1
x : α
a a' : List α
⊢ ∃ b', { toList := a' ++ [x] } = b'.push x ∧ a ++ a' = a ++ b'.toList

Proof state:
case mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b }.toList = (b'.push x).toList
⊢ a ++ b'.toList = a ++ b'.toList ∧ b = b'.toList ++ [x]

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
a b c : Array α
x : α
⊢ a ++ b = c.push x ↔ b = #[] ∧ a = c.push x ∨ ∃ b', b = b'.push x ∧ c = a ++ b'

Tactic:
rcases a with ⟨a⟩

Result:
case mk
α : Type u_1
b c : Array α
x : α
a : List α
⊢ { toList := a } ++ b = c.push x ↔
    b = #[] ∧ { toList := a } = c.push x ∨ ∃ b', b = b'.push x ∧ c = { toList := a } ++ b'

Proof state:
case mk.mk.mk.mp.inr.intro.intro.inl.intro.h
α : Type u_1
x : α
c : List α
⊢ ∃ b', { toList := [x] } = b'.push x ∧ c = c ++ [] ++ b'.toList

Tactic:
exact ⟨#[], by simp⟩

Result:
no goals

Proof state:
case mk.mk.mk.mp.inr.intro.intro
α : Type u_1
x : α
b c b' : List α
h : b' = [] ∧ b = [x] ∨ b' = [x] ∧ b = []
⊢ b = [] ∧ c ++ b' = c ++ [x] ∨ ∃ b'_1, { toList := b } = b'_1.push x ∧ c = c ++ b' ++ b'_1.toList

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h

Result:
case mk.mk.mk.mp.inr.intro.intro.inl.intro
α : Type u_1
x : α
c : List α
⊢ [x] = [] ∧ c ++ [] = c ++ [x] ∨ ∃ b', { toList := [x] } = b'.push x ∧ c = c ++ [] ++ b'.toList

case mk.mk.mk.mp.inr.intro.intro.inr.intro
α : Type u_1
x : α
c : List α
⊢ [] = [] ∧ c ++ [x] = c ++ [x] ∨ ∃ b', { toList := [] } = b'.push x ∧ c = c ++ [x] ++ b'.toList

Proof state:
case mk.mk.mk.mpr.inr.intro.intro
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b } = b'.push x
⊢ (∃ a', a ++ b'.toList = a ++ a' ∧ b = a' ++ [x]) ∨ ∃ c', a = a ++ b'.toList ++ c' ∧ [x] = c' ++ b

Tactic:
left

Result:
case mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b } = b'.push x
⊢ ∃ a', a ++ b'.toList = a ++ a' ∧ b = a' ++ [x]

Proof state:
case mk.mk.mk.mpr
α : Type u_1
x : α
a b c : List α
⊢ (b = [] ∧ a = c ++ [x] ∨ ∃ b', { toList := b } = b'.push x ∧ c = a ++ b'.toList) →
    (∃ a', c = a ++ a' ∧ b = a' ++ [x]) ∨ ∃ c', a = c ++ c' ∧ [x] = c' ++ b

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨b', h, rfl⟩)

Result:
case mk.mk.mk.mpr.inl.intro
α : Type u_1
x : α
c : List α
⊢ (∃ a', c = c ++ [x] ++ a' ∧ [] = a' ++ [x]) ∨ ∃ c', c ++ [x] = c ++ c' ∧ [x] = c' ++ []

case mk.mk.mk.mpr.inr.intro.intro
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b } = b'.push x
⊢ (∃ a', a ++ b'.toList = a ++ a' ∧ b = a' ++ [x]) ∨ ∃ c', a = a ++ b'.toList ++ c' ∧ [x] = c' ++ b

Proof state:
case mk.mk.mk.mp.inl.intro.intro.h
α : Type u_1
x : α
a a' : List α
⊢ ∃ b', { toList := a' ++ [x] } = b'.push x ∧ a ++ a' = a ++ b'.toList

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

Result:
no goals

Proof state:
case mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b } = b'.push x
⊢ ∃ a', a ++ b'.toList = a ++ a' ∧ b = a' ++ [x]

Tactic:
refine ⟨b'.toList, ?_⟩

Result:
case mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b } = b'.push x
⊢ a ++ b'.toList = a ++ b'.toList ∧ b = b'.toList ++ [x]

Proof state:
case mk.mk.mk.mp.inr.intro.intro.inl.intro
α : Type u_1
x : α
c : List α
⊢ [x] = [] ∧ c ++ [] = c ++ [x] ∨ ∃ b', { toList := [x] } = b'.push x ∧ c = c ++ [] ++ b'.toList

Tactic:
right

Result:
case mk.mk.mk.mp.inr.intro.intro.inl.intro.h
α : Type u_1
x : α
c : List α
⊢ ∃ b', { toList := [x] } = b'.push x ∧ c = c ++ [] ++ b'.toList

Proof state:
case mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b } = b'.push x
⊢ a ++ b'.toList = a ++ b'.toList ∧ b = b'.toList ++ [x]

Tactic:
replace h := congrArg Array.toList h

Result:
case mk.mk.mk.mpr.inr.intro.intro.h
α : Type u_1
x : α
a b : List α
b' : Array α
h : { toList := b }.toList = (b'.push x).toList
⊢ a ++ b'.toList = a ++ b'.toList ∧ b = b'.toList ++ [x]

Proof state:
case mk.mk.mk.mp.inr.intro.intro
α : Type u_1
x : α
b c b' : List α
h : [x] = b' ++ b
⊢ b = [] ∧ c ++ b' = c ++ [x] ∨ ∃ b'_1, { toList := b } = b'_1.push x ∧ c = c ++ b' ++ b'_1.toList

Tactic:
rw [List.singleton_eq_append_iff] at h

Result:
case mk.mk.mk.mp.inr.intro.intro
α : Type u_1
x : α
b c b' : List α
h : b' = [] ∧ b = [x] ∨ b' = [x] ∧ b = []
⊢ b = [] ∧ c ++ b' = c ++ [x] ∨ ∃ b'_1, { toList := b } = b'_1.push x ∧ c = c ++ b' ++ b'_1.toList

Proof state:
case mk.mk
α : Type u_1
c : Array α
x : α
a b : List α
⊢ { toList := a } ++ { toList := b } = c.push x ↔
    { toList := b } = #[] ∧ { toList := a } = c.push x ∨ ∃ b', { toList := b } = b'.push x ∧ c = { toList := a } ++ b'

Tactic:
rcases c with ⟨c⟩

Result:
case mk.mk.mk
α : Type u_1
x : α
a b c : List α
⊢ { toList := a } ++ { toList := b } = { toList := c }.push x ↔
    { toList := b } = #[] ∧ { toList := a } = { toList := c }.push x ∨
      ∃ b', { toList := b } = b'.push x ∧ { toList := c } = { toList := a } ++ b'

Proof state:
α : Type u_1
x : α
a a' : List α
⊢ { toList := a' ++ [x] } = { toList := a' }.push x ∧ a ++ a' = a ++ { toList := a' }.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x : α
c : List α
⊢ { toList := [x] } = #[].push x ∧ c = c ++ [] ++ #[].toList

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mp.inr.intro.intro.inr.intro.h
α : Type u_1
x : α
c : List α
⊢ [] = [] ∧ c ++ [x] = c ++ [x]

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mpr.inl.intro
α : Type u_1
x : α
c : List α
⊢ (∃ a', c = c ++ [x] ++ a' ∧ [] = a' ++ [x]) ∨ ∃ c', c ++ [x] = c ++ c' ∧ [x] = c' ++ []

Tactic:
right

Result:
case mk.mk.mk.mpr.inl.intro.h
α : Type u_1
x : α
c : List α
⊢ ∃ c', c ++ [x] = c ++ c' ∧ [x] = c' ++ []

Proof state:
case mk.mk.mk
α : Type u_1
x : α
a b c : List α
⊢ { toList := a } ++ { toList := b } = { toList := c }.push x ↔
    { toList := b } = #[] ∧ { toList := a } = { toList := c }.push x ∨
      ∃ b', { toList := b } = b'.push x ∧ { toList := c } = { toList := a } ++ b'

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

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

Proof state:
case mk.mk.mk.mp.inr.intro.intro.inr.intro
α : Type u_1
x : α
c : List α
⊢ [] = [] ∧ c ++ [x] = c ++ [x] ∨ ∃ b', { toList := [] } = b'.push x ∧ c = c ++ [x] ++ b'.toList

Tactic:
left

Result:
case mk.mk.mk.mp.inr.intro.intro.inr.intro.h
α : Type u_1
x : α
c : List α
⊢ [] = [] ∧ c ++ [x] = c ++ [x]

Proof state:
case mk.mk.mk.mpr.inl.intro.h
α : Type u_1
x : α
c : List α
⊢ ∃ c', c ++ [x] = c ++ c' ∧ [x] = c' ++ []

Tactic:
exact ⟨[x], by simp⟩

Result:
no goals

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

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
x : α
a b c : List α
⊢ ((∃ a', c = a ++ a' ∧ b = a' ++ [x]) ∨ ∃ c', a = c ++ c' ∧ [x] = c' ++ b) →
    b = [] ∧ a = c ++ [x] ∨ ∃ b', { toList := b } = b'.push x ∧ c = a ++ b'.toList

case mk.mk.mk.mpr
α : Type u_1
x : α
a b c : List α
⊢ (b = [] ∧ a = c ++ [x] ∨ ∃ b', { toList := b } = b'.push x ∧ c = a ++ b'.toList) →
    (∃ a', c = a ++ a' ∧ b = a' ++ [x]) ∨ ∃ c', a = c ++ c' ∧ [x] = c' ++ b