Theorem: List.append_eq_append_of_length_le (Lean4Lean/Std/Basic.lean)

State before:
α : Type u_1
a b c d : List α
h : length a ≤ length c
⊢ a ++ b = c ++ d ↔ ∃ a', c = a ++ a' ∧ b = a' ++ d
Tactic:
rw [append_eq_append_iff, or_iff_left_iff_imp]
State after:
α : Type u_1
a b c d : List α
h : length a ≤ length c
⊢ (∃ c', a = c ++ c' ∧ d = c' ++ b) → ∃ a', c = a ++ a' ∧ b = a' ++ d

State before:
α : Type u_1
a b c d : List α
h : length a ≤ length c
⊢ (∃ c', a = c ++ c' ∧ d = c' ++ b) → ∃ a', c = a ++ a' ∧ b = a' ++ d
Tactic:
rintro ⟨c', rfl, rfl⟩
State after:
case intro.intro
α : Type u_1
b c c' : List α
h : length (c ++ c') ≤ length c
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)

State before:
case intro.intro
α : Type u_1
b c c' : List α
h : length (c ++ c') ≤ length c
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)
Tactic:
rw [← Nat.add_zero c.length, length_append,
  Nat.add_le_add_iff_left, Nat.le_zero, length_eq_zero] at h
State after:
case intro.intro
α : Type u_1
b c c' : List α
h : c' = []
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)

State before:
case intro.intro
α : Type u_1
b c c' : List α
h : c' = []
⊢ ∃ a', c = c ++ c' ++ a' ∧ b = a' ++ (c' ++ b)
Tactic:
subst h
State after:
case intro.intro
α : Type u_1
b c : List α
⊢ ∃ a', c = c ++ [] ++ a' ∧ b = a' ++ ([] ++ b)

State before:
case intro.intro
α : Type u_1
b c : List α
⊢ ∃ a', c = c ++ [] ++ a' ∧ b = a' ++ ([] ++ b)
Tactic:
exact ⟨[], by simp⟩
State after:
no goals

State before:
α : Type u_1
b c : List α
⊢ c = c ++ [] ++ [] ∧ b = [] ++ ([] ++ b)
Tactic:
simp
State after:
no goals