set_option

Author: kim-em

Mathlib/RingTheory/MvPowerSeries/Order.lean

@@ -155,6 +155,7 @@ theorem weightedOrder_eq_top_iff :
     f.weightedOrder w = ⊤ ↔ f = 0 := by
   rw [← not_iff_not, ← ne_eq, ← ne_eq, ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- If the order of a formal power series `f` is finite,
 then some coefficient of weight equal to the order of `f` is nonzero. -/
 theorem exists_coeff_ne_zero_and_weightedOrder
@@ -165,6 +166,7 @@ theorem exists_coeff_ne_zero_and_weightedOrder
   generalize_proofs h1
   exact Nat.find_spec h1
 
+set_option backward.isDefEq.respectTransparency false in
 /-- If the `d`th coefficient of a formal power series is nonzero,
 then the weighted order of the power series is less than or equal to `weight d w`. -/
 theorem weightedOrder_le {d : σ →₀ ℕ} (h : coeff d f ≠ 0) :
@@ -180,6 +182,7 @@ theorem coeff_eq_zero_of_lt_weightedOrder {d : σ →₀ ℕ} (h : (weight w d)
     coeff d f = 0 := by
   contrapose! h; exact weightedOrder_le w h
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The order of a formal power series is at least `n` if
 the `d`th coefficient is `0` for all `d` such that `weight w d < n`. -/
 theorem nat_le_weightedOrder {n : ℕ} (h : ∀ d, weight w d < n → coeff d f = 0) :
@@ -191,6 +194,7 @@ theorem nat_le_weightedOrder {n : ℕ} (h : ∀ d, weight w d < n → coeff d f
   rw [← hd, Nat.cast_lt] at H
   exact hfd (h d H)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The order of a formal power series is at least `n` if
 the `d`th coefficient is `0` for all `d` such that `weight w d < n`. -/
 theorem le_weightedOrder {n : ℕ∞} (h : ∀ d : σ →₀ ℕ, weight w d < n → coeff d f = 0) :
@@ -201,6 +205,7 @@ theorem le_weightedOrder {n : ℕ∞} (h : ∀ d : σ →₀ ℕ, weight w d < n
   · apply nat_le_weightedOrder;
     simpa only [ENat.some_eq_coe, Nat.cast_lt] using h
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The order of a formal power series is exactly `n` if and only if some coefficient of weight `n`
 is nonzero, and the `d`th coefficient is `0` for all `d` such that `weight w d < n`. -/
 theorem weightedOrder_eq_nat {n : ℕ} :
@@ -248,6 +253,7 @@ theorem min_weightedOrder_le_add :
     [coeff_eq_zero_of_lt_weightedOrder w, lt_min_iff, map_add, add_zero,
       imp_true_iff]
 
+set_option backward.isDefEq.respectTransparency false in
 private theorem weightedOrder_add_of_weightedOrder_lt.aux
     (H : f.weightedOrder w < g.weightedOrder w) :
     (f + g).weightedOrder w = f.weightedOrder w := by
@@ -478,6 +484,7 @@ theorem le_order_prod {R : Type*} [CommSemiring R] {ι : Type*}
     (f : ι → MvPowerSeries σ R) (s : Finset ι) : ∑ i ∈ s, (f i).order ≤ (∏ i ∈ s, f i).order :=
   le_weightedOrder_prod _ _ _
 
+set_option backward.isDefEq.respectTransparency false in
 theorem one_le_order_iff_constCoeff_eq_zero :
     1 ≤ f.order ↔ f.constantCoeff = 0 := by
   constructor
@@ -617,6 +624,7 @@ theorem weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero
     exact hf
   · rw [map_zero]
 
+set_option backward.isDefEq.respectTransparency false in
 variable {w} in
 theorem weightedHomogeneousComponent_of_weightedOrder
     {f : MvPowerSeries σ R} {p : ℕ} (hf : p = f.weightedOrder w) :