awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
R S : CommRingCat
φ : R ⟶ S
rw :
  stalkwise
      (fun {R S : Type u} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
      (Spec.map φ) ↔
    (CommRingCat.Hom.hom φ).SurjectiveOnStalks
rw₁ :
  (∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      Function.Surjective (α := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (β :=
        Localization.AtPrime p)
        (⇑(Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯) :
          (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) → Localization.AtPrime p)) ↔
    (CommRingCat.Hom.hom φ).SurjectiveOnStalks
rw₂ rw₃ :
  (∀ (p : Ideal (↑S : Type u)) (x : p.IsPrime),
      Function.Surjective (α := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) (β :=
        Localization.AtPrime p)
        (⇑(Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯) :
          (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) p)) → Localization.AtPrime p)) ↔
    ∀ (P : Ideal (↑S : Type u)) (x : P.IsPrime),
      Function.Surjective (α := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) (β :=
        Localization.AtPrime P)
        (⇑(Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯) :
          (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) → Localization.AtPrime P)
⊢ SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks

Tactic:
rw [eq_stalkwise, stalkwise_SpecMap_iff RingHom.surjective_respectsIso,
    RingHom.SurjectiveOnStalks]

Premises used: AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise, AlgebraicGeometry.stalkwise_SpecMap_iff, RingHom.surjective_respectsIso, RingHom.SurjectiveOnStalks
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ HasRingHomProperty @SurjectiveOnStalks fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks

Tactic:
eq_stalkwise ▸ .stalkwise RingHom.surjective_respectsIso

Premises used: AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise, Eq.rec, AlgebraicGeometry.HasRingHomProperty.stalkwise, RingHom.surjective_respectsIso, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
rw : SurjectiveOnStalks f ↔ SurjectiveOnStalks (X := Spec Γ(X, f ⁻¹ᵁ ⊤)) (Spec.map (Scheme.Hom.app f ⊤))
rw₁ rw₂ :
  SurjectiveOnStalks (Spec.map (Scheme.Hom.appTop f)) ↔
    SurjectiveOnStalks (X := Spec Γ(X, f ⁻¹ᵁ ⊤)) (Spec.map (Scheme.Hom.app f ⊤))
⊢ SurjectiveOnStalks f ↔
    RingHom.SurjectiveOnStalks (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤))

Tactic:
rw [← Spec_iff, MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)]

Premises used: AlgebraicGeometry.SurjectiveOnStalks, AlgebraicGeometry.arrowIsoSpecΓOfIsAffine, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.SurjectiveOnStalks.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
⊢ SurjectiveOnStalks f

Tactic:
⟨fun x ↦ ?_⟩

Premises used: AlgebraicGeometry.SurjectiveOnStalks.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
refine :
  ∀ (x : ↥X),
    Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
        (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ SurjectiveOnStalks f

Tactic:
refine ⟨fun x ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
x : ↥X
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
have := (f ≫ g).stalkMap_surjective x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
x : ↥X
this :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
rw [Scheme.Hom.stalkMap_comp] at this

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
x : ↥X
this :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
Function.Surjective.of_comp this

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks (f ≫ g)
x : ↥X
this :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
exact Function.Surjective.of_comp this

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hP : RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks
⊢ MorphismProperty.IsStableUnderBaseChange @SurjectiveOnStalks

Tactic:
apply HasRingHomProperty.isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hP : RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks
hP₁ :
  ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ RingHom.IsStableUnderBaseChange.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks

Tactic:
apply RingHom.IsStableUnderBaseChange.mk

Premises used: RingHom.IsStableUnderBaseChange.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks

Tactic:
(HasRingHomProperty.isLocal_ringHomProperty @SurjectiveOnStalks).respectsIso

Premises used: AlgebraicGeometry.SurjectiveOnStalks, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks

Tactic:
exact (HasRingHomProperty.isLocal_ringHomProperty @SurjectiveOnStalks).respectsIso

Premises used: AlgebraicGeometry.SurjectiveOnStalks, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
R S T : Type u_1
hP :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
R S T : Type u_1
inst : CommRing R
hP :
  ∀ [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ ∀ [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
hP :
  ∀ [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ ∀ [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
hP :
  ∀ [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ ∀ [inst_3 : Algebra R S] [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
hP :
  ∀ [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ ∀ [inst_4 : Algebra R T],
    RingHom.SurjectiveOnStalks (algebraMap R T) →
      RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : RingHom.SurjectiveOnStalks (algebraMap R T)
⊢ RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
H.baseChange

Premises used: RingHom.SurjectiveOnStalks.baseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : RingHom.SurjectiveOnStalks (algebraMap R T)
⊢ RingHom.SurjectiveOnStalks (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
exact H.baseChange

Premises used: RingHom.SurjectiveOnStalks.baseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ Mono f

Tactic:
(Scheme.forgetToLocallyRingedSpace ⋙
    LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Functor.mono_of_mono_map, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
refine : Mono ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f)
⊢ Mono f

Tactic:
refine (Scheme.forgetToLocallyRingedSpace ⋙
    LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Functor.mono_of_mono_map, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h₁ :
  Function.Injective (α :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
          TopCat) :
      Type u))
    (β :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
          TopCat) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base) :
      (a :
          (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
                TopCat) :
            Type u)) →
        (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
              TopCat) :
          Type u))
h₂ :
  ∀
    (x :
      (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
            TopCat) :
        Type u)),
    Epi (X :=
      ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base :
            (a :
                (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                            X).toPresheafedSpace :
                      TopCat) :
                  Type u)) →
              (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                          Y).toPresheafedSpace :
                    TopCat) :
                Type u))
          x))
      (PresheafedSpace.Hom.stalkMap
        ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom x)
⊢ Mono ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f)

Tactic:
apply SheafedSpace.mono_of_base_injective_of_stalk_epi

Premises used: AlgebraicGeometry.SheafedSpace.mono_of_base_injective_of_stalk_epi
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ Function.Injective (α :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
          TopCat) :
      Type u))
    (β :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
          TopCat) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base) :
      (a :
          (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
                TopCat) :
            Type u)) →
        (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
              TopCat) :
          Type u))

Tactic:
hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ Function.Injective (α :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
          TopCat) :
      Type u))
    (β :=
    (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
          TopCat) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base) :
      (a :
          (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
                TopCat) :
            Type u)) →
        (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).toPresheafedSpace :
              TopCat) :
          Type u))

Tactic:
exact hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ ∀
    (x :
      (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
            TopCat) :
        Type u)),
    Epi (X :=
      ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base :
            (a :
                (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                            X).toPresheafedSpace :
                      TopCat) :
                  Type u)) →
              (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                          Y).toPresheafedSpace :
                    TopCat) :
                Type u))
          x))
      (PresheafedSpace.Hom.stalkMap
        ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom x)

Tactic:
fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, CategoryTheory.ConcreteCategory.epi_of_surjective, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, CategoryTheory.InducedCategory.Hom.hom, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y : Scheme
f : X ⟶ Y
inst : SurjectiveOnStalks f
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ ∀
    (x :
      (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace :
            TopCat) :
        Type u)),
    Epi (X :=
      ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj Y).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom.base :
            (a :
                (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                            X).toPresheafedSpace :
                      TopCat) :
                  Type u)) →
              (↑(↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj
                          Y).toPresheafedSpace :
                    TopCat) :
                Type u))
          x))
      (PresheafedSpace.Hom.stalkMap
        ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom x)

Tactic:
exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)

Premises used: CategoryTheory.ConcreteCategory.epi_of_surjective, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Injective).RespectsIso

Tactic:
topologically_respectsIso _ (fun e ↦ e.injective) (fun _ _ hf hg ↦ hg.comp hf)

Premises used: Homeomorph.injective, Function.Injective.comp, AlgebraicGeometry.topologically_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Injective)

Tactic:
topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s)
    fun f ι U H _ hf x₁ x₂ e ↦ ?_

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget, Function.Injective.restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
refine :
  ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (ι : Type u_1)
    (U : ι → Opens β) (H : IsOpenCover U),
    Continuous f →
      ∀ (hf : ∀ (i : ι), Function.Injective ((U i).carrier.restrictPreimage f)) (x₁ x₂ : α) (e : f x₁ = f x₂), x₁ = x₂
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Injective)

Tactic:
refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s)
    fun f ι U H _ hf x₁ x₂ e ↦ ?_

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget