Merge branch 'angle_incenter_unoriented' into imo2024q4

Author: jsm28

Mathlib.lean

@@ -202,6 +202,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
 public import Mathlib.Algebra.Category.ModuleCat.Simple
+public import Mathlib.Algebra.Category.ModuleCat.Stalk
 public import Mathlib.Algebra.Category.ModuleCat.Subobject
 public import Mathlib.Algebra.Category.ModuleCat.Tannaka
 public import Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -195,6 +195,9 @@ instance hasForgetToMonCat : HasForget₂ GrpCat MonCat where
     (f : X →* Y) :
     (forget₂ GrpCat MonCat).map (ofHom f) = MonCat.ofHom f := rfl
 
+@[to_additive (attr := simp)] lemma forget₂_map {R S : GrpCat} (f : R ⟶ S) (x) :
+    (forget₂ GrpCat MonCat).map f x = f x := rfl
+
 @[to_additive]
 instance : Coe GrpCat.{u} MonCat.{u} where coe := (forget₂ GrpCat MonCat).obj
 
@@ -412,6 +415,9 @@ instance hasForgetToGroup : HasForget₂ CommGrpCat GrpCat where
     (f : X →* Y) :
     (forget₂ CommGrpCat GrpCat).map (ofHom f) = GrpCat.ofHom f := rfl
 
