fix(algebra/big_operators): congruence rules need to provide equation…

…s for all rewritable positions

algebra/big_operators.lean

@@ -44,8 +44,9 @@ lemma prod_image [decidable_eq α] [decidable_eq γ] {s : finset γ} {g : γ →
 fold_image
 
 @[congr, to_additive finset.sum_congr]
-lemma prod_congr : (∀x∈s, f x = g x) → s.prod f = s.prod g :=
-fold_congr
+lemma prod_congr (h : s₁ = s₂) : (∀x∈s₂, f x = g x) → s₁.prod f = s₂.prod g :=
+by rw [h]; exact fold_congr
+attribute [congr] finset.sum_congr
 
 @[to_additive finset.sum_union_inter]
 lemma prod_union_inter [decidable_eq α] : (s₁ ∪ s₂).prod f * (s₁ ∩ s₂).prod f = s₁.prod f * s₂.prod f :=
@@ -120,7 +121,7 @@ eq.trans (by rw [h₁]; refl) (fold_hom h₂)
 lemma prod_subset (h : s₁ ⊆ s₂) (hf : ∀x∈s₂, x ∉ s₁ → f x = 1) : s₁.prod f = s₂.prod f :=
 by have := classical.dec_eq α; exact
 have (s₂ \ s₁).prod f = (s₂ \ s₁).prod (λx, 1),
-  from prod_congr begin simp [hf] {contextual := tt} end,
+  from prod_congr rfl begin simp [hf] {contextual := tt} end,
 by rw [←prod_sdiff h]; simp [this]
 
 @[to_additive sum_attach]
@@ -137,7 +138,7 @@ lemma prod_bij [decidable_eq α] [decidable_eq β] [decidable_eq γ]
   (i_inj : ∀a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀b∈t, ∃a ha, b = i a ha) :
   s.prod f = t.prod g :=
 calc s.prod f = s.attach.prod (λx, f x.val) : prod_attach.symm
-  ... = s.attach.prod (λx, g (i x.1 x.2)) : prod_congr $ assume x hx, h _ _
+  ... = s.attach.prod (λx, g (i x.1 x.2)) : prod_congr rfl $ assume x hx, h _ _
   ... = (s.attach.image $ λx:{x // x ∈ s}, i x.1 x.2).prod g :
     (prod_image $ assume (a₁:{x // x ∈ s}) _ a₂ _ eq, subtype.eq $ i_inj a₁.1 a₂.1 a₁.2 a₂.2 eq).symm
   ... = _ :

algebra/linear_algebra/basic.lean

@@ -222,7 +222,7 @@ lemma linear_eq_on {f g : β → γ} (hf : is_linear_map f) (hg : is_linear_map
 | _ ⟨l, hl, rfl⟩ :=
   begin
     simp [hf.finsupp_sum, hg.finsupp_sum],
-    apply finset.sum_congr,
+    apply finset.sum_congr rfl,
     assume b hb,
     have : b ∈ s, { by_contradiction, simp * at * },
     simp [this, h, hf.smul, hg.smul]
@@ -465,7 +465,7 @@ funext $ assume b, linear_eq_on hf hg h (hs.2 b)
 
 lemma constr_congr {f g : β → γ} {b : β} (hs : is_basis s) (h : ∀b∈s, f b = g b) :
   hs.constr f = hs.constr g :=
-funext $ assume b', finset.sum_congr $ assume b hb,
+funext $ assume b', finset.sum_congr rfl $ assume b hb,
   have b ∈ s, from repr_support hs.1 hb,
   by simp [h b this]
 
@@ -521,7 +521,7 @@ def module_equiv_lc (hs : is_basis s) : β ≃ (s →₀ α) :=
     have v.sum (λb' a, hs.1.repr (a • b'.val) b) = v ⟨b, hb⟩,
       from calc v.sum (λb' a, hs.1.repr (a • b'.val) b) =
           v.sum (λb' a, a * (finsupp.single b'.val 1 : lc α β) b) :
-            finset.sum_congr $ assume ⟨b', hb'⟩ h',
+            finset.sum_congr rfl $ assume ⟨b', hb'⟩ h',
               by dsimp; rw [repr_smul hs.1 (hs.2 _), repr_eq_single _ hb']; refl
         ... = ({⟨b, hb⟩} : finset s).sum (λb', v b' * (finsupp.single b'.val 1 : lc α β) b) :
           finset.sum_bij_ne_zero (λx hx x0, x)

analysis/topology/infinite_sum.lean

@@ -204,7 +204,7 @@ is_sum_of_is_sum $ assume u, exists.intro (ii u) $
     by rw [hji h] at this; exact hnc this,
   calc (u ∪ jj v).sum g = (jj v).sum g : (sum_subset subset_union_right this).symm
     ... = v.sum _ : sum_bind $ by intros x hx y hy hxy; by_cases f x = 0; by_cases f y = 0; simp [*]
-    ... = v.sum f : sum_congr $ by intros x hx; by_cases f x = 0; simp [*]
+    ... = v.sum f : sum_congr rfl $ by intros x hx; by_cases f x = 0; simp [*]
 
 lemma is_sum_iff_is_sum_of_ne_zero : is_sum f a ↔ is_sum g a :=
 iff.intro
@@ -405,7 +405,7 @@ suffices cauchy (at_top.map (λs:finset β, s.sum f')),
       ... = (u.filter (λb, f' b ≠ 0)).sum f :
         by simp
       ... = (u.filter (λb, f' b ≠ 0)).sum f' :
-        sum_congr $ assume b, by have h := h b; cases h with h h; simp [*]
+        sum_congr rfl $ assume b, by have h := h b; cases h with h h; simp [*]
       ... = u.sum f' :
         by apply sum_subset; by simp [subset_iff, not_not] {contextual := tt},
   have ∀{u₁ u₂}, t ⊆ u₁ → t ⊆ u₂ → (u₁.sum f', u₂.sum f') ∈ s',

data/finsupp.lean

@@ -272,7 +272,7 @@ begin
     refine (finset.sum_subset this _).symm,
     simp {contextual := tt} },
   { transitivity (f.support.sum (λa, (0 : β))),
-    { refine (finset.sum_congr _),
+    { refine (finset.sum_congr rfl _),
       intros a' ha',
       have h: a' ≠ a,
         { assume eq, simp * at * },
@@ -351,7 +351,7 @@ sum_zero_index
 
 lemma map_domain_congr {f g : α → α₂} (h : ∀x∈v.support, f x = g x) :
   v.map_domain f = v.map_domain g :=
-finset.sum_congr $ by simp [*] at * { contextual := tt}
+finset.sum_congr rfl $ by simp [*] at * { contextual := tt}
 
 lemma map_domain_add {f : α → α₂} : map_domain f (v₁ + v₂) = map_domain f v₁ + map_domain f v₂ :=
 sum_add_index (by simp) (by simp)