awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : IsReduced X
⊢ IsReduced Y

Tactic:
⟨fun _ ↦ isReduced_of_injective _ (f.app_injective _)⟩

Premises used: isReduced_of_injective, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.IsReduced.mk, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Hom.app_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
rw : Scheme.Hom.ker (X := pullback f g) (pullback.snd f g) = ⊥
⊢ IsSchemeTheoreticallyDominant (X := pullback f g) (pullback.snd f g)

Tactic:
rw [isSchemeTheoreticallyDominant_iff]

Premises used: AlgebraicGeometry.isSchemeTheoreticallyDominant_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
U :
  { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
    x.1 ∈ Y.affineOpens ∧
      x.1 ≤
        (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
            (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
          (↑x.2 : TopologicalSpace.Opens ↥S) }
⊢ (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 ∈ Y.affineOpens

Tactic:
U.2.1

Premises used: Set.Mem, And.left, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
U :
  { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
    x.1 ∈ Y.affineOpens ∧
      x.1 ≤
        (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
            (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
          (↑x.2 : TopologicalSpace.Opens ↥S) }
⊢ (↑U : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 ∈ Y.affineOpens

Tactic:
exact U.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
grw : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₁ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₂ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
grw₃ : LE.le (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U)
grw₄ grw₅ : LE.le (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U)
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)

Tactic:
grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Limits.pullback.condition, right_eq_inf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
⊢ Mono (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)

Tactic:
have := mono_pushoutSection_of_isCompact_of_flat_right
    (.of_hasPullback f g) (UY := pullback.snd f g ⁻¹ᵁ V) hVU le_rfl (by
      grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]) hU hV (f.isCompact_preimage hU.isCompact)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
this : Mono (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ Function.Injective (α := (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
    (β := (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)) :
      (a : (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) →
        (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))

Tactic:
rw [@ConcreteCategory.mono_iff_injective_of_preservesPullback] at this

Premises used: CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
h𝒰 : TopologicalSpace.IsOpenCover (X := ↥Y)
  fun
    (V :
      { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1) //
        x.1 ∈ Y.affineOpens ∧
          x.1 ≤
            (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base) :
                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
              (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
  (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u_1)).1 :=
  ⋯
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥S) ↦ x ∈ S.affineOpens) U hU).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : (↑Γ(Y, V) : Type u_1)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, V) : Type u_1) (↑Γ(Y, V) : Type u_1))
    (RingHom.ker (F := (↑Γ(Y, V) : Type u_1) →+* (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
      (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V)))
    x
this :
  Function.Injective (α := (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1))
    (β := (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)) :
      (a : (↑(pushout (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU)) : Type u_1)) →
        (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u_1))
⊢ Function.Injective (α := (↑Γ(S, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)) :
      (a : (↑Γ(S, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))

Tactic:
simpa [Scheme.Hom.appLE] using f.app_injective U

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.app_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y Z S : Scheme
f : X ⟶ S
g : Y ⟶ S
pX : Z ⟶ X
pY : Z ⟶ Y
H : IsPullback pX pY f g
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
rw : IsSchemeTheoreticallyDominant (CategoryStruct.comp (Y := pullback f g) (Iso.hom H.isoPullback) (pullback.snd f g))
⊢ IsSchemeTheoreticallyDominant pY

Tactic:
rw [← H.isoPullback_hom_snd]

Premises used: CategoryTheory.IsPullback.isoPullback_hom_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y Z S : Scheme
f : X ⟶ S
g : Y ⟶ S
pX : Z ⟶ X
pY : Z ⟶ Y
H : IsPullback pX pY f g
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
inst_2 : Flat g
⊢ IsSchemeTheoreticallyDominant (CategoryStruct.comp (Y := pullback f g) (Iso.hom H.isoPullback) (pullback.snd f g))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant g
inst_1 : QuasiCompact g
inst_2 : Flat f
⊢ IsSchemeTheoreticallyDominant (X := pullback f g) (pullback.fst f g)

Tactic:
.of_isPullback (.flip <| .of_hasPullback _ _)

Premises used: CategoryTheory.IsPullback.flip, AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsSeparated x_2 ↔ MorphismProperty.diagonal (@IsClosedImmersion) x_2
⊢ @IsSeparated = MorphismProperty.diagonal @IsClosedImmersion

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsSeparated x_2 ↔ MorphismProperty.diagonal (@IsClosedImmersion) x_2

Tactic:
isSeparated_iff _

Premises used: CategoryTheory.MorphismProperty.diagonal, AlgebraicGeometry.isSeparated_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsSeparated x_2 ↔ MorphismProperty.diagonal (@IsClosedImmersion) x_2

Tactic:
exact isSeparated_iff _

Premises used: AlgebraicGeometry.isSeparated_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (MorphismProperty.diagonal @IsClosedImmersion).RespectsIso
⊢ MorphismProperty.RespectsIso @IsSeparated

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]

Premises used: AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (MorphismProperty.diagonal @IsClosedImmersion).RespectsIso

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderComposition
⊢ MorphismProperty.IsStableUnderComposition @IsSeparated

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]

Premises used: AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderComposition

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated f
inst_1 : IsSeparated g
⊢ IsSeparated (f ≫ g)

Tactic:
stableUnderComposition.comp_mem f g inferInstance inferInstance

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderBaseChange
⊢ MorphismProperty.IsStableUnderBaseChange @IsSeparated

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]

Premises used: AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderBaseChange

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : IsZariskiLocalAtTarget.{u_1} (MorphismProperty.diagonal @IsClosedImmersion)
⊢ IsZariskiLocalAtTarget @IsSeparated

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]

