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

Goal state before:
pp: case h
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
i : ↑s
⊢ n i ≤ Finset.univ.sup n

Tactic:
exact Finset.le_sup (Finset.mem_univ _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
x : ↥(Spec R)
inst✝ : IsReduced (Spec R)
hx : x.asIdeal ∈ minimalPrimes ↑R
⊢ IsField ↑((Spec R).presheaf.stalk x)

Tactic:
← PrimeSpectrum.subsingleton_iff_isField_of_isReduced

Goal state after:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
inst✝ : IsReduced (Spec R)
hx : x.asIdeal ∈ minimalPrimes ↑R
⊢ Subsingleton (PrimeSpectrum ↑((Spec R).presheaf.stalk x))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
inst✝ : Finite ι
⊢ (⨅ i, I i).ideal = ⨅ i, (I i).ideal

Tactic:
by
  simpa using ideal_biInf I Set.finite_univ

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

Goal state before:
pp: case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
have : IsOpenImmersion (Spec.map φ) :=
      have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span {e}) :=
        IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
      IsOpenImmersion.of_isLocalization (1 - e)

Goal state after:
case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ ↑J.support ⊆ ⋂ U, X.zeroLocus ↑(I.ideal U)

Tactic:
J.coe_support_eq_eq_iInter_zeroLocus

Goal state after:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ ⋂ U, X.zeroLocus ↑(J.ideal U) ⊆ ⋂ U, X.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: ⊢ IsOpenImmersion =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] x ↦ Function.Bijective ⇑x

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

Goal state after:
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
⊢ (ΓSpecIso Γ(X, ↑V)).inv ≫ Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.app F ⊤ =
    X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE F (X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯

Tactic:
have H : ⊤ ≤ X.homOfLE (inf_le_left (b := V.1)) ⁻¹ᵁ U.1.ι ⁻¹ᵁ V.1 := by
        rw [← Scheme.Hom.comp_preimage, X.homOfLE_ι]; exact fun x _ ↦ by simpa using x.2.2

Goal state after:
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
H : ⊤ ≤ X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V
⊢ (ΓSpecIso Γ(X, ↑V)).inv ≫ Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.app F ⊤ =
    X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE F (X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = I.glueData.ι U

Tactic:
have H : inv (X.homOfLE inf_le_left : (U.1 ⊓ V.1).toScheme ⟶ U) = X.homOfLE (by simpa) := by
    rw [eq_comm, ← hom_comp_eq_id]; simp

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = I.glueData.ι U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
b : ↥I.glueData.glued
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
e : I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) = I.gluedTo b
⊢ (ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a = b

Tactic:
obtain ⟨ib, b : I.glueDataObj ib, rfl⟩ :=
    I.glueData.toGlueData.ι_jointly_surjective forget b

Goal state after:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
⊢ (ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a = (ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf✝ : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
left✝ : IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑a)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑a)))
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)

Tactic:
rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf✝ : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
left✝ : IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑a)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen ↑a).ι ''ᵁ ⊤)))
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case neg
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 := ⋯
x : S
i : ↑↑s
h : ¬l i = 0
⊢ l i ∈ ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
rw [Finset.coe_union, Finset.coe_image]

Goal state after:
case neg
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 ∈ ↑(s.attach.biUnion sf ∪ s) ∪ ⇑l '' ↑l.support
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝⁴ : Algebra R S := f.toAlgebra
this✝³ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝² : Algebra R' S' := f'.toAlgebra
this✝¹ : IsScalarTower R R' S'
this✝ : IsScalarTower R S S'
this : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
have : Module.Finite R S := hf

Goal state after:
R S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝⁵ : Algebra R S := f.toAlgebra
this✝⁴ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝³ : Algebra R' S' := f'.toAlgebra
this✝² : IsScalarTower R R' S'
this✝¹ : IsScalarTower R S S'
this✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
this : Module.Finite R S
⊢ (IsLocalization.map S' f ⋯).Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst✝ : LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
inst : JacobsonSpace ↥Y
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))

Tactic:
have inst : JacobsonSpace (Y.affineCover.X i) :=
      .of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝³ : LocallyOfFiniteType f
inst✝² : JacobsonSpace ↥Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y], (∃ S, Y = Spec S) → JacobsonSpace ↥X
hY : ¬∃ S, Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst✝¹ : LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
inst✝ : JacobsonSpace ↥Y
inst : JacobsonSpace ↥(Y.affineCover.X i)
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
⊢ liftCoborder f ⁻¹ᵁ U = f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
conv_rhs => enter [1]; rw [← f.liftCoborder_ι]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
⊢ liftCoborder f ⁻¹ᵁ U = (liftCoborder f ≫ (coborderRange f).ι) ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ RingHom.ker
      ((CommRingCat.Hom.hom (Hom.app f ((Hom.coborderRange f).ι ''ᵁ ↑U))).comp
        (RingHom.id ↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ ↑U))) =
    RingHom.ker (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) ↑U))

Tactic:
RingHomCompTriple.comp_eq,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ((Hom.coborderRange f).ι ''ᵁ ↑U))) =
    RingHom.ker (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) ↑U))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ IsNilpotent ((Algebra.lmul I.ResidueField (I.ResidueField ⊗[R] A)) (1 ⊗ₜ[R] f)) ↔
    ∀ i < Module.finrank R A, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

Tactic:
LinearMap.isNilpotent_iff_charpoly,

Goal state after:
case inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ LinearMap.charpoly ((Algebra.lmul I.ResidueField (I.ResidueField ⊗[R] A)) (1 ⊗ₜ[R] f)) =
      X ^ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) ↔
    ∀ i < Module.finrank R A, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
y : ↥(Spec (X.residueField x))
⊢ (fiberι f (f x)) ((asFiberHom f x) y) = (fiberι f (f x)) (asFiber f x)

Tactic:
by simp [← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this : IsReduced (Y.affineCover.X i)
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)

Tactic:
have : Finite ↑(irreducibleComponents ↥(Y.affineCover.X i)) := by
    let : IsNoetherian (Y.affineCover.X i) := {}
    exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this✝ : IsReduced (Y.affineCover.X i)
this : Finite ↑(irreducibleComponents ↥(Y.affineCover.X i))
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
⊢ IsOpen s

Tactic:
have _ : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    let 𝒰 := X.affineCover.finiteSubcover
    let p : ∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i) ⟶ X := Sigma.desc (fun i ↦ 𝒰.f i)
    refine this (f := (∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i)).isoSpec.inv ≫ p ≫ f) _ _ ?_ ⟨_, rfl⟩
    rw [← Category.assoc, Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]
    exact hs.preimage (_ ≫ p).continuous

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
i : ι
⊢ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT ≤ UY

Tactic:
subst hUY hVU

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
hUST : UT ≤ f ⁻¹ᵁ US
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
hUSX : iSup VX ≤ iX ⁻¹ᵁ US
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(X, iSup VX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (iSup VX) hUSX)).toAlgebra
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
⊢ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT ≤ g ⁻¹ᵁ iSup VX ⊓ iY ⁻¹ᵁ UT
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ IsOpenMap ⇑(𝔸(n; S) ↘ S)

Tactic:
change topologically @IsOpenMap _

Goal state after:
n : Type u
S : Scheme
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: R : CommRingCat
H : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
⊢ (Spec R).IsGermInjective

Tactic:
refine fun p ↦ ⟨?_⟩
  obtain ⟨f, hf, H⟩ := H p.asIdeal p.2
  refine ⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩
  · rw [← basicOpen_eq_of_affine]
    exact (isAffineOpen_top (Spec R)).basicOpen _
  rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
  intro x hx
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
    (S := ((Spec.structureSheaf R).obj.obj (.op <| PrimeSpectrum.basicOpen f))) (.powers f) x
  rw [← RingHom.mem_ker, IsLocalization.mk'_eq_mul_mk'_one, Ideal.mul_unit_mem_iff_mem,
    RingHom.mem_ker] at hx
  swap; · exact @isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)
  -- There is an `Opposite.unop (Opposite.op _)` in `hx` which doesn't seem removable using
  -- `simp`/`rw`.
  erw [elementwise_of% StructureSheaf.algebraMap_germ] at hx
  obtain ⟨⟨y, hy⟩, hy'⟩ := (IsLocalization.map_eq_zero_iff p.asIdeal.primeCompl
    ((Spec.structureSheaf R).presheaf.stalk p) _).mp hx
  obtain ⟨n, hn⟩ := H x y hy' hy
  refine (@IsLocalization.mk'_eq_zero_iff ..).mpr ?_
  exact ⟨⟨_, n, rfl⟩, hn⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Dominant

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
inst✝ : IsDominant f.hom
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
⊢ IsDominant (f.restrict U hU hU').hom

Tactic:
by
  dsimp only [restrict_domain, restrict_hom]
  have : IsDominant (X.homOfLE hU') := Opens.isDominant_homOfLE hU hU'
  rwa [IsDominant.comp_iff]

Goal state after:
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✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : (c.π.app i) x ∈ ↑V
this✝ : ∀ (j : (Over i)ᵒᵖ), IsAffine (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine ((opensDiagram D i V).obj j)
r : ↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
hrU : (((Functor.const I).obj c.pt).obj i).basicOpen r ≤ U
hxr : ↑⟨x, hxU⟩ ∈ (((Functor.const I).obj c.pt).obj i).basicOpen r
j : Over i
s : ((opensDiagram D i V).op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj (Opposite.op j)
hs :
  (ConcreteCategory.hom (((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).ι.app (Opposite.op j))) s =
    (ConcreteCategory.hom (c.π.app i ⁻¹ᵁ V).topIso.inv) r
⊢ ∃ U' ∈ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}, x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨s, rfl⟩ := (D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv.surjective s

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : (c.π.app i) x ∈ ↑V
this✝ : ∀ (j : (Over i)ᵒᵖ), IsAffine (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine ((opensDiagram D i V).obj j)
r : ↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V)
hrU : (((Functor.const I).obj c.pt).obj i).basicOpen r ≤ U
hxr : ↑⟨x, hxU⟩ ∈ (((Functor.const I).obj c.pt).obj i).basicOpen r
j : Over i
s : ↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V)
hs :
  (ConcreteCategory.hom (((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).ι.app (Opposite.op j)))
      ((D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv s) =
    (ConcreteCategory.hom (c.π.app i ⁻¹ᵁ V).topIso.inv) r
⊢ ∃ U' ∈ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}, x ∈ U' ∧ U' ≤ U
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (ConcreteCategory.hom (↾⇑(F.map fi))) xi = (ConcreteCategory.hom (↾⇑(F.map fj))) xj
⊢ (ConcreteCategory.hom ((G ⋙ forget).map fi)) ((s.app i) xi) =
    (ConcreteCategory.hom ((G ⋙ forget).map fj)) ((s.app j) xj)

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]

Goal state after:
J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (ConcreteCategory.hom (↾⇑(F.map fi))) xi = (ConcreteCategory.hom (↾⇑(F.map fj))) xj
⊢ (G.map fi) ((s.app i) xi) = (G.map fj) ((s.app j) xj)