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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)

Tactic:
let := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra

Goal state after:
X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f

Tactic:
let := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra

Goal state after:
X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hxU⟩)) ≫ (↑U).fromSpecStalk ⟨x, hxU⟩ ≫ (↑U).toSpecΓ ≫ Spec.map U.topIso.inv =
    Spec.map (X.presheaf.germ U x hxU)

Tactic:
fromSpecStalk_toSpecΓ_assoc,

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Spec.map (inv (Hom.stalkMap U.ι ⟨x, hxU⟩)) ≫
      Spec.map ((↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial) ≫ Spec.map U.topIso.inv =
    Spec.map (X.presheaf.germ U x hxU)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x✝¹ : ↑Γ(X, ↑V)
hx : x✝¹ ∈ I.ideal V
x : ↥(pullback (I.glueDataObjι U) (X.homOfLE ⋯))
x✝ : x ∈ ⊤
⊢ x ∈ (F ≫ (↑U ⊓ ↑V).ι) ⁻¹ᵁ ↑V

Tactic:
by simpa using (F x).2.2

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField (Triplet.ofPoint t).y =
    Spec.map (Hom.residueFieldMap (pullback.snd f g) t) ≫ Y.fromSpecResidueField ((pullback.snd f g) t)

Tactic:
rw [← pushout.inr_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t), Spec.map_comp]

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField (Triplet.ofPoint t).y =
    (Spec.map (pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) ⋯) ≫
        Spec.map
          (pushout.inr ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y))) ≫
      Y.fromSpecResidueField ((pullback.snd f g) t)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↥X
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ CompactSpace ↥X

Tactic:
rw [← isCompact_univ_iff, ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e]

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↥X
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact ↑(⨆ i ∈ ↑s', X.basicOpen i)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (pullbackComparison forgetToTop f g)

Tactic:
refine (CategoryTheory.forget TopCat).epi_of_epi_map ?_

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi ((CategoryTheory.forget TopCat).map (pullbackComparison forgetToTop f g))
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
⊢ FiniteType R S

Tactic:
obtain ⟨l, hl⟩ :=
    (Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
      (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
⊢ FiniteType R S
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : l i = 0
⊢ l i ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
rw [h]

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : l i = 0
⊢ 0 ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ IsEmpty ↥⊤.subscheme

Tactic:
rw [← (subschemeι _).ker_eq_top_iff_isEmpty, ker_subschemeι]

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) =
    @IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
by
  ext X Y f
  exact targetAffineLocally_affineAnd_iff_affineLocally hQ f

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
⊢ P (f ≫ g)

Tactic:
wlog hZ : IsAffine Z

Goal state after:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ P (f ≫ g)

Q✝ Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
⊢ P (f ≫ g)
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := ⋯
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := ⋯
x : S
t✝ : Set S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away ↑r ⊗[R] S)) ((algebraMap R S) ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ * x) ∈ adjoin R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈ adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))
⊢ ↑r ^ (n₂ + n₁) • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))

Tactic:
exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ SurjectiveOnStalks f ∧ IsClosedEmbedding ⇑f ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓ @SurjectiveOnStalks) f

Tactic:
and_comm

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedEmbedding ⇑f ∧ SurjectiveOnStalks f ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓ @SurjectiveOnStalks) f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ J ≤ I.map f

Tactic:
rw [map, ← J.ker_subschemeι, ← this]

