feat: preimage of a product by restrict (#22558)

The preimage of a product of sets by a restriction is the product of the same sets extended with `Set.univ` outside of the restriction.

Author: EtienneC30

Mathlib/Data/Finset/Pi.lean

@@ -165,30 +165,50 @@ def restrict (s : Finset ι) (f : (i : ι) → π i) : (i : s) → π i := fun x
 
 theorem restrict_def (s : Finset ι) : s.restrict (π := π) = fun f x ↦ f x := rfl
 
-theorem _root_.Set.piCongrLeft_comp_restrict {s : Finset ι} :
+variable {s t u : Finset ι}
+
+theorem _root_.Set.piCongrLeft_comp_restrict :
     (s.equivToSet.symm.piCongrLeft (fun i : s.toSet ↦ π i)) ∘ s.toSet.restrict = s.restrict := rfl
 
-theorem piCongrLeft_comp_restrict {s : Finset ι} :
+theorem piCongrLeft_comp_restrict :
     (s.equivToSet.piCongrLeft (fun i : s ↦ π i)) ∘ s.restrict = s.toSet.restrict := rfl
 
 /-- If a function `f` is restricted to a finite set `t`, and `s ⊆ t`,
 this is the restriction to `s`. -/
 @[simp]
-def restrict₂ {s t : Finset ι} (hst : s ⊆ t) (f : (i : t) → π i) : (i : s) → π i :=
-  fun x ↦ f ⟨x.1, hst x.2⟩
+def restrict₂ (hst : s ⊆ t) (f : (i : t) → π i) (i : s) : π i := f ⟨i.1, hst i.2⟩
 
-theorem restrict₂_def {s t : Finset ι} (hst : s ⊆ t) :
-    restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩ := rfl
+theorem restrict₂_def (hst : s ⊆ t) : restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩ := rfl
 
-theorem restrict₂_comp_restrict {s t : Finset ι} (hst : s ⊆ t) :
+theorem restrict₂_comp_restrict (hst : s ⊆ t) :
     (restrict₂ (π := π) hst) ∘ t.restrict = s.restrict := rfl
 
-theorem restrict₂_comp_restrict₂ {s t u : Finset ι} (hst : s ⊆ t) (htu : t ⊆ u) :
+theorem restrict₂_comp_restrict₂ (hst : s ⊆ t) (htu : t ⊆ u) :
     (restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu) := rfl
 
 lemma dependsOn_restrict (s : Finset ι) : DependsOn (s.restrict (π := π)) s :=
   (s : Set ι).dependsOn_restrict
 
+lemma restrict_preimage [DecidablePred (· ∈ s)] (t : (i : s) → Set (π i)) :
+    s.restrict ⁻¹' (Set.univ.pi t) =
+      Set.pi s (fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ) := by
+  ext x
+  simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, restrict, forall_const, Subtype.forall,
+    mem_coe]
+  refine ⟨fun h i hi ↦ by simpa [hi] using h i hi, fun h i hi ↦ ?_⟩
+  convert h i hi
+  rw [dif_pos hi]
+
+lemma restrict₂_preimage [DecidablePred (· ∈ s)] (hst : s ⊆ t) (u : (i : s) → Set (π i)) :
+    (restrict₂ hst) ⁻¹' (Set.univ.pi u) =
+      (@Set.univ t).pi (fun j ↦ if h : j.1 ∈ s then u ⟨j.1, h⟩ else Set.univ) := by
+  ext x
+  simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, restrict₂, forall_const, Subtype.forall]
+  refine ⟨fun h i hi ↦ ?_, fun h i i_mem ↦ by simpa [i_mem] using h i (hst i_mem)⟩
+  split_ifs with i_mem
+  · exact h i i_mem
+  · trivial
+
 end Pi
 
 end Finset