awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
x : (↑(CommRingCat.of S) : Type u)
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (AlgHom.toRingHom (TensorProduct.lmul' R))) :
        (a : (↑(CommRingCat.of (TensorProduct R S S)) : Type u)) → (↑(CommRingCat.of S) : Type u))
      (1 ⊗ₜ[R] x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
rw :
  ∃ (e : (↑(CommRingCat.of (TensorProduct R S S)) : Type u)),
    IsIdempotentElem e ∧
      Eq (α := Ideal (↑(CommRingCat.of (TensorProduct R S S)) : Type u))
        (RingHom.ker (F := (↑(CommRingCat.of (TensorProduct R S S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
          (CommRingCat.Hom.hom (CommRingCat.ofHom (AlgHom.toRingHom (TensorProduct.lmul' R)))))
        (Ideal.span {e})
⊢ IsOpenImmersion.{u} (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of (TensorProduct R S S)))
    (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (TensorProduct.lmul' R))))

Tactic:
rw [isOpenImmersion_SpecMap_iff_of_surjective _ (fun x ↦ ⟨1 ⊗ₜ x, by simp⟩)]

Premises used: AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
apply : IsIdempotentElem (M := Ideal (TensorProduct R S S)) (KaehlerDifferential.ideal R S)
⊢ ∃ (e : (↑(CommRingCat.of (TensorProduct R S S)) : Type u)),
    IsIdempotentElem e ∧
      Eq (α := Ideal (↑(CommRingCat.of (TensorProduct R S S)) : Type u))
        (RingHom.ker (F := (↑(CommRingCat.of (TensorProduct R S S)) : Type u) →+* (↑(CommRingCat.of S) : Type u))
          (CommRingCat.Hom.hom (CommRingCat.ofHom (AlgHom.toRingHom (TensorProduct.lmul' R)))))
        (Ideal.span {e})

Tactic:
apply (Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)).mp

Premises used: KaehlerDifferential.ideal_fg, Ideal.isIdempotentElem_iff_of_fg, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
apply : Subsingleton.{u + 1} (Ideal.Cotangent (R := TensorProduct R S S) (KaehlerDifferential.ideal R S))
⊢ IsIdempotentElem (M := Ideal (TensorProduct R S S)) (KaehlerDifferential.ideal R S)

Tactic:
apply (Ideal.cotangent_subsingleton_iff _).mp

Premises used: Iff.mp, Ideal.cotangent_subsingleton_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
⊢ Subsingleton.{u + 1} (Ideal.Cotangent (R := TensorProduct R S S) (KaehlerDifferential.ideal R S))

Tactic:
inferInstanceAs <| Subsingleton Ω[S⁄R]

Premises used: _private.0.Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul._proof_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
⊢ Subsingleton.{u + 1} (Ideal.Cotangent (R := TensorProduct R S S) (KaehlerDifferential.ideal R S))

Tactic:
exact inferInstanceAs <| Subsingleton Ω[S⁄R]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    FormallyUnramified f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified) f
⊢ @FormallyUnramified = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified) f
h₁ h₂ :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified
⊢ FormallyUnramified f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified) f

Tactic:
rw [formallyUnramified_iff, affineLocally_iff_forall_isAffineOpen]

Premises used: AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.formallyUnramified_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderComposition @FormallyUnramified

Tactic:
HasRingHomProperty.stableUnderComposition RingHom.FormallyUnramified.stableUnderComposition

Premises used: RingHom.FormallyUnramified.stableUnderComposition, AlgebraicGeometry.HasRingHomProperty.stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), FormallyUnramified f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), FormallyUnramified f
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), FormallyUnramified f
⊢ FormallyUnramified f

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), FormallyUnramified f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    FormallyUnramified (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ FormallyUnramified f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @FormallyUnramified) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), FormallyUnramified f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ IsOpenImmersion (X := pullback f (Y.affineCover.f i)) (Y :=
    pullback.diagonalObj (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)))
    (pullback.diagonal (pullback.snd f (Y.affineCover.f i)))

Tactic:
have inst : IsOpenImmersion (pullback.diagonal (pullback.snd f (Y.affineCover.f i))) :=
      MorphismProperty.pullback_snd (P := .diagonal @IsOpenImmersion) _ _ ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), FormallyUnramified f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
inst :
  IsOpenImmersion (X := pullback f (Y.affineCover.f i)) (Y :=
    pullback.diagonalObj (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)))
    (pullback.diagonal (pullback.snd f (Y.affineCover.f i)))
⊢ FormallyUnramified (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
this (pullback.snd _ _) ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.limit, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), FormallyUnramified f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
inst :
  IsOpenImmersion (X := pullback f (Y.affineCover.f i)) (Y :=
    pullback.diagonalObj (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)))
    (pullback.diagonal (pullback.snd f (Y.affineCover.f i)))
⊢ FormallyUnramified (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
exact this (pullback.snd _ _) ⟨_, rfl⟩

Premises used: CategoryTheory.Limits.pullback.snd, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)],
    FormallyUnramified f
⊢ FormallyUnramified f

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), FormallyUnramified f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), FormallyUnramified f
wlog :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), FormallyUnramified f
⊢ FormallyUnramified f

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), FormallyUnramified f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inr : ∀ (i : X.affineCover.I₀), FormallyUnramified (X.affineCover.f i ≫ f)
⊢ FormallyUnramified f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := @FormallyUnramified) X.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), FormallyUnramified f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
⊢ IsOpenImmersion (Y := pullback.diagonalObj (X.affineCover.f i ≫ f)) (pullback.diagonal (X.affineCover.f i ≫ f))