Goal state after:
case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ Hom.ker J.subschemeι ≤ Hom.ker ((inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ ⊥.map f = Hom.ker f

Tactic:
by
  simp [map, Scheme.Hom.ker_comp_of_isIso]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
h : ∀ i ∈ s✝, FinitePresentation R (Localization.Away i)
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
⊢ FinitePresentation R S

Tactic:
replace h (i : s) : Algebra.FinitePresentation R (Localization.Away i.val) := h i (h₁ i.property)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
⊢ FinitePresentation R S
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
s : ↥S
⊢ minN ↑s ∈ suitableN ↑s

Tactic:
apply Nat.sInf_mem

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := ⋯
suitableN : R → Set ℕ := ⋯
minN : R → ℕ := ⋯
s : ↥S
⊢ (suitableN ↑s).Nonempty
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
x✝ : IsNoetherianRing ↑Γ(X, ↑U)
⊢ Order.krullDim (PrimeSpectrum ↑Γ(X, ↑U)) ≤ ↑0

Tactic:
← ringKrullDim,

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
x✝ : IsNoetherianRing ↑Γ(X, ↑U)
⊢ ringKrullDim ↑Γ(X, ↑U) ≤ ↑0
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ ∃ a, comap C a = x

Tactic:
refine ⟨comap (eval₂Hom (.id _) 0) x, ?_⟩

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ comap C (comap (eval₂Hom (RingHom.id R) 0) x) = x
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
⊢ (geometrically P).IsStableUnderBaseChange

Tactic:
rw [geometrically_eq_universally]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsCompact Set.univ

Tactic:
rw [← Opens.coe_top, ← hS, Opens.iSup_mk]

Goal state after:
case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsCompact ↑{ carrier := ⋃ i, (S i).1.carrier, is_open' := ⋯ }
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))
U : { x // x.1 ∈ Y.affineOpens ∧ x.1 ≤ (TopologicalSpace.Opens.comap (TopCat.Hom.hom g.base)) ↑x.2 }
⊢ (↑U).1 ∈ Y.affineOpens

Tactic:
exact U.2.1

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

Goal state before:
pp: ⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite

Tactic:
simp [isFinite_iff]

Goal state after:
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 ⇑ψ
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
have hψ' : Function.Injective (Algebra.TensorProduct.map (AlgHom.id Γ(T, UT) Γ(T, UT)) ψ) :=
    Module.Flat.lTensor_preserves_injective_linearMap ψ.toLinearMap hψ

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.CategoryTheory.Limits.Types.ColimitTypeFiltered

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

Tactic:
F.ιColimitType_map

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
i : J
x : F.obj i
i' : J
x' : F.obj i'
eq✝ : c.ι i x = c.ι i' x'
k : J
f : i ⟶ k
f' : i' ⟶ k
eq : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
⊢ F.ιColimitType i' x' = F.ιColimitType i' x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
K : Type u
inst✝ : Field K
y : Spec (CommRingCat.of K) ⟶ S
Z : Scheme
fst : Z ⟶ 𝔸(n; S)
snd : Z ⟶ Spec (CommRingCat.of K)
h : IsPullback fst snd (𝔸(n; S) ↘ S) y
⊢ IrreducibleSpace ↥Z

Tactic:
apply ObjectProperty.prop_of_iso _
    ((h.isoIsPullback _ _ (isPullback_map _)) ≪≫ (SpecIso n (.of K))).symm

Goal state after:
n : Type u
S : Scheme
K : Type u
inst✝ : Field K
y : Spec (CommRingCat.of K) ⟶ S
Z : Scheme
fst : Z ⟶ 𝔸(n; S)
snd : Z ⟶ Spec (CommRingCat.of K)
h : IsPullback fst snd (𝔸(n; S) ↘ S) y
⊢ IrreducibleSpace ↥(Spec (CommRingCat.of (MvPolynomial n ↑(CommRingCat.of K))))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
K : Type u
inst✝ : Field K
y : Spec (CommRingCat.of K) ⟶ S
Z : Scheme
fst : Z ⟶ 𝔸(n; S)
snd : Z ⟶ Spec (CommRingCat.of K)
h : IsPullback fst snd (𝔸(n; S) ↘ S) y
⊢ IsReduced Z

Tactic:
apply ObjectProperty.prop_of_iso _
    ((h.isoIsPullback _ _ (isPullback_map _)) ≪≫ (SpecIso n (.of K))).symm

Goal state after:
n : Type u
S : Scheme
K : Type u
inst✝ : Field K
y : Spec (CommRingCat.of K) ⟶ S
Z : Scheme
fst : Z ⟶ 𝔸(n; S)
snd : Z ⟶ Spec (CommRingCat.of K)
h : IsPullback fst snd (𝔸(n; S) ↘ S) y
⊢ IsReduced (Spec (CommRingCat.of (MvPolynomial n ↑(CommRingCat.of K))))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
⊢ ∑ z ∈ h.toFinset, single z (D z) = D

Tactic:
by
  ext w
  simp only [coe_sum, Finset.sum_apply, single_apply, Finset.sum_ite_eq]
  set s := h.toFinset with hs
  by_cases hw : w ∈ s
  · simp [hw]
  · simp only [hw, if_false]
    have : w ∉ support D := by simpa only [hs, Set.Finite.mem_toFinset] using hw
    exact (notMem_support.mp this).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst✝ : IsIntegral X
x : ↥X
this✝ : Nonempty ↥↑(Scheme.Hom.opensRange (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, ⋯⟩)) (⋯.primeIdealOf ⟨x, ⋯⟩).asIdeal
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        (X.presheaf.germ (Scheme.Hom.opensRange (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) x ⋯))

Tactic:
exact @IsLocalization.injective _ _ _ _ _ (show _ from _) this
    (Ideal.primeCompl_le_nonZeroDivisors _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = 0
⊢ y = 0

Tactic:
rw [← (X.presheaf.germ U x hx).hom.map_zero] at hy

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : ↑(X.presheaf.obj (op U))
hy : (ConcreteCategory.hom (X.presheaf.germ U x hx)) y = (CommRingCat.Hom.hom (X.presheaf.germ U x hx)) 0
⊢ y = 0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
i j : I
f : i ⟶ j
⊢ IsAffineHom (D'.map f ≫ ι.app j)

Tactic:
simp only [subschemeMap_subschemeι, D', ι]

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  { obj := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subscheme,
    map := fun {X Y} f ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun i ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
i j : I
f : i ⟶ j
⊢ IsAffineHom ((vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι ≫ D.map f)
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X Y : Scheme
f g : X.PartialIso Y
⊢ f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'

Tactic:
by
  constructor
  · rintro rfl
    simp
  · obtain ⟨U₁, hU₁, U₂, hU₂, f⟩ := f
    obtain ⟨V₁, hV₁, V₂, hU₂, g⟩ := g
    simp only [forall_exists_index]
    rintro rfl rfl e
    simpa using e

Goal state after: