awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : IsOpenImmersion (Y := pullback.diagonalObj (Spec.map φ)) (pullback.diagonal (Spec.map φ))
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u) →+* (↑S : Type u) :=
  AlgHom.toRingHom (Algebra.TensorProduct.lmul' (↑R : Type u))
hF :
  Function.Surjective (α := TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)) (β := (↑S : Type u))
    (⇑F : (a : TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)) → (↑S : Type u))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : (↑(CommRingCat.of (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))) : Type u)
he : IsIdempotentElem e
he' :
  Eq (α := Ideal (↑(CommRingCat.of (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F))) (Ideal.span {e})
x : (↑(CommRingCat.of (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))) : Type u)
hx :
  Membership.mem (γ := Ideal (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)))
    (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) (e * x)
⊢ (↑(Subtype.mk (p := fun (x : TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)) ↦
          Membership.mem (γ := Ideal (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)))
            (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) x)
          (e * x) hx) :
      TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)) ∈
    HPow.hPow (α := Ideal (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))) (β := ℕ)
      (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) 2
have rw : e * (e * x) ∈
  HMul.hMul (α := Ideal (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)))
    (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u))
Tactic: rw [pow_two, Subtype.coe_mk, ← he, mul_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
inst : FormallyUnramified (f_1 ≫ g_1)
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
g : S →+* T
H : (g.comp f).FormallyUnramified
⊢ g.FormallyUnramified
have algebraizeInst : Algebra.FormallyUnramified R T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
⊢ IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
      (hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R),
      IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f))
  (hX : ¬((∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R)),
  IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: wlog hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
        (hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R),
        IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f))
    (hX : ¬((∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R)),
    IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
  (hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R),
  IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: wlog hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
    (hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
hX : ¬((∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
⊢ IsOpenImmersion (Y := pullback.diagonalObj ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
    (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
have hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
Tactic: have hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
      comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
    (hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
hX : ¬((∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
⊢ IsOpenImmersion (Y := pullback.diagonalObj ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
    (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
have hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i))
Tactic: have hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
      comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have obtain : ∀ (S R : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [FormallyUnramified f] [LocallyOfFiniteType f],
  IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: obtain ⟨⟨S, rfl⟩, R, rfl⟩ := hX
Cleared hypotheses: X, Y, f, inst, inst_1, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S R : CommRingCat
f : Spec S ⟶ Spec R
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
⊢ IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have obtain : ∀ (f : R ⟶ S) [FormallyUnramified (Spec.map f)] [LocallyOfFiniteType (Spec.map f)],
  IsOpenImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f))
Tactic: obtain ⟨f, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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)
⊢ IsOpenImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f))
have inst : (CommRingCat.Hom.hom f).FormallyUnramified
Tactic: rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at *
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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
⊢ IsOpenImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f))
have inst₁ : (CommRingCat.Hom.hom f).FiniteType
Tactic: rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at *
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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
⊢ IsOpenImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f))
have algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [f.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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)
⊢ IsOpenImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f))
have algebraizeInst₁ : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [f.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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 (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f))
have 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)))))
Tactic: rw [show f = CommRingCat.ofHom (algebraMap R S) from rfl, diagonal_SpecMap R S,
    cancel_right_of_respectsIso (P := @IsOpenImmersion)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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
⊢ Algebra.IsSeparable.{u, u} (↑(Y.residueField (f x)) : Type u) (↑(X.residueField x) : Type u)
have 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))
Tactic: have : IsLocalHom (algebraMap (Y.presheaf.stalk (f x)) (X.presheaf.stalk x)) :=
    inferInstanceAs <| IsLocalHom (f.stalkMap x).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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} (↑(Y.residueField (f x)) : Type u) (↑(X.residueField x) : Type u)
have 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
Tactic: convert! h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
have 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))
Tactic: refine Algebra.algebra_ext _ _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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.IsSeparable.{u, u} (↑(Y.residueField (f x)) : Type u) (↑(X.residueField x) : Type u)
have suffices : Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
  (IsLocalRing.ResidueField (↑(X.presheaf.stalk 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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)
have rw : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType
Tactic: rw [← RingHom.essFiniteType_algebraMap, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))
have this₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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)
have rw : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallyUnramified
Tactic: rw [← RingHom.formallyUnramified_algebraMap, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x) : Type u))
have this₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
⊢ IsDominant i
have obtain : ∀ (n : ℕ) (hn : Scheme.Hom.ker i ^ n = 0), IsDominant i
Tactic: obtain ⟨n, hn⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
⊢ IsDominant i
have rw : (↑(0 * Scheme.Hom.ker i).support : Set ↥Z) = Set.univ
Tactic: rw [isDominant_iff, denseRange_iff_closure_range, ← i.support_ker,
      ← i.ker.support_pow (n + 1) (by simp), pow_succ, hn]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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
⊢ g₁ = g₂
have this : IsDominant i
Tactic: have : IsDominant i := by
    obtain ⟨n, hn⟩ := hi
    rw [isDominant_iff, denseRange_iff_closure_range, ← i.support_ker,
      ← i.ker.support_pow (n + 1) (by simp), pow_succ, hn]
    simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
this : IsDominant i
⊢ g₁ = g₂
have refine : ∀ (x : ↥Z), ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
Tactic: refine Scheme.hom_ext_of_forall _ _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
this : IsDominant i
x : ↥Z
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
have obtain : ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)),
  ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f (g₁ x))) isOpen_univ