+@[to_additive (attr := simp)] lemma forget₂_map {R S : CommGrpCat} (f : R ⟶ S) (x) :
+    (forget₂ CommGrpCat GrpCat).map f x = f x := rfl
+
 @[to_additive]
 instance : Coe CommGrpCat.{u} GrpCat.{u} where coe := (forget₂ CommGrpCat GrpCat).obj
 

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -67,6 +67,10 @@ protected lemma map_smul {X Y : Cᵒᵖ} (f : X ⟶ Y) (r : R.obj X) (m : M.obj
 lemma congr_map_apply {X Y : Cᵒᵖ} {f g : X ⟶ Y} (h : f = g) (m : M.obj X) :
     M.map f m = M.map g m := by rw [h]
 
+lemma map_comp_apply {U V W : Cᵒᵖ} (i : U ⟶ V) (j : V ⟶ W) (x) :
+    M.map (i ≫ j) x = M.map j (M.map i x) := by
+  rw [M.map_comp]; rfl
+
 /-- A morphism of presheaves of modules consists of a family of linear maps which
 satisfy the naturality condition. -/
 @[ext]

Mathlib/Algebra/Category/ModuleCat/Stalk.lean

@@ -0,0 +1,202 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.Presheaf
+public import Mathlib.Algebra.Category.Ring.Colimits
+public import Mathlib.Algebra.Category.Ring.FilteredColimits
+public import Mathlib.CategoryTheory.Limits.Filtered
+public import Mathlib.Topology.Sheaves.Stalks
+
+/-!
+
+# Module structure on stalks
+Let `M` be a presheaf of `R`-modules on a topological space. We endow `M.presheaf.stalk x` with
+an `R.stalk x`-module structure.
+
+The key characterizing lemma is `PresheafOfModules.germ_smul`, which describes the compatibility
+of the scalar action and `TopCat.Presheaf.germ`.
+
+-/
+
+@[expose] public section
+
+open CategoryTheory LinearMap Opposite TopologicalSpace
+
+universe w₀ w u v
+
+namespace CategoryTheory.Limits
+
+open IsFiltered
+
+variable {C : Type*} [SmallCategory C] [IsFiltered C] (R : C ⥤ RingCat) (M : C ⥤ Ab)
+    [∀ i, Module (R.obj i) (M.obj i)]
+    (H : ∀ {i j} (f : i ⟶ j) r m, M.map f (r • m) = R.map f r • M.map f m)
+
+/-- (Implementation). The scalar multiplication function on `ColimitType`. -/
+protected noncomputable
+def colimit.smul (r : (R ⋙ forget _).ColimitType) (m : (M ⋙ forget _).ColimitType) :
+    (M ⋙ forget _).ColimitType := by
+  refine Quot.liftOn₂ r m (fun Ua Vb ↦ Functor.ιColimitType _ (max Ua.1 Vb.1) <|
+    letI a : R.obj (max Ua.1 Vb.1) := R.map (leftToMax Ua.1 Vb.1) Ua.2
+    letI b : M.obj (max Ua.1 Vb.1) := M.map (rightToMax Ua.1 Vb.1) Vb.2
+    a • b) ?_ ?_
+  · rintro ⟨U, a⟩ ⟨V₁, b₁⟩ ⟨V₂, b₂⟩ ⟨f : V₁ ⟶ V₂, rfl : b₂ = M.map _ b₁⟩
+    obtain ⟨s, α, β, h₁, h₂⟩ :=
+      bowtie (leftToMax U V₁) (leftToMax U V₂)
+        (rightToMax U V₁) (f ≫ rightToMax U V₂)
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
+    simp [*, ← elementwise_of% R.map_comp, ← elementwise_of% M.map_comp, -Functor.map_comp]
+  · rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩ ⟨f : U₁ ⟶ U₂, rfl : a₂ = R.map _ a₁⟩
+    obtain ⟨s, α, β, h₁, h₂⟩ :=
+      bowtie (leftToMax U₁ V) (f ≫ leftToMax U₂ V)
+        (rightToMax U₁ V) (rightToMax U₂ V)
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
+    simp [*, ← elementwise_of% R.map_comp, ← elementwise_of% M.map_comp, -Functor.map_comp]
+
+/-- (Implementation). The module structure on `AddCommGrpCat.FilteredColimits.colimit`. -/
+noncomputable abbrev filteredColimitsModule : Module (RingCat.FilteredColimits.colimit R)
+    (AddCommGrpCat.FilteredColimits.colimit M) where
+  smul := colimit.smul R M H
+  mul_smul r s m := Quot.induction_on₃ r s m <| by
+    rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩
+    obtain ⟨s, α, β, h₁, h₂, h₃⟩ := crown₃
+      (leftToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V) (leftToMax U₁ (max U₂ V))
+      (rightToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V) (leftToMax U₂ V ≫ rightToMax U₁ (max U₂ V))
+      (rightToMax (max U₁ U₂) V) (rightToMax U₂ V ≫ rightToMax U₁ (max U₂ V))
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
+    dsimp
+    simp only [map_mul, ← ConcreteCategory.comp_apply, ← Functor.map_comp, mul_smul, *]
+  one_smul m := Quot.induction_on m <| by
+    rintro ⟨V, b⟩
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (rightToMax _ _) ?_
+    dsimp
+    simp only [map_one, ← ConcreteCategory.comp_apply, ← Functor.map_comp, one_smul,
+      Category.comp_id]
+  smul_zero r := Quot.induction_on r <| by
+    rintro ⟨U, a⟩
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (rightToMax _ _) ?_
+    dsimp
+    simp only [map_zero, smul_zero]
+  smul_add r m n := Quot.induction_on₃ r m n <| by
+    rintro ⟨U, a⟩ ⟨V₁, b₁⟩ ⟨V₂, b₂⟩
+    obtain ⟨s, α, β, h₁, h₂, h₃, h₄⟩ := crown₄
+      (leftToMax U V₁ ≫ leftToMax (max U V₁) (max U V₂)) (leftToMax U (max V₁ V₂))
+      (leftToMax U V₂ ≫ rightToMax (max U V₁) (max U V₂)) (leftToMax U (max V₁ V₂))
+      (rightToMax U V₁ ≫ leftToMax (max U V₁) (max U V₂))
+      (leftToMax V₁ V₂ ≫ rightToMax U (max V₁ V₂))
+      (rightToMax U V₂ ≫ rightToMax (max U V₁) (max U V₂))
+      (rightToMax V₁ V₂ ≫ rightToMax U (max V₁ V₂))
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ β α ?_
+    dsimp
+    simp only [*, ← ConcreteCategory.comp_apply, ← Functor.map_comp, map_add, smul_add]
+  add_smul r s m := Quot.induction_on₃ r s m <| by
+    rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩
+    obtain ⟨s, α, β, h₁, h₂, h₃, h₄⟩ := crown₄
+      (rightToMax U₁ V ≫ leftToMax (max U₁ V) (max U₂ V)) (rightToMax (max U₁ U₂) V)
+      (rightToMax U₂ V ≫ rightToMax (max U₁ V) (max U₂ V)) (rightToMax (max U₁ U₂) V)
+      (leftToMax U₁ V ≫ leftToMax (max U₁ V) (max U₂ V))
+      (leftToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V)
+      (leftToMax U₂ V ≫ rightToMax (max U₁ V) (max U₂ V))
+      (rightToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V)
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ β α ?_
+    dsimp
+    simp only [add_smul, map_add, ← ConcreteCategory.comp_apply, ← Functor.map_comp, *]
+  zero_smul m := Quot.induction_on m <| by
+    rintro ⟨V, b⟩
+    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (leftToMax _ _) ?_
+    dsimp
+    simp only [map_zero, zero_smul, *]
+
+/-- Given a cofiltered diagram of rings `R`, and a module `M` over `R`,
+this is the `colim R`-module structure of `colim M`. -/
+noncomputable abbrev IsColimit.module {cR : Cocone R} (hcR : IsColimit cR) {cM : Cocone M}
+    (hcM : IsColimit cM) : Module cR.pt cM.pt :=
+  letI := filteredColimitsModule R M H
+  letI : Module (RingCat.FilteredColimits.colimit R) cM.pt :=
+    AddEquiv.module (β := AddCommGrpCat.FilteredColimits.colimit M) _
+        (IsColimit.coconePointUniqueUpToIso hcM
+          (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)).addCommGroupIsoToAddEquiv
+  .compHom (R := RingCat.FilteredColimits.colimit R) _
+    (IsColimit.coconePointUniqueUpToIso hcR
+          (RingCat.FilteredColimits.colimitCoconeIsColimit R)).ringCatIsoToRingEquiv.toRingHom
+
+lemma IsColimit.ι_smul {cR : Cocone R} (hcR : IsColimit cR) {cM : Cocone M}
+    (hcM : IsColimit cM) (i : C) (r : R.obj i) (m : M.obj i) :
+    letI := IsColimit.module R M H hcR hcM
+    cM.ι.app i (r • m) =
+      HSMul.hSMul (α := cR.pt) (β := cM.pt) (cR.ι.app i r) (cM.ι.app i m) := by
+  letI := filteredColimitsModule R M H
+  let α := IsColimit.coconePointUniqueUpToIso hcM
+    (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
+  let β := IsColimit.coconePointUniqueUpToIso hcR
+    (RingCat.FilteredColimits.colimitCoconeIsColimit R)
+  apply α.addCommGroupIsoToAddEquiv.eq_symm_apply.mpr ?_
+  change (cM.ι.app i ≫ α.hom) _ = (HSMul.hSMul (α := RingCat.FilteredColimits.colimit R)
+    (β := AddCommGrpCat.FilteredColimits.colimit M)
+    ((cR.ι.app i ≫ β.hom) r) ((cM.ι.app i ≫ α.hom) m))
+  simp only [Functor.const_obj_obj, comp_coconePointUniqueUpToIso_hom, α, β]
+  obtain ⟨s, α, H⟩ :=  IsFilteredOrEmpty.cocone_maps (leftToMax i i) (rightToMax i i)
+  refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (leftToMax _ _ ≫ α) α ?_
+  dsimp
+  simp only [← ConcreteCategory.comp_apply, ← Functor.map_comp, *]
+
+end CategoryTheory.Limits
+
+namespace PresheafOfModules
+
+variable {X : TopCat.{u}} {R : X.Presheaf RingCat.{u}} (M : PresheafOfModules.{u} R)
+
+variable (x : X)
+
+noncomputable
+instance : Module (R.stalk x) ↑(TopCat.Presheaf.stalk M.presheaf x) :=
+  letI (i : (OpenNhds x)ᵒᵖ) : Module (((OpenNhds.inclusion x).op ⋙ R).obj i)
+      (((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) := by
+    dsimp; infer_instance
+  Limits.IsColimit.module ((OpenNhds.inclusion x).op ⋙ R) ((OpenNhds.inclusion x).op ⋙ M.presheaf)
+    (fun f r m ↦ M.map_smul _ _ _) (Limits.colimit.isColimit _) (Limits.colimit.isColimit _)
+
+lemma germ_ringCat_smul (U : Opens X) (hx : x ∈ U) (r : R.obj (op U)) (m : M.obj (op U)) :
+    TopCat.Presheaf.germ M.presheaf U x hx (r • m) =
+      R.germ U x hx r • TopCat.Presheaf.germ M.presheaf U x hx m :=
+  letI (i : (OpenNhds x)ᵒᵖ) : Module (((OpenNhds.inclusion x).op ⋙ R).obj i)
+      (((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) := by
+    dsimp; infer_instance
+  Limits.IsColimit.ι_smul ((OpenNhds.inclusion x).op ⋙ R) ((OpenNhds.inclusion x).op ⋙ M.presheaf)
+    (fun f r m ↦ M.map_smul _ _ _)
+      (Limits.colimit.isColimit _) (Limits.colimit.isColimit _) ⟨_, _⟩ _ _
+
+section CommRingCat
+
+variable {X : TopCat.{u}} {R : X.Presheaf CommRingCat.{u}}
+  (M : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
+
+noncomputable
+instance (x : X) : Module (R.stalk x) ↑(TopCat.Presheaf.stalk M.presheaf x) :=
+  letI (i : (OpenNhds x)ᵒᵖ) : Module (((OpenNhds.inclusion x).op ⋙ R ⋙ forget₂ _ RingCat).obj i)
+      (((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) := by
+    dsimp; infer_instance
+  Limits.IsColimit.module ((OpenNhds.inclusion x).op ⋙ R ⋙ forget₂ _ _)
+    ((OpenNhds.inclusion x).op ⋙ M.presheaf)
+    (fun f r m ↦ M.map_smul _ _ _) (Limits.isColimitOfPreserves (forget₂ _ _)
+      (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ R))) (Limits.colimit.isColimit _)
+
+lemma germ_smul (x : X) (U : Opens X) (hx : x ∈ U) (r : R.obj (op U)) (m : M.obj (op U)) :
+    TopCat.Presheaf.germ M.presheaf U x hx (r • m) =
+      R.germ U x hx r • TopCat.Presheaf.germ M.presheaf U x hx m :=
+  letI (i : (OpenNhds x)ᵒᵖ) : Module (((OpenNhds.inclusion x).op ⋙ R ⋙ forget₂ _ RingCat).obj i)
+      (((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) := by
+    dsimp; infer_instance
+  Limits.IsColimit.ι_smul ((OpenNhds.inclusion x).op ⋙ R ⋙ forget₂ _ _)
+    ((OpenNhds.inclusion x).op ⋙ M.presheaf)
+    (fun f r m ↦ M.map_smul _ _ _) (Limits.isColimitOfPreserves (forget₂ _ _)
+      (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ R))) (Limits.colimit.isColimit _)
+      ⟨_, _⟩ _ _
+
+end CommRingCat
+
+end PresheafOfModules

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -163,6 +163,12 @@ instance hasForgetToAddCommMonCat : HasForget₂ SemiRingCat AddCommMonCat where
     { obj := fun R ↦ AddCommMonCat.of R
       map := fun f ↦ AddCommMonCat.ofHom f.hom.toAddMonoidHom }
 
+@[simp] lemma forget₂_monCat_map {R S : SemiRingCat} (f : R ⟶ S) (x) :
+    (forget₂ SemiRingCat MonCat).map f x = f x := rfl
+
+@[simp] lemma forget₂_addCommMonCat_map {R S : SemiRingCat} (f : R ⟶ S) (x) :
+    (forget₂ SemiRingCat AddCommMonCat).map f x = f x := rfl
+
 /-- Ring equivalences are isomorphisms in category of semirings -/
 @[simps]
 def _root_.RingEquiv.toSemiRingCatIso {R S : Type u} [Semiring R] [Semiring S] (e : R ≃+* S) :
@@ -314,6 +320,9 @@ instance hasForgetToSemiRingCat : HasForget₂ RingCat SemiRingCat where
     { obj := fun R ↦ SemiRingCat.of R
       map := fun f ↦ SemiRingCat.ofHom f.hom }
 
+@[simp] lemma forget₂_map {R S : RingCat} (f : R ⟶ S) (x) :
+    (forget₂ RingCat SemiRingCat).map f x = f x := rfl
+
 /-- The forgetful functor from `RingCat` to `SemiRingCat` is fully faithful. -/
 def fullyFaithfulForget₂ToSemiRingCat :
     (forget₂ RingCat SemiRingCat).FullyFaithful where

Mathlib/AlgebraicGeometry/Morphisms/Etale.lean

@@ -15,8 +15,13 @@ public import Mathlib.CategoryTheory.Limits.MorphismProperty
 
 # Étale morphisms
 
-A morphism of schemes `f : X ⟶ Y` is étale if it is smooth of relative dimension zero. We
-also define the category of schemes étale over `X`.
+A morphism of schemes `f : X ⟶ Y` is étale if for each affine `U ⊆ Y`
+and `V ⊆ f ⁻¹' U`, the induced map `Γ(Y, U) ⟶ Γ(X, V)` is étale.
+
+## Main results
+
+- `AlgebraicGeometry.Etale.iff_smoothOfRelativeDimension_zero`: Etale is equivalent to
+  smooth of relative dimension `0`.
 
 -/
 
@@ -30,35 +35,85 @@ open CategoryTheory MorphismProperty Limits
 
 namespace AlgebraicGeometry
 
-/-- A morphism of schemes is étale if it is smooth of relative dimension zero. -/
-abbrev Etale {X Y : Scheme.{u}} (f : X ⟶ Y) := SmoothOfRelativeDimension 0 f
+/-- A morphism of schemes `f : X ⟶ Y` is étale if for each affine `U ⊆ Y` and
+`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is étale. -/
+@[mk_iff]
+class Etale {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop where
+  etale_appLE (f) :
+    ∀ {U : Y.Opens} (_ : IsAffineOpen U) {V : X.Opens} (_ : IsAffineOpen V) (e : V ≤ f ⁻¹ᵁ U),
+      (f.appLE U V e).hom.Etale
+
+alias Scheme.Hom.etale_appLE := Etale.etale_appLE
 
 @[deprecated (since := "2026-02-09")] alias IsEtale := Etale
 
 namespace Etale
 
 variable {X Y : Scheme.{u}} (f : X ⟶ Y)
 
-instance [Etale f] : Smooth f :=
+/-- The property of scheme morphisms `Etale` is associated with the ring
+homomorphism property `Etale`. -/
+instance : HasRingHomProperty @Etale RingHom.Etale where
+  isLocal_ringHomProperty := RingHom.Etale.propertyIsLocal
+  eq_affineLocally' := by
+    ext X Y f
+    rw [etale_iff, affineLocally_iff_forall_isAffineOpen]
+
+/-- Being étale is multiplicative. -/
+instance : MorphismProperty.IsMultiplicative @Etale :=
+  HasRingHomProperty.isMultiplicative RingHom.Etale.stableUnderComposition
+    RingHom.Etale.containsIdentities
+
+/-- The composition of étale morphisms is étale. -/
+instance etale_comp {Z : Scheme.{u}} (g : Y ⟶ Z) [Etale f] [Etale g] :
+    Etale (f ≫ g) :=
+  MorphismProperty.comp_mem _ f g ‹Etale f› ‹Etale g›
+
+/-- Etale is stable under base change. -/
+instance etale_isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @Etale :=
+  HasRingHomProperty.isStableUnderBaseChange RingHom.Etale.isStableUnderBaseChange
+
+/-- Open immersions are étale. -/
+instance (priority := 900) [IsOpenImmersion f] : Etale f :=
+  HasRingHomProperty.of_isOpenImmersion RingHom.Etale.containsIdentities
+
+instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Etale g] :
+    Etale (pullback.fst f g) :=
+  MorphismProperty.pullback_fst f g inferInstance
+
+instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Etale f] :
+    Etale (pullback.snd f g) :=
+  MorphismProperty.pullback_snd f g inferInstance
+
+instance (f : X ⟶ Y) (V : Y.Opens) [Etale f] : Etale (f ∣_ V) :=
+  IsZariskiLocalAtTarget.restrict ‹_› V
+
+instance (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e) [Etale f] :
+    Etale (f.resLE V U e) := by
+  delta Scheme.Hom.resLE; infer_instance
+
+lemma eq_smoothOfRelativeDimension_zero : @Etale = @SmoothOfRelativeDimension 0 := by
+  apply HasRingHomProperty.ext
+  introv
+  have : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0 := by
+    ext; apply RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero
+  rw [← this, RingHom.locally_iff_of_localizationSpanTarget]
+  · exact RingHom.Etale.respectsIso
+  · exact RingHom.Etale.ofLocalizationSpanTarget
+
+lemma iff_smoothOfRelativeDimension_zero : Etale f ↔ SmoothOfRelativeDimension 0 f := by
+  rw [eq_smoothOfRelativeDimension_zero]
+
+instance [Etale f] : SmoothOfRelativeDimension 0 f := by
+  rwa [← iff_smoothOfRelativeDimension_zero]
+
+instance (priority := low) [Etale f] : Smooth f :=
   SmoothOfRelativeDimension.smooth 0 f
 
-instance : IsStableUnderBaseChange @Etale :=
-  smoothOfRelativeDimension_isStableUnderBaseChange 0
-
 open RingHom in
 instance (priority := 900) [Etale f] : FormallyUnramified f where
-  formallyUnramified_appLE {U} hU {V} hV e := by
-    have : Locally (IsStandardSmoothOfRelativeDimension 0) (f.appLE U V e).hom :=
-      HasRingHomProperty.appLE (P := @SmoothOfRelativeDimension 0) _
-        inferInstance ⟨U, hU⟩ ⟨V, hV⟩ _
-    have : Locally RingHom.FormallyUnramified (f.appLE U V e).hom := by
-      apply locally_of_locally _ this
-      intro R S _ _ f hf
-      algebraize [f]
-      rw [RingHom.FormallyUnramified]
-      infer_instance
-    rwa [← RingHom.locally_iff_of_localizationSpanTarget
-      FormallyUnramified.respectsIso FormallyUnramified.ofLocalizationSpanTarget]
+  formallyUnramified_appLE {_} hU {_} hV e :=
+    (f.etale_appLE hU hV e).formallyUnramified
 
 instance : MorphismProperty.HasOfPostcompProperty
     @Etale (@LocallyOfFiniteType ⊓ @FormallyUnramified) := by