English
If r is irreflexive and transitive, then whenever a ∈ l and m ∈ foldl(argAux r) o l, we have not r a m.
Русский
Если r иррефлексивно и транзитивно, тогда при a ∈ l и m ∈ foldl(argAux r) o l верно, что не r a m.
LaTeX
$$$ \text{Irreflexive}(r) \land \text{Transitive}(r) \Rightarrow \forall a,m,\; a \in l \to m \in \operatorname{foldl}(\operatorname{argAux}(r), o, l) \to \neg r\ a\ m$$$
Lean4
theorem not_of_mem_foldl_argAux (hr₀ : Irreflexive r) (hr₁ : Transitive r) :
∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m :=
by
induction l using List.reverseRecOn with
| nil => simp
| append_singleton tl a ih => ?_
intro b m o hb ho
rw [foldl_append, foldl_cons, foldl_nil, argAux] at ho
rcases hf : foldl (argAux r) o tl with - | c
· rw [hf] at ho
rw [foldl_argAux_eq_none] at hf
simp_all [hf.1, hf.2, hr₀ _]
rw [hf, Option.mem_def] at ho
dsimp only at ho
split_ifs at ho with hac <;> rcases mem_append.1 hb with h | h <;> injection ho with ho <;> subst ho
· exact fun hba => ih h hf (hr₁ hba hac)
· simp_all [hr₀ _]
· exact ih h hf
· simp_all
