preimage of finite sets is finite if finite fibers

Stream: Is there code for X?

[Antoine Chambert-Loir]

Three questions here,

1) does mathlib have the following

import Mathlib.Data.Set.Finite

theorem Set.Finite.preimage'  {α : Type*} {β : Type*} {f : α → β} {s : Set β}
    (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite) :
    (f ⁻¹' s).Finite := by
  apply Set.Finite.induction_on
    (C := fun s ↦ ∀ (_ : s.Finite) (_ : ∀ b ∈ s, (f ⁻¹' {b}).Finite),
      (f ⁻¹' s).Finite) h
  · intro _ _
    simp only [preimage_empty, finite_empty]
  · intro a s _ hs hrec _ hf
    rw [← singleton_union, Set.preimage_union]
    apply Set.Finite.union -- finite_biUnion''
    · exact hf a (mem_insert a s)
    · exact hrec hs (fun b hb ↦ hf b (mem_insert_of_mem a hb))
  exact h
  exact hf

2) is it worth having the (slightly strongest) version where only (range f ∩ s).Finite
(It can be deduced easily using preimage_range_inter.

3) The code above has a strange behaviour. After the apply, I have 4 goals to check, and I don't understand why h and hf have to be given.

[Vincent Beffara]

Can you use docs#Set.Finite.biUnion instead of proving it by hand?

[Vincent Beffara]

import Mathlib.Data.Set.Finite

theorem Set.Finite.preimage'  {α : Type*} {β : Type*} {f : α → β} {s : Set β}
    (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite) :
    (f ⁻¹' s).Finite := by
  rw [← Set.biUnion_preimage_singleton] ; exact Set.Finite.biUnion h hf

[Anatole Dedecker]

If someone wants to adopt #6449 feel free to do so :sweat:

[Antoine Chambert-Loir]

Thanks for the one-line proof, Vincent !
If anyone can explain the bizarre behavior of the apply, I'd be grateful too.

[Junyan Xu]

3) The code above has a strange behaviour. After the apply, I have 4 goals to check, and I don't understand why h and hf have to be given.

apply doesn't automatically close the goals with matching assumptions in the context; you can do

  apply Set.Finite.induction_on
    (C := fun s ↦ s.Finite → (∀ b ∈ s, (f ⁻¹' {b}).Finite) → (f ⁻¹' s).Finite) h _ _ h hf

to save the last two lines. h and hf are the first two arguments in C.