[Merged by Bors] - chore: bump to nightly-2023-07-15

Archive/Sensitivity.lean

@@ -103,8 +103,8 @@ theorem succ_n_eq (p q : Q n.succ) : p = q ↔ p 0 = q 0 ∧ π p = π q := by
     ext x
     by_cases hx : x = 0
     · rwa [hx]
-    · rw [← Fin.succ_pred x <| Fin.vne_of_ne hx]
-      convert congr_fun h (Fin.pred x <| Fin.vne_of_ne hx)
+    · rw [← Fin.succ_pred x hx]
+      convert congr_fun h (Fin.pred x hx)
 #align sensitivity.Q.succ_n_eq Sensitivity.Q.succ_n_eq
 
 /-- The adjacency relation defining the graph structure on `Q n`:
@@ -128,7 +128,7 @@ theorem adj_iff_proj_eq {p q : Q n.succ} (h₀ : p 0 ≠ q 0) : q ∈ p.adjacent
     use 0, h₀
     intro y hy
     contrapose! hy
-    rw [← Fin.succ_pred _ <| Fin.vne_of_ne hy]
+    rw [← Fin.succ_pred _ hy]
     apply congr_fun heq
 #align sensitivity.Q.adj_iff_proj_eq Sensitivity.Q.adj_iff_proj_eq
 
@@ -139,14 +139,14 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) :
   constructor
   · rintro ⟨i, h_eq, h_uni⟩
     have h_i : i ≠ 0 := fun h_i => absurd h₀ (by rwa [h_i] at h_eq )
-    use i.pred <| Fin.vne_of_ne h_i,
+    use i.pred h_i,
       show p (Fin.succ (Fin.pred i _)) ≠ q (Fin.succ (Fin.pred i _)) by rwa [Fin.succ_pred]
     intro y hy
     simp [Eq.symm (h_uni _ hy)]
   · rintro ⟨i, h_eq, h_uni⟩
     use i.succ, h_eq
     intro y hy
