awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst : FormallyUnramified (Spec.map f)
inst_1 : LocallyOfFiniteType (Spec.map f)
⊢ (CommRingCat.Hom.hom f).FormallyUnramified

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at *

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst_1 : FormallyUnramified (Spec.map f)
inst_2 : LocallyOfFiniteType (Spec.map f)
inst : (CommRingCat.Hom.hom f).FormallyUnramified
⊢ (CommRingCat.Hom.hom f).FiniteType

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at *

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst : (CommRingCat.Hom.hom f).FormallyUnramified
inst_1 : (CommRingCat.Hom.hom f).FiniteType
⊢ Algebra.FormallyUnramified.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [f.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst : (CommRingCat.Hom.hom f).FormallyUnramified
inst_1 : (CommRingCat.Hom.hom f).FiniteType
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑R : Type u) (↑S : Type u)
⊢ Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [f.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst : (CommRingCat.Hom.hom f).FormallyUnramified
inst_1 : (CommRingCat.Hom.hom f).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
rw :
  IsOpenImmersion.{u} (X := Spec S) (Y :=
    Spec (CommRingCat.of (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))))
    (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' (↑R : Type u)))))
⊢ IsOpenImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f))

Tactic:
rw [show f = CommRingCat.ofHom (algebraMap R S) from rfl, diagonal_SpecMap R S,
    cancel_right_of_respectsIso (P := @IsOpenImmersion)]

Premises used: AlgebraicGeometry.diagonal_SpecMap, CommRingCat.carrier, AlgebraicGeometry.IsOpenImmersion, rfl, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst : (CommRingCat.Hom.hom f).FormallyUnramified
inst_1 : (CommRingCat.Hom.hom f).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsOpenImmersion.{u} (X := Spec S) (Y :=
    Spec (CommRingCat.of (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))))
    (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' (↑R : Type u)))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
⊢ IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))

Tactic:
have : IsLocalHom (algebraMap (Y.presheaf.stalk (f x)) (X.presheaf.stalk x)) :=
    inferInstanceAs <| IsLocalHom (f.stalkMap x).hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
h :
  Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))
⊢ Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))

Tactic:
h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
h :
  Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))
h₁ :
  (↑(Y.residueField (f x)) : Type u) = IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u) →
    (↑(X.residueField x) : Type u) = IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u) →
      HEq.{u + 1} (α := CommRing (↑(Y.residueField (f x)) : Type u))
          (CommRingCat.instCommRingObjForgetRingHomCarrier :
            CommRing
              (Functor.obj
                (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier))
                (Y.residueField (f x))))
          (β := CommRing (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u)))
          (IsLocalRing.instCommRingResidueField (↑(Y.presheaf.stalk (f x)) : Type u)) →
        HEq.{u + 1} (α := Ring (↑(X.residueField x) : Type u)) DivisionRing.toRing (β :=
            Ring (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))) DivisionRing.toRing →
          (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra = IsLocalRing.ResidueField.instAlgebra
⊢ Algebra.IsSeparable.{u, u} (↑(Y.residueField (f x)) : Type u) (↑(X.residueField x) : Type u)

Tactic:
convert! h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
h :
  Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))
e_1 : (↑(Y.residueField (f x)) : Type u) = IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u)
e_2 : (↑(X.residueField x) : Type u) = IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u)
e_3 :
  HEq.{u + 1} (α := CommRing (↑(Y.residueField (f x)) : Type u))
    (CommRingCat.instCommRingObjForgetRingHomCarrier :
      CommRing
        (Functor.obj
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Y.residueField (f x))))
    (β := CommRing (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u)))
    (IsLocalRing.instCommRingResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
e_4 :
  HEq.{u + 1} (α := Ring (↑(X.residueField x) : Type u)) DivisionRing.toRing (β :=
    Ring (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))) DivisionRing.toRing
⊢ (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra = IsLocalRing.ResidueField.instAlgebra

Tactic:
Algebra.algebra_ext _ _ fun x ↦ ?_

Premises used: Algebra.algebra_ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
h :
  Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))
e_1 : (↑(Y.residueField (f x)) : Type u) = IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u)
e_2 : (↑(X.residueField x) : Type u) = IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u)
e_3 :
  HEq.{u + 1} (α := CommRing (↑(Y.residueField (f x)) : Type u))
    (CommRingCat.instCommRingObjForgetRingHomCarrier :
      CommRing
        (Functor.obj
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Y.residueField (f x))))
    (β := CommRing (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u)))
    (IsLocalRing.instCommRingResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
e_4 :
  HEq.{u + 1} (α := Ring (↑(X.residueField x) : Type u)) DivisionRing.toRing (β :=
    Ring (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))) DivisionRing.toRing
h₁ :
  ∀ (x_1 : (↑(Y.residueField (f x)) : Type u)),
    Eq (α := (↑(X.residueField x) : Type u))
      ((algebraMap (↑(Y.residueField (f x)) : Type u) (↑(X.residueField x) : Type u) :
            (a : (↑(Y.residueField (f x)) : Type u)) → (↑(X.residueField x) : Type u))
          x_1 :
        (↑(X.residueField x) : Type u))
      ((algebraMap (↑(Y.residueField (f x)) : Type u) (↑(X.residueField x) : Type u) :
            (a : (↑(Y.residueField (f x)) : Type u)) → (↑(X.residueField x) : Type u))
          x_1 :
        (↑(X.residueField x) : Type u))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra = IsLocalRing.ResidueField.instAlgebra

