chore: forward-port leanprover-community/mathlib#18429 (#2220)

Also removes a duplicate lemma that was added by accident while porting.

Mathlib/Data/Finset/Pi.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module data.finset.pi
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit 4c586d291f189eecb9d00581aeb3dd998ac34442
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -33,22 +33,23 @@ def Pi.empty (β : α → Sort _) (a : α) (h : a ∈ (∅ : Finset α)) : β a
   Multiset.Pi.empty β a h
 #align finset.pi.empty Finset.Pi.empty
 
-variable {δ : α → Type _} [DecidableEq α]
+universe u v
+variable {β : α → Type u} {δ : α → Sort v} [DecidableEq α]
 
 /-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `δ a`, then one can define the
 finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
 Note that the elements of `s.pi t` are only partially defined, on `s`. -/
-def pi (s : Finset α) (t : ∀ a, Finset (δ a)) : Finset (∀ a ∈ s, δ a) :=
+def pi (s : Finset α) (t : ∀ a, Finset (β a)) : Finset (∀ a ∈ s, β a) :=
   ⟨s.1.pi fun a => (t a).1, s.nodup.pi fun a _ => (t a).nodup⟩
 #align finset.pi Finset.pi
 
 @[simp]
-theorem pi_val (s : Finset α) (t : ∀ a, Finset (δ a)) : (s.pi t).1 = s.1.pi fun a => (t a).1 :=
+theorem pi_val (s : Finset α) (t : ∀ a, Finset (β a)) : (s.pi t).1 = s.1.pi fun a => (t a).1 :=
   rfl
 #align finset.pi_val Finset.pi_val
 
 @[simp]
-theorem mem_pi {s : Finset α} {t : ∀ a, Finset (δ a)} {f : ∀ a ∈ s, δ a} :
+theorem mem_pi {s : Finset α} {t : ∀ a, Finset (β a)} {f : ∀ a ∈ s, β a} :
     f ∈ s.pi t ↔ ∀ (a) (h : a ∈ s), f a h ∈ t a :=
   Multiset.mem_pi _ _ _
 #align finset.mem_pi Finset.mem_pi
@@ -86,12 +87,12 @@ theorem pi_cons_injective {a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) :
 #align finset.pi_cons_injective Finset.pi_cons_injective
 
 @[simp]
-theorem pi_empty {t : ∀ a : α, Finset (δ a)} : pi (∅ : Finset α) t = singleton (Pi.empty δ) :=
+theorem pi_empty {t : ∀ a : α, Finset (β a)} : pi (∅ : Finset α) t = singleton (Pi.empty β) :=
   rfl
 #align finset.pi_empty Finset.pi_empty
 
 @[simp]
-theorem pi_insert [∀ a, DecidableEq (δ a)] {s : Finset α} {t : ∀ a : α, Finset (δ a)} {a : α}
+theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, Finset (β a)} {a : α}
     (ha : a ∉ s) : pi (insert a s) t = (t a).bunionᵢ fun b => (pi s t).image (Pi.cons s a b) :=
   by
   apply eq_of_veq
@@ -128,7 +129,7 @@ theorem pi_const_singleton {β : Type _} (s : Finset α) (i : β) :
   pi_singletons s fun _ => i
 #align finset.pi_const_singleton Finset.pi_const_singleton
 
-theorem pi_subset {s : Finset α} (t₁ t₂ : ∀ a, Finset (δ a)) (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) :
+theorem pi_subset {s : Finset α} (t₁ t₂ : ∀ a, Finset (β a)) (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) :
     s.pi t₁ ⊆ s.pi t₂ := fun _ hg => mem_pi.2 fun a ha => h a ha (mem_pi.mp hg a ha)
 #align finset.pi_subset Finset.pi_subset
 

Mathlib/Data/Multiset/Pi.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module data.multiset.pi
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit 4c586d291f189eecb9d00581aeb3dd998ac34442
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,11 +25,12 @@ open Function
 
 /-- Given `δ : α → Type _`, `Pi.empty δ` is the trivial dependent function out of the empty
 multiset. -/
-def Pi.empty (δ : α → Type _) : ∀ a ∈ (0 : Multiset α), δ a :=
+def Pi.empty (δ : α → Sort _) : ∀ a ∈ (0 : Multiset α), δ a :=
   fun.
 #align multiset.pi.empty Multiset.Pi.empty
 