-    rw [← Fin.pred_inj (ha := Fin.vne_of_ne (?ha : y ≠ 0)) (hb := Fin.vne_of_ne (?hb : i.succ ≠ 0)),
+    rw [← Fin.pred_inj (ha := (?ha : y ≠ 0)) (hb := (?hb : i.succ ≠ 0)),
       Fin.pred_succ]
     case ha =>
       contrapose! hy
@@ -231,8 +231,8 @@ theorem epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 := by
   · dsimp [ε] at h; exact h fun _ => true
   · cases' v with v₁ v₂
     ext <;> change _ = (0 : V n) <;> simp only <;> apply ih <;> intro p <;>
-      [let q : Q n.succ := fun i => if h : i = 0 then true else p (i.pred <| Fin.vne_of_ne h);
-      let q : Q n.succ := fun i => if h : i = 0 then false else p (i.pred <| Fin.vne_of_ne h)]
+      [let q : Q n.succ := fun i => if h : i = 0 then true else p (i.pred h);
+      let q : Q n.succ := fun i => if h : i = 0 then false else p (i.pred h)]
     all_goals
       specialize h q
       first

Mathlib/Algebra/BigOperators/Fin.lean

@@ -353,7 +353,7 @@ theorem finFunctionFinEquiv_single {m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m
     (finFunctionFinEquiv (Pi.single i j) : ℕ) = j * m ^ (i : ℕ) := by
   rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
   rintro x hx
-  rw [Pi.single_eq_of_ne hx, Fin.val_zero, MulZeroClass.zero_mul]
+  rw [Pi.single_eq_of_ne hx, Fin.val_zero', MulZeroClass.zero_mul]
 #align fin_function_fin_equiv_single finFunctionFinEquiv_single
 
 /-- Equivalence between `∀ i : Fin m, Fin (n i)` and `Fin (∏ i : Fin m, n i)`. -/
@@ -437,7 +437,7 @@ theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)]
       j * ∏ j, n (Fin.castLE i.is_lt.le j) := by
   rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
   rintro x hx
-  rw [Pi.single_eq_of_ne hx, Fin.val_zero, MulZeroClass.zero_mul]
+  rw [Pi.single_eq_of_ne hx, Fin.val_zero', MulZeroClass.zero_mul]
 #align fin_pi_fin_equiv_single finPiFinEquiv_single
 
 namespace List

Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -108,7 +108,7 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     rintro ⟨i', j'⟩ hij'
     simp only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.compl_filter,
       not_le, Finset.mem_filter, true_and] at hij'
-    refine' ⟨(j'.pred <| Fin.vne_of_ne (j := 0) _, Fin.castSucc i'), _, _⟩
+    refine' ⟨(j'.pred <| _, Fin.castSucc i'), _, _⟩
     · rintro rfl
       simp only [Fin.val_zero, not_lt_zero'] at hij'
     · simpa only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.mem_filter,

Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

@@ -146,7 +146,7 @@ namespace StandardSimplex
 /-- When `[HasZero X]`, the shift of a map `f : Fin n → X`
 is a map `Fin (n+1) → X` which sends `0` to `0` and `i.succ` to `f i`. -/
 def shiftFun {n : ℕ} {X : Type _} [Zero X] (f : Fin n → X) (i : Fin (n + 1)) : X :=
-  dite (i = 0) (fun _ => 0) fun h => f (i.pred <| Fin.vne_of_ne h)
+  dite (i = 0) (fun _ => 0) fun h => f (i.pred h)
 set_option linter.uppercaseLean3 false in
 #align sSet.augmented.standard_simplex.shift_fun SSet.Augmented.StandardSimplex.shiftFun
 
@@ -267,7 +267,7 @@ noncomputable def ExtraDegeneracy.s (n : ℕ) :
     (fun i =>
       dite (i = 0)
         (fun _ => WidePullback.base _ ≫ S.section_)
-        (fun h => WidePullback.π _ (i.pred <| Fin.vne_of_ne h)))
+        (fun h => WidePullback.π _ (i.pred h)))
     fun i => by
       dsimp
       split_ifs with h

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -225,7 +225,7 @@ theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
 
 theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) :
     δ i ≫ δ j =
-      δ (j.pred <| Fin.vne_of_ne fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) ≫
+      δ (j.pred <| fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) ≫
         δ (Fin.castSucc i) := by
   rw [← δ_comp_δ]
   · rw [Fin.succ_pred]
@@ -325,7 +325,7 @@ theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSu
 @[reassoc]
 theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
     δ i ≫ σ j = σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le))) ≫
-      δ (i.pred <| Fin.vne_of_ne fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) := by
+      δ (i.pred <| fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) := by
   rw [← δ_comp_σ_of_gt]
   · simp
   · rw [Fin.castSucc_castLT, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
@@ -609,7 +609,7 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
     · rwa [eq, ← Fin.le_castSucc_iff]
     rw [eq]
   · simp only [not_le] at h'
-    let y := x.pred <| Fin.vne_of_ne (by rintro (rfl : x = 0); simp at h')
+    let y := x.pred <| by rintro (rfl : x = 0); simp at h'
     have hy : x = y.succ := (Fin.succ_pred x _).symm
     rw [hy] at h' ⊢
     rw [Fin.predAbove_above i y.succ h', Fin.pred_succ]

Mathlib/AlgebraicTopology/SimplicialObject.lean

@@ -115,7 +115,7 @@ theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
 theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) :
     X.δ j ≫ X.δ i =
       X.δ (Fin.castSucc i) ≫
-        X.δ (j.pred <| Fin.vne_of_ne fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) := by
+        X.δ (j.pred <| fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) := by
   dsimp [δ]
   simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]
 #align category_theory.simplicial_object.δ_comp_δ' CategoryTheory.SimplicialObject.δ_comp_δ'
@@ -189,7 +189,7 @@ theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSu
 @[reassoc]
 theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
     X.σ j ≫ X.δ i =
-      X.δ (i.pred <| Fin.vne_of_ne fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) ≫
+      X.δ (i.pred <| fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) ≫
         X.σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le))) := by
   dsimp [δ, σ]
   simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]