Tactic:
refine Algebra.algebra_ext _ _ fun x ↦ ?_

Premises used: Algebra.algebra_ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x_1 : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x_1)) : Type u) (↑(X.presheaf.stalk x_1) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x_1)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x_1)) : Type u)) (S := (↑(X.presheaf.stalk x_1) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x_1)) : Type u) →+* (↑(X.presheaf.stalk x_1) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x_1)) : Type u) (↑(X.presheaf.stalk x_1) : Type u))
h :
  Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x_1) : Type u))
e_1 : (↑(Y.residueField (f x_1)) : Type u) = IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u)
e_2 : (↑(X.residueField x_1) : Type u) = IsLocalRing.ResidueField (↑(X.presheaf.stalk x_1) : Type u)
e_3 :
  HEq.{u + 1} (α := CommRing (↑(Y.residueField (f x_1)) : Type u))
    (CommRingCat.instCommRingObjForgetRingHomCarrier :
      CommRing
        (Functor.obj
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Y.residueField (f x_1))))
    (β := CommRing (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u)))
    (IsLocalRing.instCommRingResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
e_4 :
  HEq.{u + 1} (α := Ring (↑(X.residueField x_1) : Type u)) DivisionRing.toRing (β :=
    Ring (IsLocalRing.ResidueField (↑(X.presheaf.stalk x_1) : Type u))) DivisionRing.toRing
x : (↑(Y.presheaf.stalk (f x_1)) : Type u)
⊢ Eq (α := (↑(X.residueField x_1) : Type u))
    ((algebraMap (↑(Y.residueField (f x_1)) : Type u) (↑(X.residueField x_1) : Type u) :
          (a : (↑(Y.residueField (f x_1)) : Type u)) → (↑(X.residueField x_1) : Type u))
        ((IsLocalRing.residue (↑(Y.presheaf.stalk (f x_1)) : Type u) :
            (a : (↑(Y.presheaf.stalk (f x_1)) : Type u)) →
              IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
          x) :
      (↑(X.residueField x_1) : Type u))
    ((algebraMap (↑(Y.residueField (f x_1)) : Type u) (↑(X.residueField x_1) : Type u) :
          (a : (↑(Y.residueField (f x_1)) : Type u)) → (↑(X.residueField x_1) : Type u))
        ((IsLocalRing.residue (↑(Y.presheaf.stalk (f x_1)) : Type u) :
            (a : (↑(Y.presheaf.stalk (f x_1)) : Type u)) →
              IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
          x) :
      (↑(X.residueField x_1) : Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
suffices :
  Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))
⊢ Algebra.IsSeparable.{u, u} (↑(Y.residueField (f x)) : Type u) (↑(X.residueField x) : Type u)

Tactic:
suffices h : Algebra.IsSeparable
      (IsLocalRing.ResidueField <| Y.presheaf.stalk (f x))
      (IsLocalRing.ResidueField <| X.presheaf.stalk x) by
    convert! h
    refine Algebra.algebra_ext _ _ fun x ↦ ?_
    obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
    rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
rw : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType
⊢ Algebra.EssFiniteType.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)

Tactic:
rw [← RingHom.essFiniteType_algebraMap, RingHom.algebraMap_toAlgebra]

Premises used: RingHom.essFiniteType_algebraMap, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType

Tactic:
LocallyOfFiniteType.stalkMap f x

Premises used: AlgebraicGeometry.LocallyOfFiniteType.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType

Tactic:
exact LocallyOfFiniteType.stalkMap f x

Premises used: AlgebraicGeometry.LocallyOfFiniteType.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
⊢ Algebra.EssFiniteType.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)

Tactic:
have : Algebra.EssFiniteType (Y.presheaf.stalk (f x)) (X.presheaf.stalk x) := by
    rw [← RingHom.essFiniteType_algebraMap, RingHom.algebraMap_toAlgebra]
    exact LocallyOfFiniteType.stalkMap f x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this_1 :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
this : Algebra.EssFiniteType.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)
rw : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallyUnramified
⊢ Algebra.FormallyUnramified.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)

Tactic:
rw [← RingHom.formallyUnramified_algebraMap, RingHom.algebraMap_toAlgebra]

Premises used: RingHom.formallyUnramified_algebraMap, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this_1 :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
this : Algebra.EssFiniteType.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallyUnramified

Tactic:
stalkMap f x

Premises used: AlgebraicGeometry.FormallyUnramified.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this_1 :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
this : Algebra.EssFiniteType.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallyUnramified

Tactic:
exact stalkMap f x

Premises used: AlgebraicGeometry.FormallyUnramified.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this_1 :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
this : Algebra.EssFiniteType.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)
⊢ Algebra.FormallyUnramified.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)

Tactic:
have : Algebra.FormallyUnramified (Y.presheaf.stalk (f x)) (X.presheaf.stalk x) := by
    rw [← RingHom.formallyUnramified_algebraMap, RingHom.algebraMap_toAlgebra]
    exact stalkMap f x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this_1 :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u))
this_2 : Algebra.EssFiniteType.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)
this : Algebra.FormallyUnramified.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)
⊢ Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
obtain : ∀ (n : ℕ) (hn : Scheme.Hom.ker i ^ n = 0), IsDominant i
⊢ IsDominant i

Tactic:
obtain ⟨n, hn⟩ := hi
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ n + 1 ≠ 0

Tactic:
simp