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

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

Archive/Imo/Imo1988Q6.lean

@@ -188,6 +188,7 @@ end Imo1988Q6
 
 open Imo1988Q6
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Question 6 of IMO1988. If a and b are two natural numbers
 such that a*b+1 divides a^2 + b^2, show that their quotient is a perfect square. -/
 theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
@@ -244,6 +245,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
   · -- There is no base case in this application of Vieta jumping.
     simp
 
+set_option backward.isDefEq.respectTransparency false in
 /-
 The following example illustrates the use of constant descent Vieta jumping
 in the presence of a non-trivial base case.

Archive/Imo/Imo1998Q2.lean

@@ -153,6 +153,7 @@ end
 theorem add_sq_add_sq_sub {α : Type*} [Ring α] (x y : α) :
     (x + y) * (x + y) + (x - y) * (x - y) = 2 * x * x + 2 * y * y := by noncomm_ring
 
+set_option backward.isDefEq.respectTransparency false in
 theorem norm_bound_of_odd_sum {x y z : ℤ} (h : x + y = 2 * z + 1) :
     2 * z * z + 2 * z + 1 ≤ x * x + y * y := by
   suffices 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y by

Archive/Imo/Imo2001Q4.lean

@@ -35,6 +35,7 @@ variable {n : ℕ} {c : Fin n → ℤ}
 rather than `Icc 1 n`, and as such contains `+ 1` to compensate. -/
 def S (c : Fin n → ℤ) (a : Perm (Fin n)) : ℤ := ∑ i, c i * (a i + 1)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Assuming the opposite of what is to be proved, the sum of `S` over all permutations is
 congruent to the sum of all residues modulo `n!`, i.e. `n! * (n! - 1) / 2`. -/
 lemma sum_range_modEq_sum_of_contra (hS : ¬∃ a b, a ≠ b ∧ (n ! : ℤ) ∣ S c a - S c b) :
@@ -93,6 +94,7 @@ lemma sum_modEq_zero_of_odd (hn : Odd n) : ∑ a, S c a ≡ 0 [ZMOD n !] := by
     Nat.mul_factorial_pred hn.pos.ne', Nat.cast_mul, ← mul_assoc, ← mul_rotate]
   exact (Int.dvd_mul_left ..).modEq_zero_int
 
+set_option backward.isDefEq.respectTransparency false in
 theorem result (hn : Odd n ∧ 1 < n) : ∃ a b, a ≠ b ∧ (n ! : ℤ) ∣ S c a - S c b := by
   by_contra h
   have key := (sum_range_modEq_sum_of_contra h).trans (sum_modEq_zero_of_odd hn.1)

Archive/Imo/Imo2001Q5.lean

@@ -178,6 +178,7 @@ lemma key_x_equation :
 
 /-! ### Solving the trigonometric equation -/
 
