Set.image with membership hypothesis

Stream: mathlib4

[Enrico Borba]

Is there a version of Set.image that accepts a function along with a hypothesis of membership? Something like:

def Set.image' {α : Type _} {β : Type _} (s : Set α) (f : α → α ∈ s → β) : Set β

In case this is an XY problem: I have a finite set of elements U = {a₁, .., aₙ} : Set α, and I have another set K : Set (Set α). For each element in U, there exists an element in K containing it. That is, I have hU : ∀ aᵢ ∈ U, ∃ Yᵢ ∈ K, aᵢ ∈ Yᵢ (though there may be multiple Yᵢs to choose from). I want to (noncomputably) produce a set Ys : Set α that is effectively selecting a Yᵢ for each aᵢ. Critically, however, I want a single Yᵢ for each aᵢ, as I have Set.Finite U, and want to have Set.Finite Ys as well. K is infinite and there may be infinitely many Yᵢ to choose from for each aᵢ.

I tried to do something like {Exists.choose (hU aᵢ) | aᵢ ∈ U}, but hU requires a proof of aᵢ ∈ U.

[Eric Rodriguez]

You can use Set.attach

[Enrico Borba]

Oh huh, that's an interesting idea. Let me play around with that

[Enrico Borba]

Also do you mean Finset.attach?

[Enrico Borba]

I think this will end up working, but definitely creates some nasty types b/c of the subtype.

[Enrico Borba]

I think the move is actually something like

let Ys := { (hU αᵢ αᵢ.prop).choose | αᵢ : U }

[Enrico Borba]

Note the αᵢ : U instead of αᵢ ∈ U

[Richard Copley]

Nice, and is Ys Finite?
If U is a Finset, you can write U.attach.image fun u : ↥U => (hU u.val u.property).choose, or come up with a Function.Embedding e : ↥U ↪ K and write U.attach.map e [untested (an #mwe would be useful)].

[Eric Wieser]

This works on your original code sample:

import Mathlib.Data.Set.Basic

def Set.image' {α : Type _} {β : Type _} (s : Set α) (f : (a : α) → a ∈ s → β) : Set β :=
  {b | ∃ a ha, f a ha = b}

[Eric Wieser]

As does

def Set.image'' {α : Type _} {β : Type _} (s : Set α) (f : (a : α) → a ∈ s → β) : Set β :=
  Subtype.rec f '' univ

[Enrico Borba]

Richard Copley said:

Nice, and is Ys Finite?

Actually stuck on that now haha. I have Set.Finite U.

The embedding is a good suggestion.

[Enrico Borba]

Let me put together a mwe, trying to prove some lemmas on chains needed for Lindenbaum's Lemma

[Enrico Borba]

Uh on second thought might do that (provide a mwe) later, the proof is a bit disorganized at the moment and I should reorganize it first. This has already been a big help :)

[Enrico Borba]

I have sort of a mwe. It's not as relevant to the question, but

import Mathlib.Data.Set.Finite
import Mathlib.Order.Chain

variable
  {α : Sort _} {K : Set (Set α)}
  (hK : IsChain (· ⊆ ·) K) (U₀ : Set α) (hU₀fin : Set.Finite U₀)
  (map : ∀ αᵢ ∈ U₀, ∃ Yᵢ ∈ K, αᵢ ∈ Yᵢ)

theorem U₀_supset : ∃ Y ∈ K, U₀ ⊆ Y := by
  sorry

is essentially what I'm trying to prove. My initial thought (and what spawned my original question) was to map each αᵢ ∈ U₀ to a Yᵢ using map. Then use Finset.max by showing a linear order since they are members of the chain K. I'm wondering now if there's a simpler solution, but that's beyond the scope of this thread :)

[Enrico Borba]

Maybe induction on the cardinality is simpler

[Enrico Borba]

just to close this out, while this can probably be golfed, I ended up solving it with induction:

import Mathlib.Data.Set.Finite
import Mathlib.Order.Chain

