awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ ∀ (x_1 : 𝒰.I₀) (x_2 : ↥(𝒰.X x_1)),
    Membership.mem (α := ↥X) U ((𝒰.f x_1) x_2 : ↥X) →
      (TopCat.Hom.hom f.base : (a : ↥X) → ↥Y) ((TopCat.Hom.hom (𝒰.f x_1).base : (a : ↥(𝒰.X x_1)) → ↥X) x_2 : ↥X) = x →
        ∃ x_3 ∈ U, f x_3 = x

Tactic:
grind
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' U) x ↔
    Membership.mem (γ := Set ↥Y)
      (Opens.carrier (⨆ (i : 𝒰.I₀), (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU })) x

Tactic:
exact ⟨fun ⟨x, _, _⟩ ↦ by have := 𝒰.exists_eq x; simp; grind, by simp; grind⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
x : ↥X
refine_2 :
  ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i)), IsIso (X := Y.presheaf.stalk (f ((𝒰.f i) x : ↥X))) (Scheme.Hom.stalkMap f ((𝒰.f i) x))
⊢ IsIso (Scheme.Hom.stalkMap f x)

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
i : 𝒰.I₀
x : ↥(𝒰.X i)
refine_2 : IsIso (Scheme.Hom.stalkMap (𝒰.f i ≫ f) x ≫ inv (Scheme.Hom.stalkMap (𝒰.f i) x))
⊢ IsIso (X := Y.presheaf.stalk (f ((𝒰.f i) x : ↥X))) (Scheme.Hom.stalkMap f ((𝒰.f i) x))

Tactic:
rw [← (IsIso.comp_inv_eq _).mpr (Scheme.Hom.stalkMap_comp (𝒰.f i) f x)]

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{u_1, u} X
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
i : 𝒰.I₀
x : ↥(𝒰.X i)
⊢ IsIso (Scheme.Hom.stalkMap (𝒰.f i ≫ f) x ≫ inv (Scheme.Hom.stalkMap (𝒰.f i) x))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hX :
  ∀ (x : ↥X),
    ∃ (U : Scheme.{u}) (i : U ⟶ X) (x_1 : IsOpenImmersion i), x ∈ Scheme.Hom.opensRange i ∧ IsOpenImmersion (i ≫ f)
choose :
  ∀ (U : (x : ↥X) → Scheme.{u}) (i : (x : ↥X) → U x ⟶ X) (x : ∀ (x : ↥X), IsOpenImmersion (i x))
    (hxi : ∀ (x_1 : ↥X), x_1 ∈ Scheme.Hom.opensRange (i x_1)) (hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)),
    IsOpenImmersion f
⊢ IsOpenImmersion f

Tactic:
choose U i _ hxi hi using hX
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
U : (x : ↥X) → Scheme
i : (x : ↥X) → U x ⟶ X
h : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
⊢ { I₀ := ↥X, X := U, f := i : PreZeroHypercover X }.presieve₀ ∈ Scheme.jointlySurjectivePrecoverage.coverings X

Tactic:
simpa using show ∀ x, ∃ j y, i j y = x from (⟨_, hxi ·⟩)

Premises used: Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
U : (x : ↥X) → Scheme
i : (x : ↥X) → U x ⟶ X
h : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
⊢ { I₀ := ↥X, X := U, f := i : PreZeroHypercover X }.presieve₀ ∈ IsOpenImmersion.precoverage.coverings X

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
U : (x : ↥X) → Scheme
i : (x : ↥X) → U x ⟶ X
h : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
𝒰 : X.OpenCover := { I₀ := ↥X, X := U, f := i, mem₀ := ⋯ }
⊢ IsOpenImmersion f

Tactic:
IsOpenImmersion.of_openCover_source f 𝒰 hf hi

Premises used: AlgebraicGeometry.IsOpenImmersion.of_openCover_source
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
U : (x : ↥X) → Scheme
i : (x : ↥X) → U x ⟶ X
h : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
𝒰 : X.OpenCover := { I₀ := ↥X, X := U, f := i, mem₀ := ⋯ }
⊢ IsOpenImmersion f

Tactic:
exact IsOpenImmersion.of_openCover_source f 𝒰 hf hi

Premises used: AlgebraicGeometry.IsOpenImmersion.of_openCover_source
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    IsOpenImmersion f ↔
      ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
          stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
            Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
        f
⊢ IsOpenImmersion =
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
        stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
          Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
      f

