English
If l1 extends l and l2 extends l, and |l1| ≤ |l2|, then l1 extends l2 (symmetric formulation).
Русский
Если l1 расширяет l и l2 расширяет l, и |l1| ≤ |l2|, то l1 расширяет l2.
LaTeX
$$$\\mathrm{BlankExtends}(l_1,l) \\land \\mathrm{BlankExtends}(l_2,l) \\land |l_1| \\le |l_2| \\Rightarrow \\mathrm{BlankExtends}(l_1,l_2).$$$
Lean4
theorem above_of_le {Γ} [Inhabited Γ] {l l₁ l₂ : List Γ} :
BlankExtends l₁ l → BlankExtends l₂ l → l₁.length ≤ l₂.length → BlankExtends l₁ l₂ :=
by
rintro ⟨i, rfl⟩ ⟨j, e⟩ h; use i - j
refine List.append_cancel_right (e.symm.trans ?_)
rw [List.append_assoc, ← List.replicate_add, Nat.sub_add_cancel]
apply_fun List.length at e
simp only [List.length_append, List.length_replicate] at e
rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]