Tactic:
have inst : IsOpenImmersion (pullback.diagonal (X.affineCover.f i ≫ f)) :=
      MorphismProperty.comp_mem (.diagonal @IsOpenImmersion) _ _
        (inferInstanceAs (IsOpenImmersion _)) ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), FormallyUnramified f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
inst : IsOpenImmersion (Y := pullback.diagonalObj (X.affineCover.f i ≫ f)) (pullback.diagonal (X.affineCover.f i ≫ f))
⊢ FormallyUnramified (X.affineCover.f i ≫ f)

Tactic:
this (_ ≫ _) ⟨_, rfl⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst_1 : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), FormallyUnramified f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
inst : IsOpenImmersion (Y := pullback.diagonalObj (X.affineCover.f i ≫ f)) (pullback.diagonal (X.affineCover.f i ≫ f))
⊢ FormallyUnramified (X.affineCover.f i ≫ f)

Tactic:
exact this (_ ≫ _) ⟨_, rfl⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)],
    FormallyUnramified f
⊢ FormallyUnramified f

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f_1 : X ⟶ Y
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
obtain :
  ∀ (φ : R ⟶ S) [IsOpenImmersion (Y := pullback.diagonalObj (Spec.map φ)) (pullback.diagonal (Spec.map φ))],
    FormallyUnramified (Spec.map φ)
⊢ FormallyUnramified f

Tactic:
obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f

Premises used: AlgebraicGeometry.Spec.homEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : IsOpenImmersion (Y := pullback.diagonalObj (Spec.map φ)) (pullback.diagonal (Spec.map φ))
rw : (CommRingCat.Hom.hom φ).FormallyUnramified
⊢ FormallyUnramified (Spec.map φ)

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified)]

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
x : (↑S : Type u)
⊢ (F : (a : TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)) → (↑S : Type u))
      ((((TensorProduct.mk (↑R : Type u) (↑S : Type u) (↑S : Type u) :
                (a : (↑S : Type u)) →
                  (↑S : Type u) →ₗ[(↑R : Type u)] TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))
              x :
            LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑S : Type u)
              (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))) :
          (a : (↑S : Type u)) → TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))
        1) =
    x

Tactic:
simp [F]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
⊢ 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))

Tactic:
have hF : Function.Surjective F := fun x ↦ ⟨.mk _ _ _ x 1, by simp [F]⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
rwa :
  IsOpenImmersion (Spec.map (CommRingCat.ofHom F) ≫ Iso.inv (pullbackSpecIso (↑R : Type u) (↑S : Type u) (↑S : Type u)))
rwa₁ rwa₂ rwa₃ rwa₄ :
  IsOpenImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (Y :=
    pullback (X := Spec (CommRingCat.of (↑S : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
      Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
    (pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom F))

Tactic:
rwa [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _
      (pullbackSpecIso R S S).inv, ← AlgebraicGeometry.diagonal_SpecMap R S]

Premises used: AlgebraicGeometry.diagonal_SpecMap, CommRingCat.carrier, AlgebraicGeometry.pullbackSpecIso, AlgebraicGeometry.IsOpenImmersion, CategoryTheory.Iso.inv, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom F))

Tactic:
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom F)) := by
    rwa [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _
      (pullbackSpecIso R S S).inv, ← AlgebraicGeometry.diagonal_SpecMap R S]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
obtain :
  ∀ (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})),
    (CommRingCat.Hom.hom φ).FormallyUnramified
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified

Tactic:
obtain ⟨e, he, he'⟩ := (isOpenImmersion_SpecMap_iff_of_surjective _ hF).mp this

Premises used: AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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})
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified

Tactic:
⟨subsingleton_of_forall_eq 0 fun x ↦ ?_⟩

Premises used: Algebra.FormallyUnramified.mk, subsingleton_of_forall_eq, OfNat.ofNat, RingHom.FormallyUnramified
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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})
refine : ∀ (x : Ω[(↑S : Type u)⁄(↑R : Type u)]), x = 0
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified

Tactic:
refine ⟨subsingleton_of_forall_eq 0 fun x ↦ ?_⟩