lemma chain_fin_subset_max
  {α : Sort _} {K : Set (Set α)} (hKne : Set.Nonempty K) (hKc : IsChain (· ⊆ ·) K)
  (U₀ : Set α) (hU₀fin : Set.Finite U₀)
  (map : ∀ αᵢ ∈ U₀, ∃ Yᵢ ∈ K, αᵢ ∈ Yᵢ) : ∃ Y ∈ K, U₀ ⊆ Y := by
  induction' h : Set.ncard U₀ with n n_ih generalizing U₀
  · rw [Set.ncard_eq_zero hU₀fin] at h
    rw [h]
    have ⟨Y, hY⟩ := hKne
    exact ⟨Y, hY, Set.empty_subset Y⟩

  · have ⟨αₙ, U₀', hαₙnotin, hαₙinsert, hU₀'card⟩ := Set.eq_insert_of_ncard_eq_succ h
    have hαₙ : αₙ ∈ U₀ := by rw [←hαₙinsert]; exact Set.mem_insert _ _
    have hαₙinsert_sub : insert αₙ U₀' ⊆ U₀ := by rw [hαₙinsert]
    have hU₀'sub : U₀' ⊂ U₀ := Set.ssubset_iff_insert.mpr ⟨αₙ, hαₙnotin, hαₙinsert_sub⟩
    have hU₀'fin : Set.Finite U₀' := Set.Finite.subset hU₀fin hU₀'sub.left
    have map' : ∀ αᵢ ∈ U₀', ∃ Yᵢ ∈ K, αᵢ ∈ Yᵢ := by
      intro αᵢ hαᵢ
      exact map αᵢ (Set.mem_of_subset_of_mem hU₀'sub.left hαᵢ)
    have ⟨Y', hY'memK, hY'sup⟩ := n_ih U₀' hU₀'fin map' hU₀'card
    have ⟨Yₙ, hYₙmemK, hαₙmemYₙ⟩ := map αₙ hαₙ

    wlog hneq : Y' ≠ Yₙ
    · simp only [ne_eq, not_not] at hneq
      apply Exists.intro Y'
      apply And.intro hY'memK
      intro αᵢ hαᵢ
      simp [←hαₙinsert] at hαᵢ
      match hαᵢ with
      | Or.inl hαᵢeqαₙ => rw [hαᵢeqαₙ, hneq]; exact hαₙmemYₙ
      | Or.inr hαᵢmemU₀' => exact hY'sup hαᵢmemU₀'

    apply Or.elim (hKc hY'memK hYₙmemK hneq)
    · intro hY'subYₙ
      suffices hU₀subYₙ : U₀ ⊆ Yₙ
      · exact ⟨Yₙ, hYₙmemK, hU₀subYₙ⟩
      intro αᵢ hαᵢ
      simp [←hαₙinsert] at hαᵢ
      match hαᵢ with
      | Or.inl hαᵢeqαₙ => rw [hαᵢeqαₙ]; exact hαₙmemYₙ
      | Or.inr hαᵢmemU₀' => exact hY'subYₙ (hY'sup hαᵢmemU₀')

    · intro hYₙsub
      apply Exists.intro Y'
      apply And.intro hY'memK
      intro αᵢ hαᵢ
      simp [←hαₙinsert] at hαᵢ
      match hαᵢ with
      | Or.inl hαᵢeqαₙ => rw [hαᵢeqαₙ]; exact hYₙsub hαₙmemYₙ
      | Or.inr hαᵢmemU₀' => exact hY'sup hαᵢmemU₀'

[Eric Wieser]

I get the feeling starting with induction U₀, hU₀fin using Set.Finite.dinduction_on with would make the proof shorter

[Enrico Borba]

Can you explain your intuition a bit? I'm not used to using induction tactics other than induction and induction'

[Eric Wieser]

lemma chain_fin_subset_max
  {α : Sort _} {K : Set (Set α)} (hKne : Set.Nonempty K) (hKc : IsChain (· ⊆ ·) K)
  (U₀ : Set α) (hU₀fin : Set.Finite U₀)
  (map : ∀ aᵢ ∈ U₀, ∃ Yᵢ ∈ K, aᵢ ∈ Yᵢ) : ∃ Y ∈ K, U₀ ⊆ Y := by
  induction U₀, hU₀fin using Set.Finite.dinduction_on with
  | H0 =>
    obtain ⟨Y, hY⟩ := hKne
    refine ⟨Y, hY, Set.empty_subset _⟩
  | @H1 a s _ _ ih =>
    obtain ⟨ya, hyak, haya⟩ := map a (Set.mem_insert _ _)
    obtain ⟨ys, hyk, hsys⟩ := ih fun a ha => map a (Set.mem_insert_of_mem _ ha)
    obtain rfl | hne := eq_or_ne ya ys
    · exact ⟨ya, hyak, Set.insert_subset haya hsys⟩
    cases hKc hyk hyak hne.symm with
    | inl h =>
      exact ⟨ya, hyak, Set.insert_subset haya <| hsys.trans h⟩
    | inr h =>
      refine ⟨ys, hyk, Set.insert_subset (h haya) hsys⟩

[Eric Wieser]

The induction tactic lets you pass a custom induction principle

[Eric Wieser]

docs#Set.Finite.dinduction_on is the one that say "a finite set can be built by adding one element at a time"

[Enrico Borba]

dang that is much shorter. I'll have to look at the tactic definition a bit to understand why it's a theorem that you can pass to induction. I guess, I'm unsure what counts as an "induction principle". Had I seen Set.Finite.dinduction_on earlier, I would have tried to use it directly with apply.

[Enrico Borba]

Also, can you explain your preference with obtain and refine instead of have and exact (in the cases where they can be used instead, aka not the obtain rfl | hne constructs).

[Eric Wieser]

I think that's just me being sloppy, and leaning on Lean3 muscle memory

[Eric Wieser]

Probably refine should give an error saying "use exact instead"

[Enrico Borba]

Got it. Thanks a ton :) Honestly super impressive to see such a short proof composed so quickly haha

[Eric Wieser]

Well, you already wrote down the mathematical ideas first, which made it much easier

[Enrico Borba]

Also, i'm trying to understand this section

obtain rfl | hne := eq_or_ne ya ys
· exact ⟨ya, hyak, Set.insert_subset haya hsys⟩

it seems equivalent to

wlog hne : Yₙ ≠ Y'
· rw [ne_eq, not_not] at hne
  exact ⟨Yₙ, hYₙmemK, Set.insert_subset hαₙmemYₙ (hne ▸ hY'sup)⟩

But I can't seem to wrap my head around what rfl is being applied to, or what kind of pattern rfl | hne is.

(sorry for the slightly renamed variables in my version)

[Eric Wieser]

obtain rfl | hne := eq_or_ne ya ys is the same as obtain heq | hne := eq_or_ne ya ys, then subst heq on the branch that uses it

[Eric Wieser]

The pattern is matching against the or, and rfl is matching against the equality

[Eric Wieser]

I've not seen wlog used in that way before, but my spelling avoids the annoying Not (Ne _ _) that appears in yours

[Enrico Borba]

yeah absolutely, don't like the rw needed to transform the negative ¬ (Yₙ ≠ Y'). Oh, rfl from the equality makes a bit more sense, thanks.

Hmm I'll have to reread that a few times. I might try expanding the obtains to rcases, and see if I understand that better.

[Enrico Borba]

Oh I see this from the rcases docs:

The keyword rfl, which expects the hypothesis to be h : a = b, and calls subst on the hypothesis (which has the effect of replacing b with a everywhere or vice versa).

[Eric Wieser]

obtain $patt := $val is pretty much identical torcases $val with $patt

[Eric Wieser]

So I doubt you will learn anything by rewriting obtain to rcases :wink:

[Enrico Borba]

Yeah it's just weird (to me) to see the patt and val swap places, but yeah it's not that much insight... I think what really cleared it up is the fact that rfl is special grammar, and applies the equality to all of the hypotheses, and that two goals are created. Pretty clever