English
Let x1,x2,z1,z2 be lists, a1,a2 elements. If a2 does not occur in x1 nor in z1, then x1 ++ [a1] ++ z1 = x2 ++ [a2] ++ z2 if and only if x1 = x2 and a1 = a2 and z1 = z2.
Русский
Пусть l1 = x1 ++ [a1] ++ z1 и l2 = x2 ++ [a2] ++ z2, и a2 не встречается в x1 и в z1. Тогда l1 = l2 тогда и только если x1 = x2, a1 = a2 и z1 = z2.
LaTeX
$$$$x_1 ++ [a_1] ++ z_1 = x_2 ++ [a_2] ++ z_2 \quad\text{iff}\quad x_1 = x_2 \wedge a_1 = a_2 \wedge z_1 = z_2,$$ при условии $a_2 \notin x_1$ и $a_2 \notin z_1$.$$
Lean4
/-- Consider two lists `l₁` and `l₂` with designated elements `a₁` and `a₂` somewhere in them:
`l₁ = x₁ ++ [a₁] ++ z₁` and `l₂ = x₂ ++ [a₂] ++ z₂`.
Assume the designated element `a₂` is present in neither `x₁` nor `z₁`.
We conclude that the lists are equal (`l₁ = l₂`) if and only if their respective parts are equal
(`x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂`). -/
theorem append_cons_inj_of_notMem {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α} (notin_x : a₂ ∉ x₁) (notin_z : a₂ ∉ z₁) :
x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ :=
by
constructor
· simp only [append_eq_append_iff, cons_eq_append_iff, cons_eq_cons]
rintro (⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩ | ⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩) <;> simp_all
· rintro ⟨rfl, rfl, rfl⟩
rfl
