chore: adaptations for nightly-2026-02-16-rev1

Author: kim-em

Archive/Examples/Eisenstein.lean

@@ -25,6 +25,7 @@ namespace Polynomial
 
 open Ideal.Quotient Ideal RingHom
 
+set_option backward.isDefEq.respectTransparency false in
 set_option linter.flexible false in
 example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
   -- We will apply the generalized Eisenstein criterion with `q = X ^ 2 + 1` and `K = ZMod 3`.

Archive/Examples/Kuratowski.lean

@@ -173,6 +173,7 @@ theorem k_Icc_4_5_inter_rat : k (Icc (4 : ℝ) 5 ∩ range Rat.cast) = Icc 4 5 :
   (closure_ordConnected_inter_rat ordConnected_Icc ⟨4, by norm_num, 5, by norm_num⟩).trans
     isClosed_Icc.closure_eq
 
+set_option backward.isDefEq.respectTransparency false in
 theorem i_fourteenSet : i fourteenSet = Ioo 0 1 ∪ Ioo 1 2 := by
   have := interior_eq_empty_iff_dense_compl.mpr dense_irrational
   rw [fourteenSet, interior_union_of_disjoint_closure, interior_union_of_disjoint_closure]
@@ -189,6 +190,7 @@ theorem k_fourteenSet : k fourteenSet = Icc 0 2 ∪ {3} ∪ Icc 4 5 := by
 theorem kc_fourteenSet : k fourteenSetᶜ = (Ioo 0 1 ∪ Ioo 1 2)ᶜ := by
   rw [closure_compl, compl_inj_iff, i_fourteenSet]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem kck_fourteenSet : k (k fourteenSet)ᶜ = (Ioo 0 2 ∪ Ioo 4 5)ᶜ := by
   rw [closure_compl, k_fourteenSet,
     interior_union_of_disjoint_closure, interior_union_of_disjoint_closure]

Archive/Hairer.lean

@@ -113,6 +113,7 @@ lemma inj_L : Injective (L ι) :=
     rw [isOpen_ball.interior_eq]
     apply subset_closure
 
+set_option backward.isDefEq.respectTransparency false in
 lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
     ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ∞ ρ ∧
     ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N →

Archive/Imo/Imo1959Q2.lean

@@ -88,6 +88,7 @@ theorem IsGood.sqrt_two_le (h : IsGood x A) : sqrt 2 ≤ A :=
   (le_or_gt x 1).elim (fun hx ↦ (h.eq_sqrt_two_iff_le_one.2 hx).ge) fun hx ↦
     (h.sqrt_two_lt_of_one_lt hx).le
 
+set_option backward.isDefEq.respectTransparency false in
 theorem isGood_iff_of_sqrt_two_lt (hA : sqrt 2 < A) : IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2 := by
   have : 0 < A := lt_trans (by simp) hA
   constructor

Archive/Imo/Imo1961Q3.lean

@@ -21,6 +21,7 @@ website.
 
 open Real
 
+set_option backward.isDefEq.respectTransparency false in
 theorem Imo1961Q3 {n : ℕ} {x : ℝ} (h₀ : n ≠ 0) :
     (cos x) ^ n - (sin x) ^ n = 1 ↔
       (∃ k : ℤ, k * π = x) ∧ Even n ∨ (∃ k : ℤ, k * (2 * π) = x) ∧ Odd n ∨

Archive/Imo/Imo1963Q5.lean

@@ -24,6 +24,7 @@ lemma sin_pi_mul_neg_div (a b : ℝ) : sin (π * (- a / b)) = - sin (π * (a / b
   ring_nf
   exact sin_neg _
 
+set_option backward.isDefEq.respectTransparency false in
 theorem imo1963_q5 : cos (π / 7) - cos (2 * π / 7) + cos (3 * π / 7) = 1 / 2 := by
   rw [← mul_right_inj' two_sin_pi_div_seven_ne_zero, mul_add, mul_sub, ← sin_two_mul,
     two_mul_sin_mul_cos, two_mul_sin_mul_cos]

Archive/Imo/Imo1972Q5.lean

@@ -14,6 +14,7 @@ Problem: `f` and `g` are real-valued functions defined on the real line. For all
 Prove that `|g(x)| ≤ 1` for all `x`.
 -/
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 This proof begins by introducing the supremum of `f`, `k ≤ 1` as well as `k' = k / ‖g y‖`. We then
 suppose that the conclusion does not hold (`hneg`) and show that `k ≤ k'` (by
@@ -70,6 +71,7 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
     k' < k := H₁
     _ ≤ k' := H₂
 
+set_option backward.isDefEq.respectTransparency false in
 /-- IMO 1972 Q5
 
 Problem: `f` and `g` are real-valued functions defined on the real line. For all `x` and `y`,

Archive/Imo/Imo1982Q1.lean

@@ -55,6 +55,7 @@ namespace IsGood
 variable {f : ℕ+ → ℕ} (hf : IsGood f)
 include hf
 
+set_option backward.isDefEq.respectTransparency false in
 lemma f₁ : f 1 = 0 := by
   have h : f 2 = 2 * f 1 ∨ f 2 = 2 * f 1 + 1 := by rw [two_mul]; exact hf.rel 1 1
   obtain h₁ | h₂ := hf.f₂ ▸ h

Archive/Imo/Imo1982Q3.lean

@@ -77,6 +77,7 @@ theorem imo1982_q3a (hx : Antitone x) (h0 : x 0 = 1) (hp : ∀ k, 0 < x k) :
   convert Imo1982Q3.ineq (Nat.succ_ne_zero 3998) hx h0 hp
   norm_num
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Part b of the problem is solved by `x k = (1 / 2) ^ k`. -/
 theorem imo1982_q3b : ∃ x : ℕ → ℝ, Antitone x ∧ x 0 = 1 ∧ (∀ k, 0 < x k)
     ∧ ∀ n, ∑ k ∈ range n, x k ^ 2 / x (k + 1) < 4 := by

Archive/Imo/Imo1986Q5.lean

@@ -50,6 +50,7 @@ theorem map_eq_zero : f x = 0 ↔ 2 ≤ x := by
 
 theorem map_ne_zero_iff : f x ≠ 0 ↔ x < 2 := by simp [hf.map_eq_zero]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by
   have hx' : 0 < 2 - x := tsub_pos_of_lt hx
   have hfx : f x ≠ 0 := hf.map_ne_zero_iff.2 hx
@@ -67,6 +68,7 @@ theorem map_eq (x : ℝ≥0) : f x = 2 / (2 - x) :=
 
 end IsGood
 
+set_option backward.isDefEq.respectTransparency false in
 theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2 - x) := by
   refine ⟨fun hf ↦ funext hf.map_eq, ?_⟩
   rintro rfl