awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ FormallyUnramified f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified) f
have 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
Tactic: rw [formallyUnramified_iff, affineLocally_iff_forall_isAffineOpen]
-- 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
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
⊢ FormallyUnramified f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified) f
have 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
Tactic: rw [formallyUnramified_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ FormallyUnramified f
have 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
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
⊢ FormallyUnramified f
have 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
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
⊢ FormallyUnramified f
have 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)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @FormallyUnramified) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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
⊢ 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)
have 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)))
Tactic: have inst : IsOpenImmersion (pullback.diagonal (pullback.snd f (Y.affineCover.f i))) :=
      MorphismProperty.pullback_snd (P := .diagonal @IsOpenImmersion) _ _ ‹_›
-- 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 : IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ FormallyUnramified f
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)],
  FormallyUnramified f
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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)
⊢ FormallyUnramified f
have 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
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
⊢ FormallyUnramified f
have 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
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
Cleared hypotheses: X, f, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
⊢ FormallyUnramified f
have inr : ∀ (i : X.affineCover.I₀), FormallyUnramified (X.affineCover.f i ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := @FormallyUnramified) X.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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₀
⊢ FormallyUnramified (X.affineCover.f i ≫ f)
have inst : 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 _)) ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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
⊢ FormallyUnramified f
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)],
  FormallyUnramified f
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
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)
⊢ FormallyUnramified f
have obtain : ∀ (φ : R ⟶ S) [IsOpenImmersion (Y := pullback.diagonalObj (Spec.map φ)) (pullback.diagonal (Spec.map φ))],
  FormallyUnramified (Spec.map φ)
Tactic: obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f
Cleared hypotheses: f, inst
-- 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 φ))
⊢ FormallyUnramified (Spec.map φ)
have rw : (CommRingCat.Hom.hom φ).FormallyUnramified
Tactic: rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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))
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified
have 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))
Tactic: have hF : Function.Surjective F := fun x ↦ ⟨.mk _ _ _ x 1, by simp [F]⟩
-- 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))
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
have rwa : IsOpenImmersion (Spec.map (CommRingCat.ofHom F) ≫ Iso.inv (pullbackSpecIso (↑R : Type u) (↑S : Type u) (↑S : Type u)))
Tactic: rwa [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _
      (pullbackSpecIso R S S).inv, ← AlgebraicGeometry.diagonal_SpecMap R S]
-- 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))
rwa :
  IsOpenImmersion (Spec.map (CommRingCat.ofHom F) ≫ Iso.inv (pullbackSpecIso (↑R : Type u) (↑S : Type u) (↑S : Type u)))
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
have 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)))))
Tactic: rwa [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _
      (pullbackSpecIso R S S).inv, ← AlgebraicGeometry.diagonal_SpecMap R S]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (hypothesis)
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))
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified
have this : 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]
-- 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))
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified
have 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
Tactic: obtain ⟨e, he, he'⟩ := (isOpenImmersion_SpecMap_iff_of_surjective _ hF).mp this
-- 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})
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified
have refine : ∀ (x : Ω[(↑S : Type u)⁄(↑R : Type u)]), x = 0
Tactic: refine ⟨subsingleton_of_forall_eq 0 fun x ↦ ?_⟩
-- 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 : Ω[(↑S : Type u)⁄(↑R : Type u)]
⊢ x = 0
have obtain : ∀ (x : TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))
  (hx :
    Membership.mem (γ := Ideal (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)))
      (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) x),
  Eq (α := Ω[(↑S : Type u)⁄(↑R : Type u)])
    ((Ideal.toCotangent (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) :
          (a : ↥(KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u))) →
            (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)).Cotangent)
        (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)
          x hx) :
      Ideal.Cotangent (R := TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))
        (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)))
    (0 : Ω[(↑S : Type u)⁄(↑R : Type u)])
Tactic: obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
Cleared hypotheses: x
-- 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 : TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)
hx :
  Membership.mem (γ := Ideal (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u)))
    (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) x
⊢ Eq (α := Ω[(↑S : Type u)⁄(↑R : Type u)])
    ((Ideal.toCotangent (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) :
          (a : ↥(KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u))) →
            (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)).Cotangent)
        (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)
          x hx) :
      Ideal.Cotangent (R := TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))
        (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)))
    (0 : Ω[(↑S : Type u)⁄(↑R : Type u)])
have obtain : ∀ (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)),
  Eq (α := Ω[(↑S : Type u)⁄(↑R : Type u)])
    ((Ideal.toCotangent (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) :
          (a : ↥(KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u))) →
            (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)).Cotangent)
        (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) :
      Ideal.Cotangent (R := TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))
        (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)))
    (0 : Ω[(↑S : Type u)⁄(↑R : Type u)])
Tactic: obtain ⟨x, rfl⟩ := Ideal.mem_span_singleton.mp (he'.le hx)
Cleared hypotheses: x, hx
-- 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)
⊢ Eq (α := Ω[(↑S : Type u)⁄(↑R : Type u)])
    ((Ideal.toCotangent (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)) :
          (a : ↥(KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u))) →
            (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)).Cotangent)
        (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) :
      Ideal.Cotangent (R := TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))
        (KaehlerDifferential.ideal (↑R : Type u) (↑S : Type u)))
    (0 : Ω[(↑S : Type u)⁄(↑R : Type u)])
have refine : (↑(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
Tactic: refine (Ideal.toCotangent_eq_zero _ _).mpr ?_