refactor: Lighten finiteness dependencies

update import

Archive/Imo/Imo1987Q1.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Data.Fintype.Perm
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Dynamics.FixedPoints.Basic

Archive/Imo/Imo2013Q1.lean

@@ -3,11 +3,12 @@ Copyright (c) 2021 David Renshaw. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Renshaw
 -/
+import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Data.PNat.Basic
-import Mathlib.Tactic.Ring
 import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Positivity.Basic
 
 #align_import imo.imo2013_q1 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"

Archive/OxfordInvariants/Summer2021/Week3P1.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
-import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Nat.Cast.Field
 

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+import Mathlib.Data.Nat.Interval
 import Mathlib.Data.Fintype.Powerset
 
 #align_import wiedijk_100_theorems.ascending_descending_sequences from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jalex Stark, Yury Kudryashov
 -/
-import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.FieldSimp
 

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -92,8 +92,7 @@ theorem zero_divisors_of_torsion {R A} [Nontrivial R] [Ring R] [AddMonoid A] (a
     · intro b hb b0
       rw [single_pow, one_pow, single_eq_of_ne]
       exact nsmul_ne_zero_of_lt_addOrderOf' b0 (Finset.mem_range.mp hb)
-    · simp only [(zero_lt_two.trans_le o2).ne', Finset.mem_range, not_lt, Nat.le_zero,
-        false_imp_iff]
+    · simp [(zero_lt_two.trans_le o2).ne']
     · rw [single_pow, one_pow, zero_smul, single_eq_same]
   · apply_fun fun x : R[A] => x 0
     refine sub_ne_zero.mpr (ne_of_eq_of_ne (?_ : (_ : R) = 0) ?_)

Mathlib/Algebra/BigOperators/Basic.lean

@@ -521,16 +521,6 @@ lemma prod_powerset_cons (ha : a ∉ s) (f : Finset α → β) :
   simp_rw [cons_eq_insert]
   rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]
 
-/-- A product over `powerset s` is equal to the double product over sets of subsets of `s` with
-`card s = k`, for `k = 1, ..., card s`. -/
-@[to_additive "A sum over `powerset s` is equal to the double sum over sets of subsets of `s` with
-  `card s = k`, for `k = 1, ..., card s`"]
-lemma prod_powerset (s : Finset α) (f : Finset α → β) :
-    ∏ t ∈ powerset s, f t = ∏ j ∈ range (card s + 1), ∏ t ∈ powersetCard j s, f t := by
-  rw [powerset_card_disjiUnion, prod_disjiUnion]
-#align finset.prod_powerset Finset.prod_powerset
-#align finset.sum_powerset Finset.sum_powerset
-
 end CommMonoid
 
 end Finset
@@ -1511,67 +1501,6 @@ theorem exists_ne_one_of_prod_ne_one (h : ∏ x ∈ s, f x ≠ 1) : ∃ a ∈ s,
 #align finset.exists_ne_one_of_prod_ne_one Finset.exists_ne_one_of_prod_ne_one
 #align finset.exists_ne_zero_of_sum_ne_zero Finset.exists_ne_zero_of_sum_ne_zero
 
-@[to_additive]
-theorem prod_range_succ_comm (f : ℕ → β) (n : ℕ) :
-    (∏ x ∈ range (n + 1), f x) = f n * ∏ x ∈ range n, f x := by
-  rw [range_succ, prod_insert not_mem_range_self]
-#align finset.prod_range_succ_comm Finset.prod_range_succ_comm
-#align finset.sum_range_succ_comm Finset.sum_range_succ_comm
-
-@[to_additive]
-theorem prod_range_succ (f : ℕ → β) (n : ℕ) :
-    (∏ x ∈ range (n + 1), f x) = (∏ x ∈ range n, f x) * f n := by
-  simp only [mul_comm, prod_range_succ_comm]
-#align finset.prod_range_succ Finset.prod_range_succ
-#align finset.sum_range_succ Finset.sum_range_succ
-
-@[to_additive]
-theorem prod_range_succ' (f : ℕ → β) :
-    ∀ n : ℕ, (∏ k ∈ range (n + 1), f k) = (∏ k ∈ range n, f (k + 1)) * f 0
-  | 0 => prod_range_succ _ _
-  | n + 1 => by rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]
-#align finset.prod_range_succ' Finset.prod_range_succ'
-#align finset.sum_range_succ' Finset.sum_range_succ'
-
-@[to_additive]
-theorem eventually_constant_prod {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
-    (∏ k ∈ range n, u k) = ∏ k ∈ range N, u k := by
-  obtain ⟨m, rfl : n = N + m⟩ := le_iff_exists_add.mp hn
-  clear hn
-  induction' m with m hm
-  · simp
-  erw [prod_range_succ, hm]
-  simp [hu, @zero_le' ℕ]
-#align finset.eventually_constant_prod Finset.eventually_constant_prod
-#align finset.eventually_constant_sum Finset.eventually_constant_sum
-
-@[to_additive]
-theorem prod_range_add (f : ℕ → β) (n m : ℕ) :
-    (∏ x ∈ range (n + m), f x) = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x) := by
-  induction' m with m hm
-  · simp
-  · erw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]
-#align finset.prod_range_add Finset.prod_range_add
-#align finset.sum_range_add Finset.sum_range_add
-
-@[to_additive]
-theorem prod_range_add_div_prod_range {α : Type*} [CommGroup α] (f : ℕ → α) (n m : ℕ) :
-    (∏ k ∈ range (n + m), f k) / ∏ k ∈ range n, f k = ∏ k ∈ Finset.range m, f (n + k) :=
-  div_eq_of_eq_mul' (prod_range_add f n m)
-#align finset.prod_range_add_div_prod_range Finset.prod_range_add_div_prod_range
-#align finset.sum_range_add_sub_sum_range Finset.sum_range_add_sub_sum_range
-
-@[to_additive]
-theorem prod_range_zero (f : ℕ → β) : ∏ k ∈ range 0, f k = 1 := by rw [range_zero, prod_empty]
-#align finset.prod_range_zero Finset.prod_range_zero
-#align finset.sum_range_zero Finset.sum_range_zero
-
-@[to_additive sum_range_one]
-theorem prod_range_one (f : ℕ → β) : ∏ k ∈ range 1, f k = f 0 := by
-  rw [range_one, prod_singleton]
-#align finset.prod_range_one Finset.prod_range_one
-#align finset.sum_range_one Finset.sum_range_one
-
 open List
 
 @[to_additive]
@@ -1674,68 +1603,6 @@ theorem prod_induction_nonempty {M : Type*} [CommMonoid M] (f : α → M) (p : M
 #align finset.prod_induction_nonempty Finset.prod_induction_nonempty
 #align finset.sum_induction_nonempty Finset.sum_induction_nonempty
 
-/-- For any product along `{0, ..., n - 1}` of a commutative-monoid-valued function, we can verify
-that it's equal to a different function just by checking ratios of adjacent terms.
-
-This is a multiplicative discrete analogue of the fundamental theorem of calculus. -/
-@[to_additive "For any sum along `{0, ..., n - 1}` of a commutative-monoid-valued function, we can
-verify that it's equal to a different function just by checking differences of adjacent terms.
-
-This is a discrete analogue of the fundamental theorem of calculus."]
-theorem prod_range_induction (f s : ℕ → β) (base : s 0 = 1)
-    (step : ∀ n, s (n + 1) = s n * f n) (n : ℕ) :
-    ∏ k ∈ Finset.range n, f k = s n := by
-  induction' n with k hk
-  · rw [Finset.prod_range_zero, base]
-  · simp only [hk, Finset.prod_range_succ, step, mul_comm]
-#align finset.prod_range_induction Finset.prod_range_induction
-#align finset.sum_range_induction Finset.sum_range_induction
-
-/-- A telescoping product along `{0, ..., n - 1}` of a commutative group valued function reduces to
-the ratio of the last and first factors. -/
-@[to_additive "A telescoping sum along `{0, ..., n - 1}` of an additive commutative group valued
-function reduces to the difference of the last and first terms."]
-theorem prod_range_div {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
-    (∏ i ∈ range n, f (i + 1) / f i) = f n / f 0 := by apply prod_range_induction <;> simp
-#align finset.prod_range_div Finset.prod_range_div
-#align finset.sum_range_sub Finset.sum_range_sub
-
-@[to_additive]
-theorem prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
-    (∏ i ∈ range n, f i / f (i + 1)) = f 0 / f n := by apply prod_range_induction <;> simp
-#align finset.prod_range_div' Finset.prod_range_div'
-#align finset.sum_range_sub' Finset.sum_range_sub'
-
-@[to_additive]
-theorem eq_prod_range_div {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
-    f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i := by rw [prod_range_div, mul_div_cancel]
-#align finset.eq_prod_range_div Finset.eq_prod_range_div
-#align finset.eq_sum_range_sub Finset.eq_sum_range_sub
-
-@[to_additive]
-theorem eq_prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
-    f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1) := by
-  conv_lhs => rw [Finset.eq_prod_range_div f]
-  simp [Finset.prod_range_succ', mul_comm]
-#align finset.eq_prod_range_div' Finset.eq_prod_range_div'
-#align finset.eq_sum_range_sub' Finset.eq_sum_range_sub'
-
-/-- A telescoping sum along `{0, ..., n-1}` of an `ℕ`-valued function
-reduces to the difference of the last and first terms
-when the function we are summing is monotone.
--/
-theorem sum_range_tsub [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α]
-    [ContravariantClass α α (· + ·) (· ≤ ·)] {f : ℕ → α} (h : Monotone f) (n : ℕ) :
-    ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0 := by
-  apply sum_range_induction
-  case base => apply tsub_self
-  case step =>
-    intro n
-    have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
-    have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
-    rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]
-#align finset.sum_range_tsub Finset.sum_range_tsub
-
 @[to_additive (attr := simp)]
 theorem prod_const (b : β) : ∏ _x ∈ s, b = b ^ s.card :=
   (congr_arg _ <| s.val.map_const b).trans <| Multiset.prod_replicate s.card b
@@ -1757,12 +1624,7 @@ theorem prod_mul_pow_card {b : β} : (∏ a ∈ s, f a) * b ^ s.card = ∏ a ∈
   (Finset.prod_const b).symm ▸ prod_mul_distrib.symm
 
 @[to_additive]
-theorem pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ _k ∈ range n, b := by simp
-#align finset.pow_eq_prod_const Finset.pow_eq_prod_const
-#align finset.nsmul_eq_sum_const Finset.nsmul_eq_sum_const
-
-@[to_additive]
-theorem prod_pow (s : Finset α) (n : ℕ) (f : α → β) : ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n :=
+theorem prod_pow (s : Finset α) (n : ℕ) (f : α → β) : ∏ x in s, f x ^ n = (∏ x in s, f x) ^ n :=
   Multiset.prod_map_pow
 #align finset.prod_pow Finset.prod_pow
 #align finset.sum_nsmul Finset.sum_nsmul
@@ -1780,16 +1642,6 @@ lemma prod_powersetCard (n : ℕ) (s : Finset α) (f : ℕ → β) :
     ∏ t ∈ powersetCard n s, f t.card = f n ^ s.card.choose n := by
   rw [prod_eq_pow_card, card_powersetCard]; rintro a ha; rw [(mem_powersetCard.1 ha).2]
 
-@[to_additive]
-theorem prod_flip {n : ℕ} (f : ℕ → β) :
-    (∏ r ∈ range (n + 1), f (n - r)) = ∏ k ∈ range (n + 1), f k := by
-  induction' n with n ih
-  · rw [prod_range_one, prod_range_one]
-  · rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
-    simp [← ih]
-#align finset.prod_flip Finset.prod_flip
-#align finset.sum_flip Finset.sum_flip
-
 @[to_additive]
 theorem prod_involution {s : Finset α} {f : α → β} :
     ∀ (g : ∀ a ∈ s, α) (_ : ∀ a ha, f a * f (g a ha) = 1) (_ : ∀ a ha, f a ≠ 1 → g a ha ≠ a)

Mathlib/Algebra/BigOperators/Fin.lean

@@ -29,10 +29,30 @@ open BigOperators
 
 open Finset
 
-variable {α : Type*} {β : Type*}
+variable {α β M : Type*}
+
+/-- It is equivalent to compute the product of a function over `Fin n` or `Finset.range n`. -/
+@[to_additive "It is equivalent to sum a function over `fin n` or `finset.range n`."]
+lemma Fin.prod_univ_eq_prod_range [CommMonoid M] (f : ℕ → M) (n : ℕ) :
+    ∏ i : Fin n, f i = ∏ i in range n, f i :=
+  calc
+    ∏ i : Fin n, f i = ∏ i : { x // x ∈ range n }, f i :=
+      Fintype.prod_equiv (Fin.equivSubtype.trans (Equiv.subtypeEquivRight (by simp))) _ _ (by simp)
+    _ = ∏ i in range n, f i := by rw [← attach_eq_univ, prod_attach]
+#align fin.prod_univ_eq_prod_range Fin.prod_univ_eq_prod_range
+#align fin.sum_univ_eq_sum_range Fin.sum_univ_eq_sum_range
 
 namespace Finset
 
+@[to_additive]
+lemma prod_fin_eq_prod_range [CommMonoid M] {n : ℕ} (f : Fin n → M) :
+    ∏ i, f i = ∏ i in range n, if h : i < n then f ⟨i, h⟩ else 1 := by
+  rw [← Fin.prod_univ_eq_prod_range, prod_congr rfl]
+  rintro ⟨i, hi⟩ _
+  simp only [hi, dif_pos]
+#align finset.prod_fin_eq_prod_range Finset.prod_fin_eq_prod_range
+#align finset.sum_fin_eq_sum_range Finset.sum_fin_eq_sum_range
+
 @[to_additive]
 theorem prod_range [CommMonoid β] {n : ℕ} (f : ℕ → β) :
     ∏ i in Finset.range n, f i = ∏ i : Fin n, f i :=

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -23,7 +23,7 @@ of elements of a list and `List.alternatingProd`, `List.alternatingSum`, their a
 counterparts.
 -/
 
--- Make sure we haven't imported `Data.Nat.Order.Basic`
+-- Make sure we haven't imported `Algebra.Order.Group.Nat`
 assert_not_exists OrderedSub
 assert_not_exists Ring
 
@@ -33,7 +33,6 @@ namespace List
 section Defs
 
 /-- Product of a list.
-
 `List.prod [a, b, c] = ((1 * a) * b) * c` -/
 @[to_additive "Sum of a list.\n\n`List.sum [a, b, c] = ((0 + a) + b) + c`"]
 def prod {α} [Mul α] [One α] : List α → α :=
@@ -661,7 +660,7 @@ theorem sum_map_count_dedup_filter_eq_countP (p : α → Bool) (l : List α) :
         | false => simp only
     · by_cases hp : p a
       · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h]) ?_
-        simp [hp, count_dedup]
+        simpa only [hp, count_filter, count_dedup, mem_cons, true_or, ↓reduceIte] using mul_one _
       · refine _root_.trans (List.sum_eq_zero fun n hn => ?_) (by simp [hp])
         obtain ⟨a', ha'⟩ := List.mem_map.1 hn
         split_ifs at ha' with ha