Tactic:
IsOpenImmersion.iff_isIso_stalkMap.trans
    (and_congr Iff.rfl (forall_congr' fun x ↦ ConcreteCategory.isIso_iff_bijective _))

Premises used: AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, Iff.rfl, CategoryTheory.ConcreteCategory.isIso_iff_bijective, forall_congr', Iff.trans, AlgebraicGeometry.Scheme.Hom.stalkMap, and_congr
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
        stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
          Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
      f

Tactic:
exact IsOpenImmersion.iff_isIso_stalkMap.trans
    (and_congr Iff.rfl (forall_congr' fun x ↦ ConcreteCategory.isIso_iff_bijective _))

Premises used: AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, Iff.rfl, CategoryTheory.ConcreteCategory.isIso_iff_bijective, forall_congr', Iff.trans, AlgebraicGeometry.Scheme.Hom.stalkMap, and_congr
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
hP :
  RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)
⊢ IsZariskiLocalAtTarget.{u_1}
    (stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))

Tactic:
apply stalkwiseIsZariskiLocalAtTarget_of_respectsIso

Premises used: AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
hP :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)).RespectsIso
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)

Tactic:
rw [RingHom.toMorphismProperty_respectsIso_iff]

Premises used: RingHom.toMorphismProperty_respectsIso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
⊢ MorphismProperty.RespectsIso (MorphismProperty.isomorphisms CommRingCat)

Tactic:
(inferInstance : (MorphismProperty.isomorphisms CommRingCat).RespectsIso)

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
h :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
    MorphismProperty.isomorphisms CommRingCat
⊢ (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)).RespectsIso

Tactic:
convert! (inferInstance : (MorphismProperty.isomorphisms CommRingCat).RespectsIso)

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
h :
  ∀ ⦃X Y : CommRingCat.{u_1}⦄ (f : X ⟶ Y),
    RingHom.toMorphismProperty
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
          Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
        f ↔
      MorphismProperty.isomorphisms CommRingCat f
⊢ (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
    MorphismProperty.isomorphisms CommRingCat

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
X_1 Y_1 : CommRingCat
f : X_1 ⟶ Y_1
⊢ RingHom.toMorphismProperty
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
      f ↔
    MorphismProperty.isomorphisms CommRingCat f

Tactic:
(ConcreteCategory.isIso_iff_bijective _).symm

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective, RingHom.toMorphismProperty, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
X_1 Y_1 : CommRingCat
f : X_1 ⟶ Y_1
⊢ RingHom.toMorphismProperty
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
      f ↔
    MorphismProperty.isomorphisms CommRingCat f

Tactic:
exact (ConcreteCategory.isIso_iff_bijective _).symm

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X Y : Scheme
⊢ IsZariskiLocalAtTarget IsOpenImmersion

Tactic:
isOpenImmersion_eq_inf ▸ inferInstance

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.isOpenImmersion_eq_inf, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Goal:
X_1 Y_1 X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (X := X ⨿ Y) (Y := X' ⨿ Y') (coprod.map f g)

Tactic:
IsZariskiLocalAtTarget.coprodMap f g ‹_› ‹_›

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.coprodMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
h :
  ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
    IsPreimmersion x_2 ↔
      (@SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding)
        x_2
⊢ @IsPreimmersion =
    @SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
h :
  SurjectiveOnStalks x_2 ∧ IsEmbedding (X := ↥x) (Y := ↥x_1) ⇑x_2 ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding)
      x_2
⊢ IsPreimmersion x_2 ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding)
      x_2

Tactic:
rw [isPreimmersion_iff]

Premises used: AlgebraicGeometry.isPreimmersion_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ SurjectiveOnStalks x_2 ∧ IsEmbedding (X := ↥x) (Y := ↥x_1) ⇑x_2 ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding)
      x_2

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
⊢ IsZariskiLocalAtTarget @IsPreimmersion

Tactic:
isPreimmersion_eq_inf ▸ inferInstance

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.isPreimmersion_eq_inf, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion f
inst_1 : IsPreimmersion g
⊢ IsPreimmersion (f ≫ g)

Tactic:
MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsPreimmersion f
⊢ Mono f

Tactic:
SurjectiveOnStalks.mono_of_injective f.isEmbedding.injective

Premises used: AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective, AlgebraicGeometry.Scheme.Hom.isEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
x : ↥X
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : 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.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
have h := (f ≫ g).stalkMap_surjective x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
x : ↥X
h :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : 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.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : 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.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

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

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
x : ↥X
h :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : 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.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : 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.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
Function.Surjective.of_comp h

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
x : ↥X
h :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : 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.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : 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.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
exact Function.Surjective.of_comp h

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
⊢ IsEmbedding (X := ↥X) (Y := ↥Z) ⇑(f ≫ g)

Tactic:
have h := (f ≫ g).isEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
h : IsEmbedding (X := ↥X) (Y := ↥Z) ⇑(f ≫ g)
rwa rwa₁ rwa₂ rwa₃ : IsEmbedding (X := ↥X) (Y := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)
⊢ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
rwa [← g.isEmbedding.of_comp_iff]

