awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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})
x : Ω[(↑S : Type u)⁄(↑R : Type u)]
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)])
⊢ x = 0

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x

Premises used: Ideal.toCotangent_surjective, 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 φ))
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
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)])
⊢ 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, rfl⟩ := Ideal.mem_span_singleton.mp (he'.le hx)

Premises used: Eq.le, Iff.mp, Ideal.mem_span_singleton, 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 φ))
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)])

Tactic:
(Ideal.toCotangent_eq_zero _ _).mpr ?_

Premises used: Iff.mpr, Ideal.toCotangent_eq_zero, KaehlerDifferential
-- 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})
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)
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
⊢ 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:
refine (Ideal.toCotangent_eq_zero _ _).mpr ?_

Premises used: Iff.mpr, Ideal.toCotangent_eq_zero
-- 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})
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)
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))
⊢ (↑(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:
rw [pow_two, Subtype.coe_mk, ← he, mul_assoc]

Premises used: Subtype.coe_mk, pow_two, mul_assoc
-- 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})
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)
⊢ 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:
Ideal.mul_mem_mul (he'.ge (Ideal.mem_span_singleton_self e)) hx

Premises used: Eq.ge, Set.Mem, Ideal.mul_mem_mul, Ideal.mem_span_singleton_self
-- 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})
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)
⊢ 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:
exact Ideal.mul_mem_mul (he'.ge (Ideal.mem_span_singleton_self e)) hx

Premises used: Eq.ge, Ideal.mul_mem_mul, Ideal.mem_span_singleton_self
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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
⊢ Algebra.FormallyUnramified R T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallyUnramified R T
⊢ g.FormallyUnramified

Tactic:
Algebra.FormallyUnramified.of_restrictScalars R S T

Premises used: Algebra.FormallyUnramified.of_restrictScalars, RingHom.FormallyUnramified
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallyUnramified R T
⊢ g.FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.of_restrictScalars R S T

Premises used: Algebra.FormallyUnramified.of_restrictScalars
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderBaseChange @FormallyUnramified

Tactic:
HasRingHomProperty.isStableUnderBaseChange RingHom.FormallyUnramified.isStableUnderBaseChange

Premises used: RingHom.FormallyUnramified.isStableUnderBaseChange, AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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)
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)
⊢ IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
wlog hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R

Premises used: AlgebraicGeometry.Spec, Exists, Eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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₀
⊢ 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)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
⊢ 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)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
hfin : LocallyOfFiniteType ((𝒰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)))

Tactic:
this _ ⟨⟨_, rfl⟩, ⟨_, rfl⟩⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
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))
hfin : LocallyOfFiniteType ((𝒰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)))

Tactic:
exact this _ ⟨⟨_, rfl⟩, ⟨_, rfl⟩⟩

Premises used: And.intro, 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 : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (S R : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [FormallyUnramified f] [LocallyOfFiniteType f],
    IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
obtain ⟨⟨S, rfl⟩, R, rfl⟩ := hX

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

Tactic:
obtain ⟨f, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl