x: scripts/add_set_option.py

Author: kim-em

Mathlib/AlgebraicGeometry/Fiber.lean

@@ -57,6 +57,8 @@ lemma Scheme.Hom.fiberToSpecResidueField_apply (f : X ⟶ Y) (y : Y) (x : f.fibe
     f.fiberToSpecResidueField y x = IsLocalRing.closedPoint (Y.residueField y) :=
   Subsingleton.elim (α := PrimeSpectrum _) _ _
 
+set_option backward.whnf.reducibleClassField false in
+set_option backward.isDefEq.respectTransparency false in
 lemma isPullback_fiberToSpecResidueField_of_isPullback {P X Y Z : Scheme.{u}} {fst : P ⟶ X}
     {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) (y : Y) :
     IsPullback (pullback.map _ _ _ _ fst (Spec.map (g.residueFieldMap y)) g h.w.symm (by simp))
@@ -68,6 +70,7 @@ lemma isPullback_fiberToSpecResidueField_of_isPullback {P X Y Z : Scheme.{u}} {f
   · simpa using (IsPullback.of_hasPullback _ _).paste_horiz h
   · simp [Scheme.Hom.fiberToSpecResidueField]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The morphism from the fiber of `Spec S ⟶ Spec R` at some prime `p` to `Spec κ(p)`
 is isomorphic to the map induced by `κ(p) ⟶ κ(p) ⊗[R] S`. -/
 noncomputable def Spec.fiberToSpecResidueFieldIso (R S : Type u) [CommRing R] [CommRing S]

Mathlib/AlgebraicGeometry/Morphisms/SmoothFiber.lean

@@ -28,6 +28,7 @@ namespace AlgebraicGeometry
 
 variable {X Y : Scheme.{u}} (f : X ⟶ Y)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- If `f : X ⟶ Y` is locally of finite presentation, flat and has smooth fibers, then `f` is
 smooth. -/
 lemma Smooth.of_smooth_fiberToSpecResidueField [LocallyOfFinitePresentation f] [Flat f]

Mathlib/Analysis/Complex/Poisson.lean

@@ -144,6 +144,8 @@ private lemma circleAverage_re_smul_on_ball_zero_aux {φ θ : ℝ} {r : ℝ} :
 ## Integral Formulas
 -/
 
+set_option backward.whnf.reducibleClassField false in
+set_option backward.isDefEq.respectTransparency false in
 -- Version of `DiffContOnCl.circleAverage_re_smul` in case where the center of the ball is zero.
 private lemma DiffContOnCl.circleAverage_re_smul_on_ball_zero [CompleteSpace E]
     (hf : DiffContOnCl ℂ f (ball 0 R)) (hw : w ∈ ball 0 R) :
@@ -204,6 +206,8 @@ private lemma DiffContOnCl.circleAverage_re_smul_on_ball_zero [CompleteSpace E]
       rw [← abs_of_pos hR] at hw hf
       simp [← hf.circleAverage_smul_div hw, circleAverage_eq_circleIntegral (ne_of_lt hR).symm, h0]
 
+set_option backward.isDefEq.respectTransparency false in
+set_option backward.whnf.reducibleClassField false in
 /--
 **Poisson integral formula** for ℂ-differentiable functions on arbitrary disks in the complex plane,
 formulated with the real part of the Herglotz–Riesz kernel of integration.

Mathlib/Analysis/LocallyConvex/WeakDual.lean

@@ -180,6 +180,7 @@ theorem mem_span_iff_bound {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜]
 
 variable [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The Weak Representation Theorem: Every continuous functional on `E` endowed with
 the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`. -/
 theorem dualEmbedding_surjective : Function.Surjective (WeakBilin.eval B) := fun f ↦ by

Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean

@@ -134,10 +134,13 @@ should prefer the generic API, especially because it will make rewriting easier.
 protected noncomputable def cfc (f : ℝ → ℝ) : Matrix n n 𝕜 :=
   conjStarAlgAut 𝕜 _ hA.eigenvectorUnitary (diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues))
 
+set_option backward.whnf.reducibleClassField false in
+set_option backward.isDefEq.respectTransparency false in
 lemma cfcHom_eq_cfcAux : cfcHom hA.isSelfAdjoint = hA.cfcAux :=
   cfcHom_eq_of_continuous_of_map_id hA hA.cfcAux
     hA.isClosedEmbedding_cfcAux.continuous hA.cfcAux_id
 
+set_option backward.isDefEq.respectTransparency false in
 instance instContinuousFunctionalCalculusIsClosedEmbedding :
     ClosedEmbeddingContinuousFunctionalCalculus ℝ (Matrix n n 𝕜) IsSelfAdjoint where
   isClosedEmbedding _ hA := cfcHom_eq_cfcAux hA ▸ hA.isHermitian.isClosedEmbedding_cfcAux

Mathlib/Analysis/ODE/PicardLindelof.lean

@@ -656,6 +656,7 @@ lemma weaken_lipschitz (hf : IsPicardLindelof f t₀ x₀ a r L K) {K' : ℝ≥0
   norm_le := hf.norm_le
   mul_max_le := hf.mul_max_le
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Given `IsPicardLindelof` on a symmetric interval `[t₀ - ε, t₀ + ε]`, if we shrink the radius
 from `a` to `a'` with `a' ≤ a`, and choose any `r' < a'`, then there exists `ε' > 0` such that
 `IsPicardLindelof` holds on `[t₀ - ε', t₀ + ε']` with the new parameters. -/

Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean

@@ -745,6 +745,7 @@ lemma sheafifyHomEquivOfIsEquivalence_naturality_right
 
 variable (A)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Assuming that `(C, J)` is a dense subsite of `(D, K)` (via a functor `G : C ⥤ D`)
 and `sheafPushforwardContinuous G A J K` is an equivalence of categories, and
 that `HasWeakSheafify J A` holds, then this adjunction shows the existence

Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean

@@ -642,6 +642,8 @@ namespace presheafObjObjIso
 
 variable (X₀ : C₀)
 
+set_option backward.whnf.reducibleClassField false in
+set_option backward.isDefEq.respectTransparency false in
 /-- Auxiliary definition for `OneHypercoverDenseData.essSurj.presheafObjObjIso`. -/
 noncomputable def hom : (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.val.obj (op X₀) :=
   G₀.2.amalgamate ⟨_, cover_lift F J₀ _ (data (F.obj X₀)).mem₀⟩ (fun ⟨W₀, a, ha⟩ ↦
@@ -660,6 +662,7 @@ noncomputable def hom : (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.val.
 
 variable {X₀}
 
+set_option backward.whnf.reducibleClassField false in
 @[reassoc]
 lemma hom_map {W₀ : C₀} (a : W₀ ⟶ X₀) {i : (data (F.obj X₀)).I₀}
     (p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i))
@@ -701,6 +704,7 @@ lemma inv_π (i : (data (F.obj X₀)).I₀) :
       IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i) :=
   Multiequalizer.lift_ι _ _ _ _ _
 
+set_option backward.isDefEq.respectTransparency false in
 @[reassoc (attr := simp)]
 lemma inv_restriction {Y₀ : C₀} (f : F.obj Y₀ ⟶ F.obj X₀) :
     inv data G₀ X₀ ≫ restriction data G₀ f =
@@ -721,6 +725,8 @@ lemma inv_restriction {Y₀ : C₀} (f : F.obj Y₀ ⟶ F.obj X₀) :
 
 end presheafObjObjIso
 
+set_option backward.whnf.reducibleClassField false in
+set_option backward.isDefEq.respectTransparency false in
 /-- The presheaf `presheaf data G₀` extends `G₀`. -/
 noncomputable def presheafObjObjIso (X₀ : C₀) :
     (presheaf data G₀).obj (op (F.obj X₀)) ≅ G₀.val.obj (op X₀) where
@@ -737,6 +743,8 @@ noncomputable def presheafObjObjIso (X₀ : C₀) :
     dsimp at i b fac ⊢
     simp [presheafObjObjIso.hom_map data G₀ _ b fac, ← IsDenseSubsite.mapPreimage_comp, fac]
 
+set_option backward.isDefEq.respectTransparency false in
+set_option backward.whnf.reducibleClassField false in
 @[reassoc (attr := simp)]
 lemma presheafMap_presheafObjObjIso_hom (X : C) (i : (data X).I₀) :
     presheafMap data G₀ ((data X).f i) ≫ (presheafObjObjIso data G₀ ((data X).X i)).hom =
@@ -749,6 +757,7 @@ lemma presheafMap_presheafObjObjIso_hom (X : C) (i : (data X).I₀) :
   apply restriction_eq_of_fac
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[reassoc]
 lemma presheafObjObjIso_inv_naturality {X₀ Y₀ : C₀} (f : X₀ ⟶ Y₀) :
     G₀.val.map f.op ≫ (presheafObjObjIso data G₀ X₀).inv =

Mathlib/LinearAlgebra/QuadraticForm/Radical.lean

@@ -86,6 +86,7 @@ lemma lift_mk {N : Submodule R M} (hN : N ≤ Q.radical) (m : M) :
     Q.lift N hN (Submodule.Quotient.mk m) = Q m :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 Universal property of the radical of a quadratic form:
 `Q.radical` is the largest subspace `N` such that

Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean

@@ -140,6 +140,7 @@ theorem le_iff_le (x : K) (r : ℝ) : (∀ w : InfinitePlace K, w x ≤ r) ↔ 
 
 theorem pos_iff {w : InfinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0 := AbsoluteValue.pos_iff w.1
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem mk_eq_iff {φ ψ : K →+* ℂ} : mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ := by
   constructor