mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
            (limit.isoLimitCone
                { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).f
        ((Equiv.refl (Cover.ulift 𝒰).I₀) i)

Tactic:
Cover.pushforwardIso_f,

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (gluing (Cover.ulift 𝒰) f g).openCover.f ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
⊢ IsOpenCover Subtype.val

Tactic:
ext

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
x✝ : ↥X
⊢ x✝ ∈ ↑(iSup Subtype.val) ↔ x✝ ∈ ↑⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q

Tactic:
ext

Goal state after:
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
x✝³ x✝² : Scheme
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsAffine x✝²
⊢ P x✝¹ ↔ Q x✝¹
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f

Tactic:
constructor

Goal state after:
case mp
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f

case mpr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    (Iso.refl (pullback (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)))).hom ≫
      (openCoverOfBase' 𝒰 f g).f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i)

Tactic:
rw [Iso.refl_hom, Category.id_comp, openCoverOfBase'_f]

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    (pullbackSymmetry
          (pullback.snd f
            (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
          (pullback.snd g
            (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))).hom ≫
      (limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv ≫
        pullback.map
            (pullback.snd f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)
            g
            (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              f)
            g
            (𝟙
              (pullback f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)))
            (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫
          pullback.map
            (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              f)
            g f g
            (pullback.fst f
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
            (𝟙 Y) (𝟙 Z) ⋯ ⋯
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h =
    pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f

Tactic:
ext

Goal state after:
case h₀
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h) ≫ pullback.fst fXZ fYZ =
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.fst fXZ fYZ

case h₁
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h) ≫ pullback.snd fXZ fYZ =
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.snd fXZ fYZ
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U)) ∧
    (D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i =
      𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))

Tactic:
constructor

Goal state after:
case h.left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))

case h.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ (D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i =
    𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj ↔ ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
constructor

Goal state after:
case mp
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

case mpr
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj) → (colimit.ι F i) xi = (colimit.ι F j) xj
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : s.fst.base ≫ D.toTopGlueData.ι i = s.snd.base ≫ D.toTopGlueData.ι j
⊢ Set.range (⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) ∘ ⇑(ConcreteCategory.hom s.fst.base)) ⊆
    Set.range ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j))

Tactic:
← TopCat.coe_comp,

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : s.fst.base ≫ D.toTopGlueData.ι i = s.snd.base ≫ D.toTopGlueData.ι j
⊢ Set.range ⇑(ConcreteCategory.hom (s.fst.base ≫ (D.mapGlueData (forget C)).ι i)) ⊆
    Set.range ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j))
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: ⊢ @Surjective = topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ Surjective x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: ⊢ @IsDominant = topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsDominant x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ DenseRange) x✝
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
constructor

Goal state after:
case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
⊢ IsLocalization.Away (IsLocalization.Away.mulNumerator s t ⟨a, b⟩)
    ((fun x ↦
        match x with
        | ⟨a, b⟩ => Localization.Away ↑b)
      ⟨a, b⟩)

Tactic:
have : IsLocalization.Away ((algebraMap S (Localization.Away a.val))
        (IsLocalization.Away.sec a.val b.val).1) (Localization.Away b.val) := by
      apply IsLocalization.Away.of_associated (r := b.val)
      rw [← IsLocalization.Away.sec_spec]
      apply associated_mul_unit_right
      rw [map_pow _ _]
      exact IsUnit.pow _ (IsLocalization.Away.algebraMap_isUnit _)
    apply IsLocalization.Away.mul' (Localization.Away a.val) (Localization.Away b.val)

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
⊢ ∀ t ∈ ⇑e '' s,
    (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp (e.toRingHom.comp f))

Tactic:
rintro - ⟨a, ha, rfl⟩
      let e' : Localization.Away a ≃+* Localization.Away (e a) :=
        IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a)
      have : (algebraMap T (Localization.Away (e a))).comp e.toRingHom =
          e'.toRingHom.comp (algebraMap S (Localization.Away a)) := by
        ext x
        simp [e']
      rw [← RingHom.comp_assoc, this, RingHom.comp_assoc]
      apply hPi.left
      exact hs a ha

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := HasAffineProperty.isLocal_affineProperty P
⊢ P.diagonal f ↔ targetAffineLocally Q.diagonal f

Tactic:
constructor

Goal state after:
case mp
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ P.diagonal f → targetAffineLocally Q.diagonal f

case mpr
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ targetAffineLocally Q.diagonal f → P.diagonal f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P.diagonal (U.ι ≫ f)

Tactic:
change P _
    apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance
    rw [← pullback.comp_diagonal]
    apply IsZariskiLocalAtSource.comp
    exact hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: ⊢ @SurjectiveOnStalks = stalkwise fun {R S} [CommRing R] [CommRing S] x ↦ Function.Surjective ⇑x

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ SurjectiveOnStalks x✝ ↔ stalkwise (fun {R S} [CommRing R] [CommRing S] x ↦ Function.Surjective ⇑x) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ P).IsLocal

Tactic:
constructor

Goal state after:
case respectsIso
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso

case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen r)

case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ →
      (∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)) →
        sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case e'_5
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(pullback (Spec.map φ) (Spec.map ψ))
⊢ (L ∘ ⇑(pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂)) x =
    ((Prod.map ⇑iX ⇑iY ∘ PrimeSpectrum.tensorProductTo ↑R ↑A ↑B) ∘ ⇑(Scheme.homeoOfIso (pullbackSpecIso ↑R ↑A ↑B))) x

Tactic:
obtain ⟨x, rfl⟩ := (Scheme.homeoOfIso (pullbackSpecIso R A B).symm).surjective x

Goal state after:
case e'_5
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (L ∘ ⇑(pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂))
      ((Scheme.homeoOfIso (pullbackSpecIso ↑R ↑A ↑B).symm) x) =
    ((Prod.map ⇑iX ⇑iY ∘ PrimeSpectrum.tensorProductTo ↑R ↑A ↑B) ∘ ⇑(Scheme.homeoOfIso (pullbackSpecIso ↑R ↑A ↑B)))
      ((Scheme.homeoOfIso (pullbackSpecIso ↑R ↑A ↑B).symm) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case e'_5
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ L ((pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂) ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)) =
    Prod.map (⇑iX) (⇑iY)
      (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
        ((pullbackSpecIso ↑R ↑A ↑B).hom ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)))

Tactic:
ext

Goal state after:
case e'_5.fst
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := ⋯
algInst✝ : Algebra ↑R ↑B := ⋯
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (L ((pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂) ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x))).1 =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((pullbackSpecIso ↑R ↑A ↑B).hom ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)))).1

case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := ⋯
algInst✝ : Algebra ↑R ↑B := ⋯
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (L ((pullback.map (Spec.map φ) (Spec.map ψ) f g iX iY iS e₁ e₂) ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x))).2 =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B)
          ((pullbackSpecIso ↑R ↑A ↑B).hom ((pullbackSpecIso ↑R ↑A ↑B).symm.hom x)))).2
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: ⊢ @IsPreimmersion =
    @SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsPreimmersion x✝ ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↥X
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
exact Function.Surjective.of_comp h

Goal state after: