Update lean-toolchain for leanprover/lean4#14298

Author: leanprover-community-mathlib4-bot

Archive/Hairer.lean

@@ -93,6 +93,7 @@ def L : MvPolynomial ι ℝ →ₗ[ℝ]
     (fun p f₁ f₂ ↦ by simp_rw [smul_eq_mul, ← integral_add (int p _) (int p _), ← mul_add]; rfl)
     fun r p f ↦ by simp_rw [← integral_smul, smul_comm r]; rfl
 
+set_option backward.isDefEq.respectTransparency.types false in
 lemma inj_L : Injective (L ι) :=
   (injective_iff_map_eq_zero _).mpr fun p hp ↦ by
     have H : ∀ᵐ x : EuclideanSpace ℝ ι, x ∈ ball 0 1 → eval x p = 0 :=

Archive/Imo/Imo1987Q1.lean

@@ -31,6 +31,7 @@ open Finset (range sum_const)
 
 namespace Imo1987Q1
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The set of pairs `(x : α, σ : Perm α)` such that `σ x = x` is equivalent to the set of pairs
 `(x : α, σ : Perm {x}ᶜ)`. -/
 def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x : α, Perm ({x}ᶜ : Set α) :=
@@ -41,6 +42,7 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x :
       (sigmaCongrRight fun x => Equiv.setCongr <| by simp only [SetCoe.forall]; simp)
     _ ≃ Σ x : α, Perm ({x}ᶜ : Set α) := sigmaCongrRight fun x => by apply Equiv.Set.compl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem card_fixed_points :
     card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! := by
   simp only [card_congr (fixedPointsEquiv α), card_sigma, card_perm]

Archive/Imo/Imo2013Q1.lean

@@ -39,6 +39,8 @@ theorem prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :
 end Imo2013Q1
 
 open Imo2013Q1
+
+set_option backward.isDefEq.respectTransparency.types false in
 theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
     ∃ m : ℕ → ℕ+, (1 : ℚ) + (2 ^ k - 1) / n = ∏ i ∈ Finset.range k, (1 + 1 / (m i : ℚ)) := by
   induction k generalizing n with

Archive/Imo/Imo2024Q5.lean

@@ -128,6 +128,7 @@ def MonsterData.reflect (m : MonsterData N) : MonsterData N where
   toFun := Fin.rev ∘ m
   inj' := fun i j hij ↦ by simpa using hij
 
+set_option backward.isDefEq.respectTransparency false in
 lemma MonsterData.reflect_reflect (m : MonsterData N) : m.reflect.reflect = m := by
   ext i
   simp [MonsterData.reflect]