Premises used: AlgebraicGeometry.Scheme.Hom.isEmbedding, Topology.IsEmbedding.of_comp_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
⊢ IsPreimmersion (f ≫ g) ↔ IsPreimmersion f

Tactic:
⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.IsPreimmersion.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
R S : CommRingCat
f : R ⟶ S
rw :
  IsEmbedding (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f) ∧ SurjectiveOnStalks (Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)
⊢ IsPreimmersion (Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks

Tactic:
rw [← HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks), isPreimmersion_iff, and_comm]

Premises used: and_comm, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ IsEmbedding (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f) ∧ SurjectiveOnStalks (Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h₁ : IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f))
h₂ : (CommRingCat.Hom.hom f).SurjectiveOnStalks
⊢ IsPreimmersion (Spec.map f)

Tactic:
(SpecMap_iff f).mpr ⟨h₁, h₂⟩

Premises used: Iff.mpr, AlgebraicGeometry.IsPreimmersion.SpecMap_iff, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
R S : Type u
inst : CommRing R
M : Submonoid R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ IsPreimmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (Spec.map (CommRingCat.ofHom (algebraMap R S)))

Tactic:
IsPreimmersion.mk_SpecMap
    (PrimeSpectrum.localization_comap_isEmbedding (R := R) S M)
    (RingHom.surjectiveOnStalks_of_isLocalization (M := M) S)

Premises used: AlgebraicGeometry.IsPreimmersion.mk_SpecMap, PrimeSpectrum.localization_comap_isEmbedding, RingHom.surjectiveOnStalks_of_isLocalization
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
⊢ IsStableUnderBaseChange @IsPreimmersion

Tactic:
.mk' fun X Y Z f g _ _ ↦ ?_

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
refine :
  ∀ (X Y Z : Scheme.{u_1}) (f : X ⟶ Z) (g : Y ⟶ Z) (x : HasPullback f g),
    IsPreimmersion g → IsPreimmersion (X := pullback f g) (pullback.fst f g)
⊢ IsStableUnderBaseChange @IsPreimmersion

Tactic:
refine .mk' fun X Y Z f g _ _ ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
⊢ SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)

Tactic:
have := pullback_fst (P := @SurjectiveOnStalks) f g inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
isEmbedding : IsEmbedding (X := ↥(pullback f g)) (Y := ↥X) ⇑(pullback.fst f g)
⊢ IsPreimmersion (X := pullback f g) (pullback.fst f g)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
x : ↥(pullback f g)
⊢ Membership.mem (α := ↥X × ↥Y) (γ := Set (↥X × ↥Y)) {x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)}
    (((pullback.fst f g) x, (pullback.snd f g) x) : ↥X × ↥Y)

Tactic:
simp only [Set.mem_setOf, ← Scheme.Hom.comp_apply, pullback.condition]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, Set.mem_setOf, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
L : (x : ↥(pullback f g)) → (↑{x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} : Type u_1) :=
  fun (x : ↥(pullback f g)) ↦
    Subtype.mk (p := fun (x : ↥X × ↥Y) ↦
      Membership.mem (γ := Set (↥X × ↥Y)) {x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} x)
      ((pullback.fst f g) x, (pullback.snd f g) x) ⋯
⊢ Continuous L

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
L : (x : ↥(pullback f g)) → (↑{x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} : Type u_1) :=
  fun (x : ↥(pullback f g)) ↦
    Subtype.mk (p := fun (x : ↥X × ↥Y) ↦
      Membership.mem (γ := Set (↥X × ↥Y)) {x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} x)
      ((pullback.fst f g) x, (pullback.snd f g) x) ⋯
⊢ IsEmbedding L

Tactic:
have : IsEmbedding L := IsEmbedding.of_comp (by fun_prop) continuous_subtype_val
    (SurjectiveOnStalks.isEmbedding_pullback f g)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this_1 : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
L : (x : ↥(pullback f g)) → (↑{x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} : Type u_1) :=
  fun (x : ↥(pullback f g)) ↦
    Subtype.mk (p := fun (x : ↥X × ↥Y) ↦
      Membership.mem (γ := Set (↥X × ↥Y)) {x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} x)
      ((pullback.fst f g) x, (pullback.snd f g) x) ⋯
this : IsEmbedding L
⊢ IsEmbedding (X := ↥(pullback f g)) (Y := ↥X) ⇑(pullback.fst f g)

Tactic:
IsEmbedding.subtypeVal.comp ((TopCat.pullbackHomeoPreimage _ f.continuous _
    g.isEmbedding).isEmbedding.comp this)

Premises used: Homeomorph.isEmbedding, AlgebraicGeometry.Scheme.Hom.isEmbedding, Topology.IsEmbedding.comp, TopCat.pullbackHomeoPreimage, AlgebraicGeometry.Scheme.Hom.continuous, Topology.IsEmbedding.subtypeVal