+set_option backward.isDefEq.respectTransparency false in
 lemma x_eq : s.x = 2 * π / 9 := by
   have work := s.key_x_equation
   rw [Real.sin_add_sin, show 2 * π / 3 - s.x = π - 2 * ((s.x + π / 3) / 2) by ring, Real.sin_pi_sub,

Archive/Imo/Imo2006Q3.lean

@@ -82,6 +82,7 @@ theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
   · convert this y z x _ h using 2 <;> linarith
   · convert this z x y _ h using 2 <;> linarith
 
+set_option backward.isDefEq.respectTransparency false in
 theorem proof₁ {a b c : ℝ} :
     |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤
       9 * sqrt 2 / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2 :=

Archive/Imo/Imo2010Q5.lean

@@ -126,6 +126,7 @@ lemma double {B : Fin 6 → ℕ} {i : Fin 6}
       · grind [swap_apply_right, single_eq_same, single_succ]
       · rw [swap_apply_of_ne_of_ne hk' hk'', single_eq_of_ne hk', this, single_eq_of_ne hk'']
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `double` as many times as possible, emptying $B_i$ and doubling $B_{i+1}$ that many times. -/
 lemma doubles {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (zB : B (i + 2) = 0) :
     Reachable (update (B - single i (B i)) (i + 1) (B (i + 1) * 2 ^ B i)) := by
@@ -144,6 +145,7 @@ lemma doubles {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (z
       · simp_rw [single_eq_of_ne hk]
 termination_by B i
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Empty $B_i$ and set $B_{i+1} = 2^{B_i}$, assuming $B_{i+1} = B_{i+2} = 0$. -/
 lemma exp {B : Fin 6 → ℕ} {i : Fin 6}
     (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 1) = 0) (zB' : B (i + 2) = 0) :

Archive/Imo/Imo2011Q3.lean

@@ -21,6 +21,7 @@ Direct translation of the solution found in https://www.imo-official.org/problem
 -/
 
 
+set_option backward.isDefEq.respectTransparency false in
 theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f x)) : ∀ x ≤ 0, f x = 0 := by
   -- reparameterize
   have hxt : ∀ x t, f t ≤ t * f x - x * f x + f (f x) := fun x t =>

Archive/Imo/Imo2013Q5.lean

@@ -31,6 +31,7 @@ https://www.imo-official.org/problems/IMO2013SL.pdf
 
 namespace Imo2013Q5
 
+set_option backward.isDefEq.respectTransparency false in
 theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
     (h : ∀ n : ℕ, 0 < n → x ^ n - 1 < y ^ n) : x ≤ y := by
   by_contra! hxy
@@ -164,6 +165,7 @@ end Imo2013Q5
 
 open Imo2013Q5
 
+set_option backward.isDefEq.respectTransparency false in
 theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
     (H2 : ∀ x y, 0 < x → 0 < y → f x + f y ≤ f (x + y)) (H_fixed_point : ∃ a, 1 < a ∧ f a = a) :
     ∀ x, 0 < x → f x = x := by

Archive/Imo/Imo2015Q6.lean

@@ -175,6 +175,7 @@ lemma sum_pool_le : ∑ x ∈ pool a t, x ≤ ∑ i ∈ range (b - 1), (2014 - i
 
 end Sums
 
+set_option backward.isDefEq.respectTransparency false in
 theorem result (ha : Condition a) :
     ∃ b > 0, ∃ N, ∀ m ≥ N, ∀ n > m, |∑ j ∈ Ico m n, (a j - b)| ≤ 1007 ^ 2 := by
   obtain ⟨b, N, hbN⟩ := exists_max_card_pool ha

Archive/Imo/Imo2024Q1.lean

@@ -57,6 +57,7 @@ lemma condition_sub_two_mul_int_iff {α : ℝ} (m : ℤ) : Condition (α - 2 * m
   rw [Int.floor_intCast]
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 lemma condition_toIcoMod_iff {α : ℝ} :
     Condition (toIcoMod (by simp : (0 : ℝ) < 2) 0 α) ↔ Condition α := by
   rw [toIcoMod, zsmul_eq_mul, mul_comm, condition_sub_two_mul_int_iff]
@@ -66,6 +67,7 @@ namespace Condition
 variable {α : ℝ} (hc : Condition α)
 include hc
 
+set_option backward.isDefEq.respectTransparency false in
 lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
   rcases h with ⟨h0, h2⟩
   refine ⟨?_, h2⟩
@@ -96,6 +98,7 @@ lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
     calc x * α < α⁻¹ * α := by gcongr; exact hx.2
       _ = 1 := by simp [h0.ne']
 
+set_option backward.isDefEq.respectTransparency false in
 lemma mem_Ico_n_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) {n : ℕ} (hn : 0 < n) :
     α ∈ Set.Ico ((2 * n - 1) / n : ℝ) 2 := by
   suffices ∑ i ∈ Finset.Icc 1 n, ⌊i * α⌋ = n ^ 2 ∧ α ∈ Set.Ico ((2 * n - 1) / n : ℝ) 2 from this.2
@@ -173,6 +176,7 @@ lemma condition_iff_of_mem_Ico {α : ℝ} (h : α ∈ Set.Ico 0 2) : Condition 
 recall Imo2024Q1.Condition (α : ℝ) := (∀ n : ℕ, 0 < n → (n : ℤ) ∣ ∑ i ∈ Finset.Icc 1 n, ⌊i * α⌋)
 recall Imo2024Q1.solutionSet := {α : ℝ | ∃ m : ℤ, α = 2 * m}
 
+set_option backward.isDefEq.respectTransparency false in
 theorem result (α : ℝ) : Condition α ↔ α ∈ solutionSet := by
   refine ⟨fun h ↦ ?_, ?_⟩
   · rw [← condition_toIcoMod_iff, condition_iff_of_mem_Ico (toIcoMod_mem_Ico' _ _),

Archive/Imo/Imo2024Q2.lean

@@ -27,6 +27,7 @@ open scoped Nat
 def Condition (a b : ℕ) : Prop :=
   0 < a ∧ 0 < b ∧ ∃ g N : ℕ, 0 < g ∧ 0 < N ∧ ∀ n : ℕ, N ≤ n → Nat.gcd (a ^ n + b) (b ^ n + a) = g
 
+set_option backward.isDefEq.respectTransparency false in
 lemma dvd_pow_iff_of_dvd_sub {a b d n : ℕ} {z : ℤ} (ha : a.Coprime d)
     (hd : (φ d : ℤ) ∣ (n : ℤ) - z) :
     d ∣ a ^ n + b ↔ (((ZMod.unitOfCoprime _ ha) ^ z : (ZMod d)ˣ) : ZMod d) + b = 0 := by

Archive/Imo/Imo2024Q3.lean

@@ -502,6 +502,7 @@ lemma small_apply_N' : Small a (a (N' a N)) := by
       simpa [hi] using hc.small_or_big_of_N'aux_lt (Nat.lt_add_one (N'aux a N))
     exact hc.apply_add_one_small_of_apply_big_of_N'aux_le hb (by lia)
 
+set_option backward.isDefEq.respectTransparency false in
 lemma small_apply_N'_add_iff_even {n : ℕ} : Small a (a (N' a N + n)) ↔ Even n := by
   induction n with
   | zero => simpa using hc.small_apply_N'

