List.Chain'.not_map_lt_of_mem or so?

Stream: mathlib4

[Malvin Gattinger]

Roughly: "There is no chain with a strictly decreasing measure that repeats the head."

I did not find this in mathlib. Is it there under a different name? I'd also like to improve my naming/searching skills. Would this be flipped around with x not in rest as conclusion? Or should it be more general, using Nodup? Or less general, without the f but using docs@List.chain_map_of_chain instead?

import Mathlib.Data.List.Chain
import Mathlib.Tactic.Linarith

theorem List.Chain'.not_map_lt_of_mem {α: Type} (f : α → Nat)
    {x : α} {rest : List α} (h : x ∈ rest)
    : ¬ (List.Chain' (fun p q => f q < f p) (x :: rest)) := by
  induction rest <;> simp_all only [mem_cons, chain'_cons, not_and, not_mem_nil]
  intro fy_lt_fx
  case cons y rest IH =>
    rcases h with h|h
    · subst_eqs; simp_all
    · specialize IH h
      rw [List.chain'_cons']
      cases rest <;> simp_all
      case cons z rest =>
        cases h
        · subst_eqs
          intro fy_lt_fx
          linarith
        · intro fz_lt_fy
          exact IH (Nat.lt_trans fz_lt_fy fy_lt_fx)

[Edward van de Meent]

going via List.chain'_iff_pairwise feels like it would help?

[Edward van de Meent]

basically, the logic would be "the relation is transitive, therefore any distinct pair is related in that order, therefore x < x, which is not possible as the relation is antireflexive"

[Edward van de Meent]

theorem List.Chain'.not_map_lt_of_mem {α: Type} (f : α → Nat)
    {x : α} {rest : List α} (h : x ∈ rest)
    : ¬ (List.Chain' (fun p q => f q < f p) (x :: rest)) := by
  intro hr
  rw [← List.chain'_map (R := (. > .)), List.chain'_iff_pairwise, pairwise_map, pairwise_cons] at hr
  exact (hr.left x h).ne rfl

[Edward van de Meent]

to me, the main gist of the theorem here is the following lemma:

lemma List.chain'_lemma_we_care_about {α: Type}
    {x : α} {rest : List α} {r : α → α → Prop} [IsTrans α r] (h:(List.Chain' r (x :: rest)))
    : ∀ y ∈ rest, r x y := by
  rw [List.chain'_iff_pairwise,pairwise_cons] at h
  exact h.left

[Edward van de Meent]

basically, the original theorem is (imo) too specific to be in mathlib, as the theorem mentions a specific relation depending on a keying function, and additionally is formulated in a negative way .