orders of set / add conditons

Stream: mathlib4

[Yi.Yuan]

import Mathlib

universe u v w

variable {ι : Type v} [OrderedAddCommMonoid ι]

/--For `σ` satisfying `SetLike σ A`, an increasing series of `F` in `σ` is filtration if
there is another series `F_lt` equal to the supremum of `F` with smaller index-/
class IsFiltration {A : Type u} {σ : Type*} [SetLike σ A](F : ι → σ) (F_lt : outParam <| ι → σ) : Prop where
  mono {i j} : i ≤ j → F i ≤ F j
  is_le {i} : i < j → F i ≤ F_lt j
  is_sup (B : σ) (j : ι) : (∀ i < j, F i ≤ B) → F_lt j ≤ B
/- In fact `F_lt j = ⨆ i < j, F i`, the design of `F_lt` can handle different conditions in the
same structure, it avoid adding `CompleteLattice` to `σ`, also providing convenience when the index
is `ℤ`-/

variable {A : Type*} (σA : Type*) [SetLike σA A] {B : Type*}  (σB : Type*) [SetLike σB B]

class SubmonoidClassHom (f : A → B) where
  map : σA → σB
  coe_map (x : σA) : f '' (x : Set A) = map x
  comap : σB → σA/-I want to change `comap` and `coe_comap` to some weaker conditions-/
  coe_comap (y : σB) : (comap y : Set A) = f ⁻¹' y

lemma IsFiltration_isSup (FA : ι → σA) (FA_lt : ι → σA) (f : A → B) [fil : IsFiltration FA FA_lt]
[SubmonoidClassHom σA σB f] (Sup : σB) (j : ι) : ∀ i < j, SubmonoidClassHom.map f (FA i) ≤ Sup →
 ((SubmonoidClassHom.map f (FA_lt j) : σB): Set B) ≤ (Sup : Set B) := by
  intro i i_lt_j h
  rw[← SubmonoidClassHom.coe_map <| FA_lt j]
  refine Set.le_iff_subset.mpr <| Set.image_subset_iff.mpr ?_
  have h : ∀ i < j, ↑(FA i) ≤ f ⁻¹' ↑Sup := by
    intro i i_lt_j
    have : f '' (FA i) ≤ Sup := by
      have : ((SubmonoidClassHom.map f (FA i) : σB) : Set B) ≤ (Sup : Set B) := h i i_lt_j
      rwa[← SubmonoidClassHom.coe_map <| FA i] at this
    exact Set.le_iff_subset.mpr <| Set.image_subset_iff.mp this

  /-How to finish the proof by using weaker conditions? -/
  have : (SubmonoidClassHom.comap f Sup : σA) = f ⁻¹' Sup := SubmonoidClassHom.coe_comap Sup
  rw[← this] at h ⊢
  exact IsFiltration.is_sup (SubmonoidClassHom.comap f Sup : σA) j h

In mathmatics, we have two sets σA and σB of type A and B (It may be empty sets in lean!, so we add conditions to describ them) and f : A → B , we need to add some conditions to describe σA and σB in order to proof : ∀ i < j, f (FA i) ≤ Sup → f (FA_lt j) ≤ Sup

the first and second condition in SubmonoidClassHom is necessary to ensure f (FA i) exist in σB. Now, the question is how to weaker the third and fourth condition(comap and coe_comap)?