Map factorization

Stream: new members

[Florestan]

Hi, I'm having trouble proving the following statement:

lemma map_factor {A B C:Type*} {U : Set A} {f : A → B} {s : C → B}
    (h: ∀ c : C, s c ∈ f '' U):
    ∃ s' : C → A, ( s = f ∘ s' ∧ ∀ c : C, s' c ∈ U) := by sorry

I can define the s' I'm looking for:

  set s' : C → A := by
    intro c
    choose a ha using (h c)
    exact a

but then I don't know how to prove that it satisfies the properties, because the proofs hathat I need are somehow lost when we left the definition of the function.

By the way I would also be happy to know if this result is already stated somewhere !

[Mitchell Lee]

It's frowned upon to use tactic mode for anything other than proofs for essentially this reason. If you define s' using tactic mode, it's hard to then look into the definition later.

You can start the proof with the line choose s' hs' using h, which will get you both the function and the hypothesis that it satisfies.

theorem map_factor {A B C : Type*} {U : Set A} {f : A → B} {s : C → B}
    (h : ∀ c : C, s c ∈ f '' U):
    ∃ s' : C → A, s = f ∘ s' ∧ ∀ c : C, s' c ∈ U := by
  choose s' hs' using h
  -- s' : C → A
  -- hs' : ∀ (c : C), s' c ∈ U ∧ f (s' c) = s c
  use s'
  constructor
  · ext c
    exact (hs' c).2.symm
  · exact (forall_and.mp hs').1

[Florestan]

Oh, I see thank you !
Does it means that for Lean
\forall x \exists y, P(x,y)
is "the same" as
\exists y \forall x, P(x, y(x))
?

[Mitchell Lee]

No. However, the choose tactic will yield a function when used on a hypothesis of the form∀ x, ∃ y, P x y. You can read more about the tactic here: https://raw.githubusercontent.com/haruhisa-enomoto/mathlib4-all-tactics/main/all-tactics.md

This is more powerful than the cases or obtain tactic, which can be used to obtain an term satisfying an existence statement, but cannot be used on ∀ x, ∃ y, P x y.