@@ -149,7 +150,7 @@ lemma MonsterData.mk_mem_monsterCells_iff_of_le {m : MonsterData N} {r : Fin (N
   simp only [monsterCells, Set.mem_range, Prod.mk.injEq]
   refine ⟨?_, ?_⟩
   · rintro ⟨r', rfl, rfl⟩
-    simp only [Subtype.coe_eta]
+    simp only
   · rintro rfl
     exact ⟨⟨r, hr1, hrN⟩, rfl, rfl⟩
 
@@ -449,6 +450,7 @@ def Path.reflect (p : Path N) : Path N where
     simp_rw [Adjacent, Nat.dist, Cell.reflect, Fin.rev] at h ⊢
     lia
 
+set_option backward.isDefEq.respectTransparency false in
 lemma Path.firstMonster_reflect (p : Path N) (m : MonsterData N) :
     p.reflect.firstMonster m.reflect = (p.firstMonster m).map Cell.reflect := by
   simp_rw [firstMonster, reflect, List.find?_map]
@@ -524,6 +526,7 @@ lemma Strategy.ForcesWinIn.mono (s : Strategy N) {k₁ k₂ : ℕ} (h : s.Forces
 
 /-! ### Proof of lower bound with constructions used therein -/
 
+set_option backward.isDefEq.respectTransparency false in
 /-- An arbitrary choice of monster positions, which is modified to put selected monsters in
 desired places. -/
 def baseMonsterData (N : ℕ) : MonsterData N where
@@ -539,6 +542,7 @@ def baseMonsterData (N : ℕ) : MonsterData N where
 def monsterData12 (hN : 2 ≤ N) (c₁ c₂ : Fin (N + 1)) : MonsterData N :=
   ((baseMonsterData N).setValue (row2 hN) c₂).setValue (row1 hN) c₁
 
+set_option backward.isDefEq.respectTransparency false in
 lemma monsterData12_apply_row2 (hN : 2 ≤ N) {c₁ c₂ : Fin (N + 1)} (h : c₁ ≠ c₂) :
     monsterData12 hN c₁ c₂ (row2 hN) = c₂ := by
   rw [monsterData12, Function.Embedding.setValue_eq_of_ne]
@@ -729,6 +733,7 @@ def winningStrategy (hN : 2 ≤ N) : Strategy N
   | 1 => fun r => path1 hN ((r 0).getD 0).2
   | _ + 2 => fun r => path2 hN ((r 0).getD 0).2 ((r 1).getD 0).1
 
+set_option backward.isDefEq.respectTransparency false in
 lemma path0_firstMonster_eq_apply_row1 (hN : 2 ≤ N) (m : MonsterData N) :
     (path0 hN).firstMonster m = some (1, m (row1 hN)) := by
   simp_rw [path0, Path.firstMonster, Path.ofFn]
@@ -958,6 +963,7 @@ lemma winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero (hN : 2
   exact path2OfEdge0_firstMonster_eq_none_of_path1OfEdge0_firstMonster_eq_some hN hx2N.1
     hx2N.2 hc₁0 hx.symm
 
+set_option backward.isDefEq.respectTransparency false in
 lemma winningStrategy_play_one_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
     (hc₁N : (m (row1 hN) : ℕ) = N) : (winningStrategy hN).play m 3 ⟨1, by simp⟩ =
       ((winningStrategy hN).play m.reflect 3 ⟨1, by simp⟩).map Cell.reflect := by
@@ -972,6 +978,7 @@ lemma winningStrategy_play_one_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
   simp_rw [winningStrategy_play_one hN, path1, path1OfEdgeN, dif_neg hc₁0, if_pos hc₁N,
     dif_pos hc₁r0, ← Path.firstMonster_reflect, MonsterData.reflect_reflect]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma winningStrategy_play_two_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
     (hc₁N : (m (row1 hN) : ℕ) = N) : (winningStrategy hN).play m 3 ⟨2, by simp⟩ =
       ((winningStrategy hN).play m.reflect 3 ⟨2, by simp⟩).map Cell.reflect := by
@@ -994,6 +1001,7 @@ lemma winningStrategy_play_two_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
   · rcases h with ⟨x, hx⟩
     simp [hx, Cell.reflect]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_N (hN : 2 ≤ N)
     {m : MonsterData N} (hc₁N : (m (row1 hN) : ℕ) = N) :
     (winningStrategy hN).play m 3 ⟨1, by simp⟩ = none ∨

Archive/Sensitivity.lean

@@ -407,6 +407,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   rw [Set.toFinset_card] at hH
   linarith
 
+set_option backward.isDefEq.respectTransparency false in
 open Classical in
 /-- **Huang sensitivity theorem** also known as the **Huang degree theorem** -/
 theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -173,6 +173,7 @@ theorem isRegularOf_not_existsPolitician (hG' : ¬ExistsPolitician G) :
 
 open scoped Classical in
 include hG in
+set_option backward.isDefEq.respectTransparency.types false in
 /-- Let `A` be the adjacency matrix of a `d`-regular friendship graph, and let `v` be a vector
   all of whose components are `1`. Then `v` is an eigenvector of `A ^ 2`, and we can compute
   the eigenvalue to be `d * d`, or as `d + (Fintype.card V - 1)`, so those quantities must be equal.

Archive/Wiedijk100Theorems/Konigsberg.lean

@@ -17,6 +17,7 @@ between them has no Eulerian trail.
 
 namespace Konigsberg
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- The vertices for the Königsberg graph; four vertices for the bodies of land and seven
 vertices for the bridges. -/
 inductive Verts : Type

Archive/ZagierTwoSquares.lean

@@ -113,6 +113,7 @@ def complexInvo : Function.End (zagierSet k) := fun ⟨⟨x, y, z⟩, h⟩ =>
 
 variable [hk : Fact (4 * k + 1).Prime]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `complexInvo k` is indeed an involution. -/
 theorem complexInvo_sq : complexInvo k ^ 2 = 1 := by
   change complexInvo k ∘ complexInvo k = id
@@ -139,6 +140,7 @@ theorem complexInvo_sq : complexInvo k ^ 2 = 1 := by
       ← Nat.add_sub_assoc less, ← add_assoc, Nat.sub_add_cancel more, Nat.sub_sub _ _ y,
       ← two_mul, add_comm, Nat.add_sub_cancel]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Any fixed point of `complexInvo k` must be `(1, 1, k)`. -/
 theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (complexInvo k)) :
     t.val = (1, 1, k) := by
@@ -169,6 +171,7 @@ theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (comple
 def singletonFixedPoint : Finset (zagierSet k) :=
   {⟨(1, 1, k), (by simp only [zagierSet, Set.mem_setOf_eq]; linarith)⟩}
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `complexInvo k` has exactly one fixed point. -/
 theorem card_fixedPoints_eq_one : Fintype.card (fixedPoints (complexInvo k)) = 1 := by
   rw [show 1 = Finset.card (singletonFixedPoint k) by rfl, ← Set.toFinset_card]

Counterexamples/AharoniKorman.lean

@@ -205,6 +205,7 @@ lemma induction_on_level {n : ℕ} {p : (x : Hollom) → x ∈ level n → Prop}
   rintro x y _ rfl
   exact h _ _
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 For each `n`, there is an order embedding from ℕ × ℕ (which has the product order) to the Hollom
 partial order.
@@ -218,6 +219,7 @@ lemma embed_apply (n : ℕ) (x y : ℕ) : embed n (x, y) = h(x, y, n) := rfl
 
 lemma embed_strictMono {n : ℕ} : StrictMono (embed n) := (embed n).strictMono
 
+set_option backward.isDefEq.respectTransparency false in
 lemma level_eq_range (n : ℕ) : level n = Set.range (embed n) := by
   simp [level, Set.range, embed]
 
@@ -812,6 +814,7 @@ variable {n : ℕ}
 
 lemma R_subset_level : R n C ⊆ level n := Set.sep_subset (level n) _
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 A helper lemma to show `square_subset_R`.  In particular shows that if `C ∩ level n` is finite, the
 set of points `x` such that `x` is at least as large as every element of `C ∩ level n` contains an
@@ -853,6 +856,7 @@ lemma square_subset_above (h : (C ∩ level n).Finite) :
     specialize hab _ _ hfg
     lia
 
+set_option backward.isDefEq.respectTransparency false in
 lemma square_subset_R (h : (C ∩ level n).Finite) :
     ∀ᶠ a in atTop, embed n '' Set.Ici (a, a) ⊆ R n C \ (C ∩ level n) := by
   filter_upwards [square_subset_above h] with a ha
@@ -935,6 +939,7 @@ lemma S_subset_R : S n C ⊆ R n C := by
 
 lemma S_subset_level : S n C ⊆ level n := S_subset_R.trans R_subset_level
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 Assuming `C ∩ level n` is finite, and `C ∩ level (n + 1)` is finite, that there exists cofinitely
 many `a` such that `{(x, y, n) | x ≥ a ∧ y ≥ a} ⊆ S \ (C ∩ level n)`.

Counterexamples/MapFloor.lean

@@ -59,6 +59,7 @@ instance isOrderedAddMonoid : IsOrderedAddMonoid ℤ[ε] :=
   Function.Injective.isOrderedAddMonoid
     (toLex ∘ coeff) (fun _ _ => funext fun _ => coeff_add _ _ _) .rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem pos_iff {p : ℤ[ε]} : 0 < p ↔ 0 < p.trailingCoeff := by
   rw [trailingCoeff]
   refine
@@ -118,6 +119,7 @@ theorem forgetEpsilons_floor_lt (n : ℤ) :
   exact (if_neg <| by rw [coeff_sub, intCast_coeff_zero]; simp [this]).trans (by
     rw [coeff_sub, intCast_coeff_zero]; simp)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The ceil of `n + ε` is `n + 1` but its image under `forgetEpsilons` is `n`, whose ceil is
 itself. -/
 theorem lt_forgetEpsilons_ceil (n : ℤ) :