instSupSet — Mathlib

Lean4
instance : SupSet (SubDPIdeal hI) :=
  ⟨fun S ↦
    SubDPIdeal.mk' (J := sSup ((fun J ↦ J.carrier) '' S)) <|
      by
      have h : (⋃ (i : Ideal A) (_ : i ∈ (fun J ↦ J.carrier) '' S), ↑i) ⊆ (I : Set A) :=
        by
        rintro a ⟨-, ⟨J, rfl⟩, haJ⟩
        rw [Set.mem_iUnion, SetLike.mem_coe, exists_prop] at haJ
        obtain ⟨J', hJ'⟩ := (Set.mem_image _ _ _).mp haJ.1
        exact J'.isSubideal (hJ'.2 ▸ haJ.2)
      rw [sSup_eq_iSup, Submodule.iSup_eq_span', submodule_span_eq, span_isSubDPIdeal_iff h]
      rintro n hn x ⟨T, ⟨J, rfl⟩, ⟨J', ⟨⟨hJ', rfl⟩, h'⟩⟩⟩
      apply subset_span
      apply Set.mem_biUnion hJ'
      obtain ⟨K, hKS, rfl⟩ := hJ'
      exact K.dpow_mem _ hn x h'⟩
Похожие утверждения