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

Goal state before:
pp: case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
h✝ : Nonempty ↥X
⊢ IsLocallyArtinian X

Tactic:
have : IsIntegral X := (isIntegral_iff_irreducibleSpace_and_isReduced _).mpr
    ⟨⟨inferInstance⟩, inferInstance⟩

Goal state after:
case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
h✝ : Nonempty ↥X
this : IsIntegral X
⊢ IsLocallyArtinian X
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ IsOpenMap (comap C)

Tactic:
by
  intro U hU
  obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU
  rw [Set.image_sUnion]
  apply isOpen_sUnion
  rintro _ ⟨t, ht, rfl⟩
  obtain ⟨r, rfl⟩ := hS ht
  simp only [image_comap_C_basicOpen]
  exact (isClosed_zeroLocus _).isOpen_compl

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

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Mono (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ x ∈ ⊥

Tactic:
@ConcreteCategory.mono_iff_injective_of_preservesPullback

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Function.Injective ⇑(ConcreteCategory.hom (pushoutSection ⋯ hVU ⋯ ⋯))
⊢ x ∈ ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically (@IsOpenMap) (f ∣_ U i)
⊢ topologically (@IsOpenMap) f

Tactic:
[

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically (@IsOpenMap) (f ∣_ U i)
⊢ topologically (@IsOpenMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)
⊢ topologically (@IsClosedMap) f

Tactic:
[

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)
⊢ topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
[

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral) ∧
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FiniteType ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral) ∧ LocallyOfFiniteType f

Tactic:
refine and_congr_right fun ⟨_, _⟩ ↦
    (HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)).symm

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), monomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
[

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), monomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ ∃ U' ∈ {x | ∃ r, ∃ (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}, x ∈ U' ∧ U' ≤ U

Tactic:
[

Goal state after:
X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ ∃ U' ∈ {x | ∃ r, ∃ (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}, x ∈ U' ∧ U' ≤ U
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ ∃ U, X.toSpecΓ x ∈ U ∧ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)

Tactic:
refine ⟨PrimeSpectrum.basicOpen r, (X.toSpecΓ_preimage_basicOpen r).ge hxr, ?_⟩

Goal state after:
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ (pullbackRestrictIsoRestrict f (Y.basicOpen ↑r)).hom ≫
      (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ f ∣_ Y.basicOpen ↑r ≫ (Y.basicOpen ↑r).toSpecΓ =
    pullback.snd f (Y.basicOpen ↑r).ι ≫ (Y.basicOpen ↑r).toSpecΓ

Tactic:
[

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ (pullbackRestrictIsoRestrict f (Y.basicOpen ↑r)).hom ≫
      (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ f ∣_ Y.basicOpen ↑r ≫ (Y.basicOpen ↑r).toSpecΓ =
    pullback.snd f (Y.basicOpen ↑r).ι ≫ (Y.basicOpen ↑r).toSpecΓ
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))) ≫
        Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv =
    𝔸(n; S) ↘ S

Tactic:
← Spec.map_comp_assoc,

Goal state after:
case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom C ≫
            CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))) ≫
        S.isoSpec.inv =
    𝔸(n; S) ↘ S
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
[

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
⊢ Mono (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
@ConcreteCategory.mono_iff_injective_of_preservesPullback

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV✝ : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
hV : ∀ (i : ι), Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST hUSX hUY))
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ F.ιColimitType j x = F.ιColimitType j y ↔
    ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y

Tactic:
ιColimitType_eq_iff_of_isFiltered

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y) ↔
    ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Injective (F.descColimitType c)
j j' : J
x : F.obj j
x' : F.obj j'
eq : c.ι j x = c.ι j' x'
this : F.ιColimitType j x = F.ιColimitType j' x'
⊢ ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
ιColimitType_eq_iff_of_isFiltered

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Injective (F.descColimitType c)
j j' : J
x : F.obj j
x' : F.obj j'
eq : c.ι j x = c.ι j' x'
this : ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ support fun x ↦ 0).Finite

Tactic:
[

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ support fun x ↦ 0).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x | f x = 0 x}
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x | f x = 0 x})).Finite) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite

Tactic:
this

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
this : support f = U \ {x | f x = 0 x}
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x | f x = 0 x})).Finite) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x | f x = 0 x})).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x₁ x₂ : X
y : Y
⊢ (single x₁ y) x₂ = if x₂ = x₁ then y else 0

Tactic:
[

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x₁ x₂ : X
y : Y
⊢ (single x₁ y) x₂ = if x₂ = x₁ then y else 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x₁ x₂ : X
y : Y
⊢ (single x₁ y).toFun x₂ = if x₂ = x₁ then y else 0

Tactic:
single,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x₁ x₂ : X
y : Y
⊢ Pi.single x₁ y x₂ = if x₂ = x₁ then y else 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = {x | D x = 0}ᶜ ∩ U
⊢ IsDiscrete D.support

Tactic:
this

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = {x | D x = 0}ᶜ ∩ U
⊢ IsDiscrete ({x | D x = 0}ᶜ ∩ U)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx : x ∈ Function.support fun z ↦ if hz : z ∈ V then D z else 0
⊢ x ∈ V

Tactic:
[

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx : x ∈ Function.support fun z ↦ if hz : z ∈ V then D z else 0
⊢ x ∈ V
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ EqOn (⇑(D.restrict h)) (⇑D) V

Tactic:
intro _ _
  simp_all [restrict_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (X.presheaf.germ W x hxW) ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV

Tactic:
← Spec.map_comp_assoc,

Goal state after:
case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (φ' ≫ X.presheaf.germ W x hxW) ≫ IsAffineOpen.fromSpec hV
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ Spec.map (Scheme.Hom.appLE sY U V iVU) ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX

Tactic:
← Spec.map_comp_assoc,

Goal state after:
case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ W.toSpecΓ ≫ Spec.map (Scheme.Hom.appLE sY U V iVU ≫ φ') ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX