chore(algebra/big_operators): move, golf (#9218)

move 2 lemmas up and golf the proof of `finset.prod_subset`.

src/algebra/big_operators/basic.lean

@@ -387,13 +387,23 @@ lemma prod_hom_rel [comm_monoid γ] {r : β → γ → Prop} {f : α → β} {g
   (h₁ : r 1 1) (h₂ : ∀ a b c, r b c → r (f a * b) (g a * c)) : r (∏ x in s, f x) (∏ x in s, g x) :=
 by { delta finset.prod, apply multiset.prod_hom_rel; assumption }
 
+@[to_additive]
+lemma prod_eq_one {f : α → β} {s : finset α} (h : ∀ x ∈ s, f x = 1) : (∏ x in s, f x) = 1 :=
+calc (∏ x in s, f x) = ∏ x in s, 1 : finset.prod_congr rfl h
+  ... = 1 : finset.prod_const_one
+
+@[to_additive]
+lemma prod_subset_one_on_sdiff [decidable_eq α] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ (s₂ \ s₁), g x = 1)
+  (hfg : ∀ x ∈ s₁, f x = g x) : ∏ i in s₁, f i = ∏ i in s₂, g i :=
+begin
+  rw [← prod_sdiff h, prod_eq_one hg, one_mul],
+  exact prod_congr rfl hfg
+end
+
 @[to_additive]
 lemma prod_subset (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1) :
   (∏ x in s₁, f x) = ∏ x in s₂, f x :=
-by haveI := classical.dec_eq α; exact
-have ∏ x in s₂ \ s₁, f x = ∏ x in s₂ \ s₁, 1,
-  from prod_congr rfl $ by simpa only [mem_sdiff, and_imp],
-by rw [←prod_sdiff h]; simp only [this, prod_const_one, one_mul]
+by haveI := classical.dec_eq α; exact prod_subset_one_on_sdiff h (by simpa) (λ _ _, rfl)
 
 @[to_additive]
 lemma prod_filter_of_ne {p : α → Prop} [decidable_pred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) :
@@ -534,11 +544,6 @@ lemma prod_subtype {p : α → Prop} {F : fintype (subtype p)} (s : finset α)
   ∏ a in s, f a = ∏ a : subtype p, f a :=
 have (∈ s) = p, from set.ext h, by { substI p, rw [←prod_finset_coe], congr }
 
-@[to_additive]
-lemma prod_eq_one {f : α → β} {s : finset α} (h : ∀ x ∈ s, f x = 1) : (∏ x in s, f x) = 1 :=
-calc (∏ x in s, f x) = ∏ x in s, 1 : finset.prod_congr rfl h
-  ... = 1 : finset.prod_const_one
-
 @[to_additive] lemma prod_apply_dite {s : finset α} {p : α → Prop} {hp : decidable_pred p}
   [decidable_pred (λ x, ¬ p x)] (f : Π (x : α), p x → γ) (g : Π (x : α), ¬p x → γ)
   (h : γ → β) :
@@ -749,14 +754,6 @@ begin
   exact ⟨x, (mem_filter.1 hx).1, (mem_filter.1 hx).2⟩
 end
 
-@[to_additive]
-lemma prod_subset_one_on_sdiff [decidable_eq α] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ (s₂ \ s₁), g x = 1)
-  (hfg : ∀ x ∈ s₁, f x = g x) : ∏ i in s₁, f i = ∏ i in s₂, g i :=
-begin
-  rw [← prod_sdiff h, prod_eq_one hg, one_mul],
-  exact prod_congr rfl hfg
-end
-
 @[to_additive]
 lemma prod_range_succ_comm (f : ℕ → β) (n : ℕ) :
   ∏ x in range (n + 1), f x = f n * ∏ x in range n, f x :=