@@ -486,7 +486,7 @@ theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
 @[reassoc]
 theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) :
     X.δ i ≫ X.δ j =
-      X.δ (j.pred <| Fin.vne_of_ne fun (hj : j = 0) => by simp only [hj, Fin.not_lt_zero] at H) ≫
+      X.δ (j.pred <| fun (hj : j = 0) => by simp only [hj, Fin.not_lt_zero] at H) ≫
         X.δ (Fin.castSucc i) := by
   dsimp [δ]
   simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]
@@ -563,7 +563,7 @@ theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSu
 theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
     X.δ i ≫ X.σ j =
       X.σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le))) ≫
-        X.δ (i.pred <| Fin.vne_of_ne
+        X.δ (i.pred <|
           fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) := by
   dsimp [δ, σ]
   simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]

Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

@@ -151,7 +151,6 @@ noncomputable def preservesFinOfPreservesBinaryAndTerminal :
     · apply (Category.id_comp _).symm
     · rintro i _
       dsimp [extendFan_π_app, Iso.refl_hom, Fan.mk_π_app]
-      rw [Fin.cases_succ, Fin.cases_succ]
       change F.map _ ≫ _ = 𝟙 _ ≫ _
       simp only [id_comp, ← F.map_comp]
       rfl
@@ -295,7 +294,7 @@ noncomputable def preservesFinOfPreservesBinaryAndInitial :
     · apply Category.comp_id
     · rintro i _
       dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι_app]
-      rw [Fin.cases_succ, Fin.cases_succ, comp_id, ← F.map_comp]
+      rw [comp_id, ← F.map_comp]
 #align category_theory.preserves_fin_of_preserves_binary_and_initial CategoryTheory.preservesFinOfPreservesBinaryAndInitialₓ  -- Porting note: order of universes changed
 
 /-- If `F` preserves the initial object and binary coproducts, then it preserves colimits of shape

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -94,7 +94,7 @@ theorem IsAcyclic.path_unique {G : SimpleGraph V} (h : G.IsAcyclic) {v w : V} (p
     specialize h ph
     rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
     replace h := h.2 (q.append p.reverse)
-    simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse'] at h
+    simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h
     cases' h with h h
     · cases q with
       | nil => simp [Walk.isPath_def] at hp

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -1754,7 +1754,7 @@ theorem transfer_append (q : G.Walk v w) (hpq) :
 @[simp]
 theorem reverse_transfer (hp) :
     (p.transfer H hp).reverse =
-      p.reverse.transfer H (by simp only [edges_reverse, List.mem_reverse']; exact hp) := by
+      p.reverse.transfer H (by simp only [edges_reverse, List.mem_reverse]; exact hp) := by
   induction p with
   | nil => simp
   | cons _ _ ih => simp only [transfer_append, Walk.transfer, reverse_nil, reverse_cons, ih]
@@ -2486,7 +2486,7 @@ theorem reachable_deleteEdges_iff_exists_cycle.aux [DecidableEq V] {u v w : V}
   -- so they both contain the edge ⟦(v, w)⟧, but that's a contradiction since c is a trail.
   have hbq := hb (pvu.append puw)
   have hpq' := hb pwv.reverse
-  rw [Walk.edges_reverse, List.mem_reverse'] at hpq'
+  rw [Walk.edges_reverse, List.mem_reverse] at hpq'
   rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
     ← List.append_assoc, ← Walk.edges_append] at hc
   exact List.disjoint_of_nodup_append hc hbq hpq'