Archive/Imo/Imo2024Q5.lean

@@ -488,8 +488,8 @@ lemma Strategy.play_one (s : Strategy N) (m : MonsterData N) {k : ℕ} (hk : 1 <
     s.play m k ⟨1, hk⟩ = (s ![(s Fin.elim0).firstMonster m]).firstMonster m := by
   have hk' : 2 ≤ k := by lia
   rw [s.play_apply_of_le m one_lt_two hk']
-  simp only [play, Fin.snoc, lt_self_iff_false, ↓reduceDIte, Nat.reduceAdd,
-    Fin.mk_one, Fin.isValue, cast_eq, Nat.succ_eq_add_one]
+  simp only [play, Fin.snoc, lt_self_iff_false, ↓reduceDIte, Nat.reduceAdd, cast_eq,
+    Nat.succ_eq_add_one]
   congr
   refine funext fun i ↦ ?_
   simp_rw [Fin.fin_one_eq_zero]

Archive/Imo/Imo2024Q6.lean

@@ -207,12 +207,14 @@ lemma aquaesulian_fExample : Aquaesulian fExample := by
     exact .inr (apply_fExample_add_apply_of_fract_le h.le)
   · exact .inl (apply_fExample_add_apply_of_fract_le h)
 
+set_option backward.isDefEq.respectTransparency false in
 lemma fract_fExample (x : ℚ) :
     Int.fract (fExample x) = if Int.fract x = 0 then 0 else 1 - Int.fract x := by
   by_cases h : Int.fract x = 0
   · simp [fExample, h]
   · simp [fExample, h, sub_eq_add_neg, Int.fract_neg]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma floor_fExample (x : ℚ) :
     ⌊fExample x⌋ = if Int.fract x = 0 then x else ⌊x⌋ - 1 := by
   by_cases h : Int.fract x = 0
@@ -225,6 +227,7 @@ lemma floor_fExample (x : ℚ) :
     rw [Int.floor_eq_iff]
     simp [(Int.fract_nonneg x).lt_of_ne' h, (Int.fract_lt_one x).le]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma card_range_fExample : #(Set.range (fun x ↦ fExample x + fExample (-x))) = 2 := by
   have h : Set.range (fun x ↦ fExample x + fExample (-x)) = {0, -2} := by
     ext x

Archive/Kuratowski.lean

@@ -98,6 +98,7 @@ theorem mem_theFourteen_iff_isObtainable {s t : Set X} :
       exact IsObtainable.base
   mpr := (·.mem_theFourteen)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- **Kuratowski's closure-complement theorem**: the number of obtainable sets via closure and
 complement operations from a single set `s` is at most 14. -/
 theorem ncard_isObtainable_le_fourteen (s : Set X) : {t | IsObtainable s t}.ncard ≤ 14 := by

Archive/MiuLanguage/DecisionNec.lean

@@ -59,6 +59,7 @@ theorem mod3_eq_1_or_mod3_eq_2 {a b : ℕ} (h1 : a % 3 = 1 ∨ a % 3 = 2)
     · right; simp [h2, mul_mod, h1]
     · left; simp only [h2, mul_mod, h1, mod_mod]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `count_equiv_one_or_two_mod3_of_derivable` shows any derivable string must have a `count I` that
 is 1 or 2 modulo 3.
 -/
@@ -104,8 +105,10 @@ string to be derivable, namely that the string must start with an M and contain
 def Goodm (xs : Miustr) : Prop :=
   List.headI xs = M ∧ M ∉ List.tail xs
 
+set_option backward.isDefEq.respectTransparency false in
 instance : DecidablePred Goodm := by unfold Goodm; infer_instance
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Demonstration that `"MI"` starts with `M` and has no `M` in its tail.
 -/
 theorem goodmi : Goodm [M, I] := by
@@ -119,6 +122,7 @@ We'll show, for each `i` from 1 to 4, that if `en` follows by Rule `i` from `st`
 -/
 
 
+set_option backward.isDefEq.respectTransparency false in
 theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ [I])) (h₂ : Goodm (xs ++ [I])) :
     Goodm (xs ++ [I, U]) := by
   obtain ⟨mhead, nmtail⟩ := h₂
@@ -138,6 +142,7 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
     rw [cons_append] at mtail
     exact or_self_iff.mp (mem_append.mp mtail)
 
+set_option backward.isDefEq.respectTransparency false in
 theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs))
     (h₂ : Goodm (as ++ [I, I, I] ++ bs)) : Goodm (as ++ (U :: bs)) := by
   obtain ⟨mhead, nmtail⟩ := h₂
