MaximalFor P (g ∘ f) i → MaximalFor P f i

Stream: Is there code for X?

[Snir Broshi]

What's the weakest property on g that implies this?
I'm fine with requiring more of the types, such as [PartialOrder α] [LinearOrder β].
Is there a better version for the special case f = id (aka MaximalFor P g i → Maximal P i)?

import Mathlib

theorem MaximalFor.of_relEmbedding_comp {ι α β : Type*} [Preorder α] [Preorder β] {P : ι → Prop}
    {f : ι → α} {i : ι} (g : α ↪o β) (h : MaximalFor P (g ∘ f) i) : MaximalFor P f i :=
  -- this only uses `f a ≤ f b ↔ a ≤ b` when `P a` and `P b` and doesn't use injectivity, which is weaker than `OrderEmbedding`
  ⟨h.prop, fun _ hj hle ↦ g.le_iff_le.mp <| h.le_of_le hj <| g.monotone hle⟩

theorem MaximalFor.of_strictMonoOn_comp {ι α β : Type*} [Preorder α] [Preorder β] {P : ι → Prop}
    {f : ι → α} {g : α → β} {i : ι} (hg : StrictMonoOn g (f '' setOf P))
    (h : MaximalFor P (g ∘ f) i) : MaximalFor P f i := by
  refine ⟨h.prop, fun j hj hle ↦ ?_⟩
  by_contra
  exact h.not_gt hj <| hg ⟨i, h.prop, rfl⟩ ⟨j, hj, rfl⟩ <| lt_of_le_not_ge hle this

[Bhavik Mehta]

(I haven't thought about your specific question but let me quickly say that results like this should be in mathlib, there's a lot of useful and basic api missing for MaximalFor!)

[Snir Broshi]

#34655