refactor(*): Use finset.Iix/finset.Ixi (#14448)

Now that `finset.Iix`/`finset.Ixi` work for empty types, there is no need for `univ.filter (λ j, j < i)` and similar.

src/algebra/big_operators/fin.lean

@@ -3,10 +3,10 @@ Copyright (c) 2020 Yury Kudryashov, Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Anne Baanen
 -/
-import algebra.big_operators.basic
-import data.fintype.fin
 import data.fintype.card
+import data.fintype.fin
 import logic.equiv.fin
+
 /-!
 # Big operators and `fin`
 
@@ -103,16 +103,14 @@ lemma prod_const [comm_monoid α] (n : ℕ) (x : α) : ∏ i : fin n, x = x ^ n
 
 lemma sum_const [add_comm_monoid α] (n : ℕ) (x : α) : ∑ i : fin n, x = n • x := by simp
 
-@[to_additive]
-lemma prod_filter_zero_lt {M : Type*} [comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
-  ∏ i in univ.filter (λ (i : fin n.succ), 0 < i), v i = ∏ (j : fin n), v j.succ :=
-by rw [univ_filter_zero_lt, finset.prod_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
+@[to_additive] lemma prod_Ioi_zero {M : Type*} [comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
+  ∏ i in Ioi 0, v i = ∏ j : fin n, v j.succ :=
+by rw [Ioi_zero_eq_map, finset.prod_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
 
 @[to_additive]
-lemma prod_filter_succ_lt {M : Type*} [comm_monoid M] {n : ℕ} (j : fin n) (v : fin n.succ → M) :
-  ∏ i in univ.filter (λ i, j.succ < i), v i =
-    ∏ j in univ.filter (λ i, j < i), v j.succ :=
-by rw [univ_filter_succ_lt, finset.prod_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
+lemma prod_Ioi_succ {M : Type*} [comm_monoid M] {n : ℕ} (i : fin n) (v : fin n.succ → M) :
+  ∏ j in Ioi i.succ, v j = ∏ j in Ioi i, v j.succ :=
+by rw [Ioi_succ, finset.prod_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
 
 @[to_additive]
 lemma prod_congr' {M : Type*} [comm_monoid M] {a b : ℕ} (f : fin b → M) (h : a = b) :

src/data/fin/interval.lean

@@ -26,8 +26,6 @@ instance : Π n, locally_finite_order_top (fin n)
 | (n + 1) := infer_instance
 
 namespace fin
-
-section bounded
 variables {n} (a b : fin n)
 
 lemma Icc_eq_finset_subtype : Icc a b = (Icc (a : ℕ) b).subtype (λ x, x < n) := rfl
@@ -134,58 +132,4 @@ by rw [fintype.card_of_finset, card_Iic]
 @[simp] lemma card_fintype_Iio : fintype.card (set.Iio b) = b :=
 by rw [fintype.card_of_finset, card_Iio]
 
-end bounded
-
-section filter
-
-variables {n} (a b : fin n)
-
-@[simp]
-lemma card_filter_lt : (finset.univ.filter (λ j, a < j)).card = n - a - 1 :=
-by rw [filter_lt_eq_Ioi, card_Ioi, tsub_right_comm]
-
-@[simp]
-lemma card_filter_le : (univ.filter $ λ j, a ≤ j).card = n - a := by rw [filter_le_eq_Ici, card_Ici]
-
-@[simp]
-lemma card_filter_gt : (univ.filter $ λ j, j < a).card = a := by rw [filter_gt_eq_Iio, card_Iio]
-
-@[simp]
-lemma card_filter_ge : (univ.filter $ λ j, j ≤ a).card = a + 1 := by rw [filter_ge_eq_Iic, card_Iic]
-
-@[simp]
-lemma card_filter_lt_lt : (univ.filter (λ j, a < j ∧ j < b)).card = b - a - 1 :=
-by rw [filter_lt_lt_eq_Ioo, card_Ioo]
-
-@[simp]
-lemma card_filter_lt_le : (finset.univ.filter (λ j, a < j ∧ j ≤ b)).card = b - a :=
-by rw [filter_lt_le_eq_Ioc, card_Ioc]
-
-@[simp]
-lemma card_filter_le_lt : (finset.univ.filter (λ j, a ≤ j ∧ j < b)).card = b - a :=
-by rw [filter_le_lt_eq_Ico, card_Ico]
-
-@[simp]
-lemma card_filter_le_le : (finset.univ.filter (λ j, a ≤ j ∧ j ≤ b)).card = b + 1 - a :=
-by rw [filter_le_le_eq_Icc, card_Icc]
-
-lemma prod_filter_lt_mul_neg_eq_prod_off_diag {R : Type*} [comm_monoid R] {n : ℕ}
-  {f : fin n → fin n → R} :
-  ∏ i, (∏ j in univ.filter (λ j, i < j), (f j i) * (f i j)) =
-  ∏ i, (∏ j in univ.filter (λ j, i ≠ j), (f j i)) :=
-begin
-  simp_rw [ne_iff_lt_or_gt, or.comm, filter_or, prod_mul_distrib],
-  have : ∀ i : fin n, disjoint (filter (gt i) univ) (filter (has_lt.lt i) univ),
-  { simp_rw disjoint_filter,
-    intros i x y,
-    apply lt_asymm },
-  simp only [prod_union, this, prod_mul_distrib],
-  rw mul_comm,
-  congr' 1,
-  rw [prod_sigma', prod_sigma'],
-  refine prod_bij' (λ i hi, ⟨i.2, i.1⟩) _ _ (λ i hi, ⟨i.2, i.1⟩) _ _ _; simp
-end
-
-end filter
-
 end fin

src/data/finset/basic.lean

@@ -2453,7 +2453,7 @@ end bUnion
 section disjoint
 variables [decidable_eq α] [decidable_eq β] {f : α → β} {s t u : finset α} {a b : α}
 
-lemma disjoint_left : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
+lemma disjoint_left : disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t :=
 by simp only [_root_.disjoint, inf_eq_inter, le_iff_subset, subset_iff, mem_inter, not_and,
   and_imp]; refl
 
@@ -2463,7 +2463,7 @@ lemma disjoint_iff_inter_eq_empty : disjoint s t ↔ s ∩ t = ∅ := disjoint_i
 instance decidable_disjoint (U V : finset α) : decidable (disjoint U V) :=
 decidable_of_decidable_of_iff (by apply_instance) eq_bot_iff
 
-lemma disjoint_right : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s := by rw [disjoint.comm, disjoint_left]
+lemma disjoint_right : disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s := by rw [disjoint.comm, disjoint_left]
 lemma disjoint_iff_ne : disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b :=
 by simp only [disjoint_left, imp_not_comm, forall_eq']
 

src/data/finset/card.lean

@@ -305,7 +305,7 @@ lemma card_union_le (s t : finset α) : (s ∪ t).card ≤ s.card + t.card :=
 card_union_add_card_inter s t ▸ nat.le_add_right _ _
 
 lemma card_union_eq (h : disjoint s t) : (s ∪ t).card = s.card + t.card :=
-by rw [←disj_union_eq_union s t $ λ x, disjoint_left.mp h, card_disj_union _ _ _]
+by rw [←disj_union_eq_union s t $ disjoint_left.mp h, card_disj_union _ _ _]
 
 @[simp] lemma card_disjoint_union (h : disjoint s t) : card (s ∪ t) = s.card + t.card :=
 card_union_eq h

src/data/finset/locally_finite.lean

@@ -16,9 +16,15 @@ This file provides basic results about all the `finset.Ixx`, which are defined i
 This file was originally only about `finset.Ico a b` where `a b : ℕ`. No care has yet been taken to
 generalize these lemmas properly and many lemmas about `Icc`, `Ioc`, `Ioo` are missing. In general,
 what's to do is taking the lemmas in `data.x.intervals` and abstract away the concrete structure.
+
+Complete the API. See
+https://github.com/leanprover-community/mathlib/pull/14448#discussion_r906109235
+for some ideas.
 -/
 
-variables {α : Type*}
+open_locale big_operators
+
+variables {ι α : Type*}
 
 namespace finset
 section preorder
@@ -255,6 +261,12 @@ lemma filter_gt_eq_Iio [decidable_pred (< a)] : univ.filter (< a) = Iio a := by
 lemma filter_ge_eq_Iic [decidable_pred (≤ a)] : univ.filter (≤ a) = Iic a := by { ext, simp }
 
 end locally_finite_order_bot
+
+variables [decidable_eq α] [locally_finite_order_top α] [locally_finite_order_bot α]
+
+lemma disjoint_Ioi_Iio (a : α) :  disjoint (Ioi a) (Iio a) :=
+disjoint_left.2 $ λ b hab hba, (mem_Ioi.1 hab).not_lt $ mem_Iio.1 hba
+
 end preorder
 
 section partial_order
@@ -377,7 +389,11 @@ end order_bot
 end partial_order
 
 section linear_order
-variables [linear_order α] [locally_finite_order α] {a b : α}
+variables [linear_order α]
+
+
+section locally_finite_order
+variables [locally_finite_order α] {a b : α}
 
 lemma Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
   Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
@@ -438,6 +454,14 @@ begin
     exact and_congr_right' ⟨λ hx, hx.2 hx.1, λ hx, ⟨hx.trans_le h, λ _, hx⟩⟩ }
 end
 
+end locally_finite_order
+
+variables [fintype α] [locally_finite_order_top α] [locally_finite_order_bot α]
+
+lemma Ioi_disj_union_Iio (a : α) :
+  (Ioi a).disj_union (Iio a) (disjoint_left.1 $ disjoint_Ioi_Iio a) = ({a} : finset α)ᶜ :=
+by { ext, simp [eq_comm] }
+
 end linear_order
 
 section ordered_cancel_add_comm_monoid
@@ -515,4 +539,15 @@ lemma image_add_right_Ioo (a b c : α) : (Ioo a b).image (+ c) = Ioo (a + c) (b
 by { simp_rw add_comm _ c, exact image_add_left_Ioo a b c }
 
 end ordered_cancel_add_comm_monoid
+
+@[to_additive] lemma prod_prod_Ioi_mul_eq_prod_prod_off_diag [fintype ι] [linear_order ι]
+  [locally_finite_order_top ι] [locally_finite_order_bot ι] [comm_monoid α] (f : ι → ι → α) :
+  ∏ i, ∏ j in Ioi i, f j i * f i j = ∏ i, ∏ j in {i}ᶜ, f j i :=
+begin
+  simp_rw [←Ioi_disj_union_Iio, prod_disj_union, prod_mul_distrib],
+  congr' 1,
+  rw [prod_sigma', prod_sigma'],
+  refine prod_bij' (λ i hi, ⟨i.2, i.1⟩) _ _ (λ i hi, ⟨i.2, i.1⟩) _ _ _; simp,
+end
+
 end finset

src/data/fintype/fin.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import data.fin.basic
-import data.fintype.basic
+import data.fin.interval
+
 /-!
 # The structure of `fintype (fin n)`
 
@@ -18,14 +18,11 @@ open fintype
 
 namespace fin
 
-@[simp]
-lemma univ_filter_zero_lt {n : ℕ} :
-  (univ : finset (fin n.succ)).filter (λ i, 0 < i) =
-    univ.map (fin.succ_embedding _).to_embedding :=
+@[simp] lemma Ioi_zero_eq_map {n : ℕ} :
+  Ioi (0 : fin n.succ) = univ.map (fin.succ_embedding _).to_embedding :=
 begin
   ext i,
-  simp only [mem_filter, mem_map, mem_univ, true_and,
-  function.embedding.coe_fn_mk, exists_true_left],
+  simp only [mem_Ioi, mem_map, mem_univ, function.embedding.coe_fn_mk, exists_true_left],
   split,
   { refine cases _ _ i,
     { rintro ⟨⟨⟩⟩ },
@@ -34,13 +31,11 @@ begin
     exact succ_pos _ },
 end
 
-@[simp]
-lemma univ_filter_succ_lt {n : ℕ} (j : fin n) :
-  (univ : finset (fin n.succ)).filter (λ i, j.succ < i) =
-    (univ.filter (λ i, j < i)).map (fin.succ_embedding _).to_embedding :=
+@[simp] lemma Ioi_succ {n : ℕ} (i : fin n) :
+  Ioi i.succ = (Ioi i).map (fin.succ_embedding _).to_embedding :=
 begin
   ext i,
-  simp only [mem_filter, mem_map, mem_univ, true_and,
+  simp only [mem_filter, mem_Ioi, mem_map, mem_univ, true_and,
   function.embedding.coe_fn_mk, exists_true_left],
   split,
   { refine cases _ _ i,

src/linear_algebra/vandermonde.lean

@@ -8,7 +8,6 @@ import algebra.big_operators.fin
 import algebra.geom_sum
 import group_theory.perm.fin
 import linear_algebra.matrix.determinant
-import tactic.ring_exp
 
 /-!
 # Vandermonde matrix
@@ -27,10 +26,8 @@ This file defines the `vandermonde` matrix and gives its determinant.
 
 variables {R : Type*} [comm_ring R]
 
-open_locale big_operators
-open_locale matrix
-
-open equiv
+open equiv finset
+open_locale big_operators matrix
 
 namespace matrix
 
@@ -71,7 +68,7 @@ lemma vandermonde_transpose_mul_vandermonde {n : ℕ} (v : fin n → R) (i j) :
 by simp only [vandermonde_apply, matrix.mul_apply, matrix.transpose_apply, pow_add]
 
 lemma det_vandermonde {n : ℕ} (v : fin n → R) :
-  det (vandermonde v) = ∏ i : fin n, ∏ j in finset.univ.filter (λ j, i < j), (v j - v i) :=
+  det (vandermonde v) = ∏ i : fin n, ∏ j in Ioi i, (v j - v i) :=
 begin
   unfold vandermonde,
 
@@ -99,9 +96,8 @@ begin
     det_mul_column (λ i, v (fin.succ i) - v 0) _
   ... = (∏ (i : fin n), (v (fin.succ i) - v 0)) * det (λ (i j : fin n), v (fin.succ i) ^ (j : ℕ)) :
     congr_arg ((*) _) _
-  ... = ∏ i : fin n.succ, ∏ j in finset.univ.filter (λ j, i < j), (v j - v i) :
-    by { simp_rw [ih (v ∘ fin.succ), fin.prod_univ_succ, fin.prod_filter_zero_lt,
-                  fin.prod_filter_succ_lt] },
+  ... = ∏ i : fin n.succ, ∏ j in Ioi i, (v j - v i) :
+    by simp_rw [ih (v ∘ fin.succ), fin.prod_univ_succ, fin.prod_Ioi_zero, fin.prod_Ioi_succ],
   { intros i j,
     rw fin.cons_zero,
     refine fin.cases _ (λ i, _) i,
@@ -127,7 +123,7 @@ lemma det_vandermonde_eq_zero_iff [is_domain R] {n : ℕ} {v : fin n → R} :
 begin
   split,
   { simp only [det_vandermonde v, finset.prod_eq_zero_iff, sub_eq_zero, forall_exists_index],
-    exact λ i _ j h₁ h₂, ⟨j, i, h₂, (finset.mem_filter.mp h₁).2.ne'⟩ },
+    exact λ i _ j h₁ h₂, ⟨j, i, h₂, (mem_Ioi.mp h₁).ne'⟩ },
   { simp only [ne.def, forall_exists_index, and_imp],
     refine λ i j h₁ h₂, matrix.det_zero_of_row_eq h₂ (funext $ λ k, _),
     rw [vandermonde_apply, vandermonde_apply, h₁], }

src/ring_theory/discriminant.lean

@@ -152,7 +152,7 @@ by rw [discr_def, ring_hom.map_det, ring_hom.map_matrix_apply,
 /-- The discriminant of a power basis. -/
 lemma discr_power_basis_eq_prod (e : fin pb.dim ≃ (L →ₐ[K] E)) [is_separable K L] :
   algebra_map K E (discr K pb.basis) =
-  ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j), (e j pb.gen- (e i pb.gen)) ^ 2 :=
+  ∏ i : fin pb.dim, ∏ j in Ioi i, (e j pb.gen- (e i pb.gen)) ^ 2 :=
 begin
   rw [discr_eq_det_embeddings_matrix_reindex_pow_two K E pb.basis e,
     embeddings_matrix_reindex_eq_vandermonde, det_transpose, det_vandermonde, ← prod_pow],
@@ -163,8 +163,7 @@ end
 /-- A variation of `of_power_basis_eq_prod`. -/
 lemma discr_power_basis_eq_prod' [is_separable K L] (e : fin pb.dim ≃ (L →ₐ[K] E)) :
   algebra_map K E (discr K pb.basis) =
-  ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
-  -((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen))) :=
+  ∏ i : fin pb.dim, ∏ j in Ioi i, -((e j pb.gen - e i pb.gen) * (e i pb.gen - e j pb.gen)) :=
 begin
   rw [discr_power_basis_eq_prod _ _ _ e],
   congr, ext i, congr, ext j,
@@ -176,20 +175,19 @@ local notation `n` := finrank K L
 /-- A variation of `of_power_basis_eq_prod`. -/
 lemma discr_power_basis_eq_prod'' [is_separable K L] (e : fin pb.dim ≃ (L →ₐ[K] E)) :
   algebra_map K E (discr K pb.basis) =
-  (-1) ^ (n * (n - 1) / 2) * ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
-  ((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen))) :=
+  (-1) ^ (n * (n - 1) / 2) * ∏ i : fin pb.dim, ∏ j in Ioi i,
+    (e j pb.gen - e i pb.gen) * (e i pb.gen - e j pb.gen) :=
 begin
   rw [discr_power_basis_eq_prod' _ _ _ e],
   simp_rw [λ i j, neg_eq_neg_one_mul ((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen))),
     prod_mul_distrib],
   congr,
   simp only [prod_pow_eq_pow_sum, prod_const],
   congr,
-  simp_rw [fin.card_filter_lt],
   apply (@nat.cast_inj ℚ _ _ _ _ _).1,
   rw [nat.cast_sum],
   have : ∀ (x : fin pb.dim), (↑x + 1) ≤ pb.dim := by simp [nat.succ_le_iff, fin.is_lt],
-  simp_rw [nat.sub_sub],
+  simp_rw [fin.card_Ioi, nat.sub_sub, add_comm 1],
   simp only [nat.cast_sub, this, finset.card_fin, nsmul_eq_mul, sum_const, sum_sub_distrib,
     nat.cast_add, nat.cast_one, sum_add_distrib, mul_one],
   rw [← nat.cast_sum, ← @finset.sum_range ℕ _ pb.dim (λ i, i), sum_range_id ],
@@ -228,7 +226,7 @@ begin
   rw [ring_hom.map_mul, ring_hom.map_pow, ring_hom.map_neg, ring_hom.map_one,
     discr_power_basis_eq_prod'' _ _ _ e],
   congr,
-  rw [norm_eq_prod_embeddings, fin.prod_filter_lt_mul_neg_eq_prod_off_diag],
+  rw [norm_eq_prod_embeddings, prod_prod_Ioi_mul_eq_prod_prod_off_diag],
   conv_rhs { congr, skip, funext,
     rw [← aeval_alg_hom_apply, aeval_root_derivative_of_splits (minpoly.monic
       (is_separable.is_integral K pb.gen)) (is_alg_closed.splits_codomain _) (hroots σ),
@@ -239,16 +237,15 @@ begin
   { simp only [true_and, finset.mem_mk, mem_univ, mem_sigma],
     rw [multiset.mem_erase_of_ne (λ h, _)],
     { exact hroots _ },
-    { simp only [true_and, mem_filter, mem_univ, ne.def, mem_sigma] at hi,
-      refine hi (equiv.injective e (equiv.injective (power_basis.lift_equiv pb) _)),
+    { simp only [true_and, mem_univ, ne.def, mem_sigma, mem_compl, mem_singleton] at hi,
       rw [← power_basis.lift_equiv_apply_coe, ← power_basis.lift_equiv_apply_coe] at h,
-      exact subtype.eq h } },
+      exact hi (e.injective $ pb.lift_equiv.injective $ subtype.eq h.symm) } },
   { simp only [equiv.apply_eq_iff_eq, heq_iff_eq] at hij,
     have h := hij.2,
     rw [← power_basis.lift_equiv_apply_coe, ← power_basis.lift_equiv_apply_coe] at h,
     refine sigma.eq (equiv.injective e (equiv.injective _ (subtype.eq h))) (by simp [hij.1]) },
-  { simp only [true_and, finset.mem_mk, mem_univ, mem_sigma] at hσ,
-    simp only [sigma.exists, true_and, exists_prop, mem_filter, mem_univ, ne.def, mem_sigma],
+  { simp only [true_and, finset.mem_mk, mem_univ, mem_sigma] at ⊢ hσ,
+    simp only [sigma.exists, exists_prop, mem_compl, mem_singleton, ne.def],
     refine ⟨e.symm (power_basis.lift pb σ.2 _), e.symm σ.1, ⟨λ h, _, sigma.eq _ _⟩⟩,
     { rw [aeval_def, eval₂_eq_eval_map, ← is_root.def, ← mem_roots],
       { exact multiset.erase_subset _ _ hσ },

src/ring_theory/trace.lean

@@ -514,7 +514,7 @@ begin
   refine mt mul_self_eq_zero.mp _,
   { simp only [det_vandermonde, finset.prod_eq_zero_iff, not_exists, sub_eq_zero],
     intros i _ j hij h,
-    exact (finset.mem_filter.mp hij).2.ne' (e.injective $ pb.alg_hom_ext h) },
+    exact (finset.mem_Ioi.mp hij).ne' (e.injective $ pb.alg_hom_ext h) },
   { rw [alg_hom.card, pb.finrank] }
 end