-variable [DecidableEq α] {δ : α → Type _}
+universe u v
+variable [DecidableEq α] {β : α → Type u} {δ : α → Sort v}
 
 /-- Given `δ : α → Type _`, a multiset `m` and a term `a`, as well as a term `b : δ a` and a
 function `f` such that `f a' : δ a'` for all `a'` in `m`, `Pi.cons m a b f` is a function `g` such
@@ -62,9 +63,9 @@ theorem Pi.cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f :
 #align multiset.pi.cons_swap Multiset.Pi.cons_swap
 
 /-- `pi m t` constructs the Cartesian product over `t` indexed by `m`. -/
-def pi (m : Multiset α) (t : ∀ a, Multiset (δ a)) : Multiset (∀ a ∈ m, δ a) :=
-  m.recOn {Pi.empty δ}
-    (fun a m (p : Multiset (∀ a ∈ m, δ a)) => (t a).bind fun b => p.map <| Pi.cons m a b)
+def pi (m : Multiset α) (t : ∀ a, Multiset (β a)) : Multiset (∀ a ∈ m, β a) :=
+  m.recOn {Pi.empty β}
+    (fun a m (p : Multiset (∀ a ∈ m, β a)) => (t a).bind fun b => p.map <| Pi.cons m a b)
     (by
       intro a a' m n
       by_cases eq : a = a'
@@ -83,12 +84,12 @@ def pi (m : Multiset α) (t : ∀ a, Multiset (δ a)) : Multiset (∀ a ∈ m, 
 #align multiset.pi Multiset.pi
 
 @[simp]
-theorem pi_zero (t : ∀ a, Multiset (δ a)) : pi 0 t = {Pi.empty δ} :=
+theorem pi_zero (t : ∀ a, Multiset (β a)) : pi 0 t = {Pi.empty β} :=
   rfl
 #align multiset.pi_zero Multiset.pi_zero
 
 @[simp]
-theorem pi_cons (m : Multiset α) (t : ∀ a, Multiset (δ a)) (a : α) :
+theorem pi_cons (m : Multiset α) (t : ∀ a, Multiset (β a)) (a : α) :
     pi (a ::ₘ m) t = (t a).bind fun b => (pi m t).map <| Pi.cons m a b :=
   recOn_cons a m
 #align multiset.pi_cons Multiset.pi_cons
@@ -105,12 +106,12 @@ theorem pi_cons_injective {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) :
         _ = f₂ a' h' := by rw [Pi.cons_ne this ne.symm]
 #align multiset.pi_cons_injective Multiset.pi_cons_injective
 
-theorem card_pi (m : Multiset α) (t : ∀ a, Multiset (δ a)) :
+theorem card_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
     card (pi m t) = prod (m.map fun a => card (t a)) :=
   Multiset.induction_on m (by simp) (by simp (config := { contextual := true }) [mul_comm])
 #align multiset.card_pi Multiset.card_pi
 
-protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (δ a)} :
+protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} :
     Nodup s → (∀ a ∈ s, Nodup (t a)) → Nodup (pi s t) :=
   Multiset.induction_on s (fun _ _ => nodup_singleton _)
     (by
@@ -139,14 +140,11 @@ theorem pi.cons_ext {m : Multiset α} {a : α} (f : ∀ a' ∈ a ::ₘ m, δ a')
   · rw [Pi.cons_ne _ h]
 #align multiset.pi.cons_ext Multiset.pi.cons_ext
 
-theorem pi.con_ext {m : Multiset α} {a : α} (f : ∀ a' ∈ a ::ₘ m, δ a') :
-    (Pi.cons m a (f _ (mem_cons_self _ _)) fun a' ha' => f a' (mem_cons_of_mem ha')) = f := by simp
-
-theorem mem_pi (m : Multiset α) (t : ∀ a, Multiset (δ a)) :
-    ∀ f : ∀ a ∈ m, δ a, f ∈ pi m t ↔ ∀ (a) (h : a ∈ m), f a h ∈ t a := by
+theorem mem_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
+    ∀ f : ∀ a ∈ m, β a, f ∈ pi m t ↔ ∀ (a) (h : a ∈ m), f a h ∈ t a := by
   intro f
   induction' m using Multiset.induction_on with a m ih
-  . have : f = Pi.empty δ := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
+  . have : f = Pi.empty β := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
     simp only [this, pi_zero, mem_singleton, true_iff]
     intro _ h; exact (not_mem_zero _ h).elim
   simp_rw [pi_cons, mem_bind, mem_map, ih]