Premises used: AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget.{u_1} (MorphismProperty.diagonal @IsClosedImmersion)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSeparated g
⊢ IsSeparated (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSeparated f
⊢ IsSeparated (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
V : Y.Opens
inst : IsSeparated f
⊢ IsSeparated (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : IsSeparated f
⊢ IsSeparated (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
isClosedImmersion_diagonal :
  autoParam (IsClosedImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f)))
    IsSeparated.isClosedImmersion_diagonal._autoParam
⊢ IsSeparated (Spec.map f)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
isClosedImmersion_diagonal :
  IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (Y :=
    pullback.diagonalObj (X := Spec (CommRingCat.of (↑S : Type u))) (Y := Spec (CommRingCat.of (↑R : 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)))))
⊢ autoParam (IsClosedImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f)))
    IsSeparated.isClosedImmersion_diagonal._autoParam

Tactic:
change IsClosedImmersion
    (Limits.pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))))

Premises used: CommRingCat.carrier, Algebra.algebraMap, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CategoryTheory.Limits.pullback.diagonal, AlgebraicGeometry.IsClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
isClosedImmersion_diagonal :
  IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (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)))))
⊢ IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (Y :=
    pullback.diagonalObj (X := Spec (CommRingCat.of (↑S : Type u))) (Y := Spec (CommRingCat.of (↑R : 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:
rw [diagonal_SpecMap, MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion]

Premises used: AlgebraicGeometry.diagonal_SpecMap, AlgebraicGeometry.IsClosedImmersion, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (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:
.spec_of_surjective _ fun x ↦ ⟨.tmul R 1 x,
    (Algebra.TensorProduct.lmul'_apply_tmul (R := R) (S := S) 1 x).trans (one_mul x)⟩

Premises used: CommRingCat.carrier, Algebra.TensorProduct.lmul'_apply_tmul, AlgebraicGeometry.IsClosedImmersion.spec_of_surjective, Exists.intro, TensorProduct.tmul, OfNat.ofNat, one_mul, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (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:
exact .spec_of_surjective _ fun x ↦ ⟨.tmul R 1 x,
    (Algebra.TensorProduct.lmul'_apply_tmul (R := R) (S := S) 1 x).trans (one_mul x)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
inr :
  ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f) (hY : ¬IsAffine Y),
    IsSeparated f
wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
⊢ IsSeparated f

Tactic:
wlog hY : IsAffine Y

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
hY : ¬IsAffine Y
inr : ∀ (i : (↑Y.affineOpens : Type u)), IsSeparated (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
⊢ IsSeparated f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsSeparated) _
      (iSup_affineOpens_eq_top Y)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
⊢ IsAffineHom (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
have H : IsAffineHom (f ∣_ U) := IsZariskiLocalAtTarget.restrict h U
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
H : IsAffineHom (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
⊢ IsSeparated (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
this _ U.2

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
H : IsAffineHom (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
⊢ IsSeparated (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
exact this _ U.2

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
⊢ IsAffine X

Tactic:
have : IsAffine X := HasAffineProperty.iff_of_isAffine.mp h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
rw : IsSeparated (Spec.map (Scheme.Hom.appTop f))
⊢ IsSeparated f

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff @IsSeparated (arrowIsoSpecΓOfIsAffine f)]

Premises used: AlgebraicGeometry.arrowIsoSpecΓOfIsAffine, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.IsSeparated
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated (Spec.map (Scheme.Hom.appTop f))

Tactic:
infer_instance