@@ -156,6 +161,7 @@ The proof of the next lemma is identical, on the tactic level, to the previous p
 -/
 
 
+set_option backward.isDefEq.respectTransparency false in
 theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs))
     (h₂ : Goodm (as ++ [U, U] ++ bs)) : Goodm (as ++ bs) := by
   obtain ⟨mhead, nmtail⟩ := h₂

Archive/MiuLanguage/DecisionSuf.lean

@@ -49,6 +49,7 @@ namespace Miu
 
 open MiuAtom List Nat
 
+set_option backward.isDefEq.respectTransparency false in
 /-- We start by showing that an `Miustr` `M::w` can be derived, where `w` consists only of `I`s and
 where `count I w` is a power of 2.
 -/
@@ -243,6 +244,7 @@ conditions under which `count I ys = length ys`.
 -/
 
 
+set_option backward.isDefEq.respectTransparency false in
 /-- If an `Miustr` has a zero `count U` and contains no `M`, then its `count I` is its length.
 -/
 theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count U ys = 0)
@@ -284,6 +286,7 @@ relate to `count U`.
 -/
 
 
+set_option backward.isDefEq.respectTransparency false in
 theorem mem_of_count_U_eq_succ {xs : Miustr} {k : ℕ} (h : count U xs = succ k) : U ∈ xs := by
   induction xs with
   | nil => exfalso; rw [count] at h; contradiction
@@ -296,6 +299,7 @@ theorem eq_append_cons_U_of_count_U_pos {k : ℕ} {zs : Miustr} (h : count U zs
     ∃ as bs : Miustr, zs = as ++ ↑(U :: bs) :=
   append_of_mem (mem_of_count_U_eq_succ h)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `ind_hyp_suf` is the inductive step of the sufficiency result.
 -/
 theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : Decstr ys) :