chore: forward-port leanprover-community/mathlib#19050 (#4119)

Mathlib/Algebra/BigOperators/Ring.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 algebra.big_operators.ring
-! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
+! leanprover-community/mathlib commit b2c89893177f66a48daf993b7ba5ef7cddeff8c9
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -111,7 +111,7 @@ theorem prod_sum {δ : α → Type _} [DecidableEq α] [∀ a, DecidableEq (δ a
     rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
     refine' sum_congr rfl fun b _ => _
     have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
-      fun p₁ _ p₂ _ eq => pi_cons_injective ha eq
+      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
     rw [sum_image h₂, mul_sum]
     refine' sum_congr rfl fun g _ => _
     rw [attach_insert, prod_insert, prod_image]

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 4c586d291f189eecb9d00581aeb3dd998ac34442
+! leanprover-community/mathlib commit b2c89893177f66a48daf993b7ba5ef7cddeff8c9
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -74,17 +74,17 @@ theorem Pi.cons_ne {s : Finset α} {a a' : α} {b : δ a} {f : ∀ a, a ∈ s 
   Multiset.Pi.cons_ne _ (Ne.symm ha)
 #align finset.pi.cons_ne Finset.Pi.cons_ne
 
-theorem pi_cons_injective {a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) :
+theorem Pi.cons_injective {a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) :
     Function.Injective (Pi.cons s a b) := fun e₁ e₂ eq =>
-  @Multiset.pi_cons_injective α _ δ a b s.1 hs _ _ <|
+  @Multiset.Pi.cons_injective α _ δ a b s.1 hs _ _ <|
     funext fun e =>
       funext fun h =>
         have :
           Pi.cons s a b e₁ e (by simpa only [Multiset.mem_cons, mem_insert] using h) =
             Pi.cons s a b e₂ e (by simpa only [Multiset.mem_cons, mem_insert] using h) :=
           by rw [eq]
         this
-#align finset.pi_cons_injective Finset.pi_cons_injective
+#align finset.pi.cons_injective Finset.Pi.cons_injective
 
 @[simp]
 theorem pi_empty {t : ∀ a : α, Finset (β a)} : pi (∅ : Finset α) t = singleton (Pi.empty β) :=
@@ -108,7 +108,7 @@ theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, F
       _ (insert_val_of_not_mem ha)
   subst s'; rw [pi_cons]
   congr ; funext b
-  exact ((pi s t).nodup.map <| Multiset.pi_cons_injective ha).dedup.symm
+  exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm
 #align finset.pi_insert Finset.pi_insert
 
 theorem pi_singletons {β : Type _} (s : Finset α) (f : α → β) :

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 4c586d291f189eecb9d00581aeb3dd998ac34442
+! leanprover-community/mathlib commit b2c89893177f66a48daf993b7ba5ef7cddeff8c9
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -61,6 +61,28 @@ theorem Pi.cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f :
   all_goals simp [*, Pi.cons_same, Pi.cons_ne]
 #align multiset.pi.cons_swap Multiset.Pi.cons_swap
 
+@[simp, nolint simpNF] --Porting note: false positive, this lemma can prove itself
+theorem pi.cons_eta {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
+  ext (a' h')
+  by_cases h : a' = a
+  · subst h
+    rw [Pi.cons_same]
+  · rw [Pi.cons_ne _ h]
+#align multiset.pi.cons_eta Multiset.pi.cons_eta
+
+theorem Pi.cons_injective {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) :
+    Function.Injective (Pi.cons s a b) := fun f₁ f₂ eq =>
+  funext fun a' =>
+    funext fun h' =>
+      have ne : a ≠ a' := fun h => hs <| h.symm ▸ h'
+      have : a' ∈ a ::ₘ s := mem_cons_of_mem h'
+      calc
+        f₁ a' h' = Pi.cons s a b f₁ a' this := by rw [Pi.cons_ne this ne.symm]
+        _ = Pi.cons s a b f₂ a' this := by rw [eq]
+        _ = f₂ a' h' := by rw [Pi.cons_ne this ne.symm]
+#align multiset.pi.cons_injective Multiset.Pi.cons_injective
+
 /-- `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 β}
@@ -93,18 +115,6 @@ theorem pi_cons (m : Multiset α) (t : ∀ a, Multiset (β a)) (a : α) :
   recOn_cons a m
 #align multiset.pi_cons Multiset.pi_cons
 
-theorem pi_cons_injective {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) :
-    Function.Injective (Pi.cons s a b) := fun f₁ f₂ eq =>
-  funext fun a' =>
-    funext fun h' =>
-      have ne : a ≠ a' := fun h => hs <| h.symm ▸ h'
-      have : a' ∈ a ::ₘ s := mem_cons_of_mem h'
-      calc
-        f₁ a' h' = Pi.cons s a b f₁ a' this := by rw [Pi.cons_ne this ne.symm]
-        _ = Pi.cons s a b f₂ a' this := by rw [eq]
-        _ = 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)) :
     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])
@@ -119,7 +129,7 @@ protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} :
       have hs : Nodup s := by simp at hs; exact hs.2
       simp
       refine'
-        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (pi_cons_injective has),
+        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
           _⟩
       refine' (ht a <| mem_cons_self _ _).pairwise _
       exact fun b₁ _ b₂ _ neb =>
@@ -129,16 +139,6 @@ protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} :
           neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this)
 #align multiset.nodup.pi Multiset.Nodup.pi
 
-@[simp, nolint simpNF] --Porting note: false positive, this lemma can prove itself
-theorem pi.cons_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
-  ext (a' h')
-  by_cases h : a' = a
-  · subst h
-    rw [Pi.cons_same]
-  · rw [Pi.cons_ne _ h]
-#align multiset.pi.cons_ext Multiset.pi.cons_ext
-
 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
@@ -156,7 +156,7 @@ theorem mem_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
       apply hf'
   · intro hf
     refine' ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), _⟩
-    rw [pi.cons_ext]
+    rw [pi.cons_eta]
 #align multiset.mem_pi Multiset.mem_pi
 
 end Pi