mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
⊢ ringKrullDim R ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n

Tactic:
rw [ringKrullDim, Order.krullDim_eq_iSup_height, iSup_le_iff]
  refine ⟨fun h p hp ↦ ?_, fun h p ↦ ?_⟩
  · rw [Ideal.height_eq_primeHeight]
    exact h ⟨p, hp⟩
  · specialize h p.2
    rwa [Ideal.height_eq_primeHeight] at h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s ^ n = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0

Tactic:
rw [← map_pow, ← map_zero (X.presheaf.germ _ x hxU).hom] at e

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : (X : Scheme) → ↥X → Prop
h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
⊢ ∀ (X : Scheme) (x : ↥X), P X x

Tactic:
intro X x
  obtain ⟨y, e⟩ := X.affineCover.covers x
  convert! h₂ (X.affineCover.f (X.affineCover.idx x)) y _
  · rw [e]
  apply h₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case neg
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
hxU : x ∉ ↑U
⊢ x ∈ I.supportSet ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
· simp [hxU]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) ∩ ↑↑U ↔
    x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z))

Tactic:
· simp [hxU]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ f₁ = f₂ ↔ ∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd

Tactic:
by
  constructor
  · rintro rfl
    simp
  · obtain ⟨f, _⟩ := f₁
    obtain ⟨g, _⟩ := f₂
    rintro ⟨(rfl : f = g), h⟩
    simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ (∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd) → T₁ = T₂

Tactic:
obtain ⟨T, _⟩ := T₁

Goal state after:
case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
T : Triplet f g
snd✝ : ↥(Spec T.tensor)
⊢ (∃ (e : ⟨T, snd✝⟩.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) ⟨T, snd✝⟩.snd = T₂.snd) → ⟨T, snd✝⟩ = T₂
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
⊢ Nonempty ↥(pullback f g)

Tactic:
have : Nonempty S := .map f ‹_›

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
this : Nonempty ↥S
⊢ Nonempty ↥(pullback f g)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
⊢ Hom.ker X.toSpecΓ = ⊥

Tactic:
apply IdealSheafData.ext_of_isAffine

Goal state after:
X : Scheme
inst✝ : CompactSpace ↥X
⊢ (Hom.ker X.toSpecΓ).ideal ⟨⊤, ⋯⟩ = ⊥.ideal ⟨⊤, ⋯⟩
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ (I.glueData.ι ix ≫ I.gluedTo) x ∈ I.support

Tactic:
rw [ι_gluedTo]

Goal state after:
case refine_1
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ (I.glueDataObjι ix ≫ (↑ix).ι) x ∈ I.support
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U = ↑↑U ∩ Set.range ⇑I.gluedTo

Tactic:
range_gluedTo,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U = ↑↑U ∩ ↑I.support
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
isAffineHom_iff

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
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) = ⊤
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
r : ↑↑s
⊢ ∃ n, ↑r ^ n • x ∈ adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

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

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
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ n, ↑r ^ n • x ∈ adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))
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
hQi : 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
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
isAffineHom_iff

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔
        (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
          ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U✝ : ↑Y.affineOpens
U V : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀
⊢ (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U)
          ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f V) ≫
        liftQuotient (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ) ((ker f).ideal U) ⋯ ≫ (ker f).subschemeCover.f U) ≫
      imageι f =
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U)
          ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f V) ≫
        liftQuotient (pullback.snd f (↑V).ι ≫ (↑V).toSpecΓ) ((ker f).ideal V) ⋯ ≫ (ker f).subschemeCover.f V) ≫
      imageι f

Tactic:
simp [IdealSheafData.glueDataObjι, Scheme.Hom.liftQuotient_comp_assoc,
      ← pullback.condition, ← pullback.condition_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
x✝² x✝¹ : (Over Y)ᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ Over.Hom.left
      ((Y.kerFunctor ⋙ (subschemeFunctor Y).rightOp).map x✝ ≫
          (Over.homMk (Hom.toImage (Opposite.unop x✝¹).hom) ⋯).op).unop =
    Over.Hom.left ((Over.homMk (Hom.toImage (Opposite.unop x✝²).hom) ⋯).op ≫ (𝟭 (Over Y)ᵒᵖ).map x✝).unop

Tactic:
simp [← cancel_mono (subschemeι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y✝ : Scheme
f : X ⟶ Y✝
U : ↑Y✝.affineOpens
Y : Scheme
I : Y.IdealSheafData
⊢ Over.Hom.left
      ((subschemeFunctor Y).rightOp.map ({ app := fun I ↦ eqToHom ⋯, naturality := ⋯ }.app I) ≫
          { app := fun f ↦ (Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯).op, naturality := ⋯ }.app
            ((subschemeFunctor Y).rightOp.obj I)).unop =
    Over.Hom.left (𝟙 ((subschemeFunctor Y).rightOp.obj I)).unop

Tactic:
simp [← cancel_mono (subschemeι _)]

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

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↥(Spec R)
⊢ JacobsonSpace ↥X

Tactic:
rw [X.affineCover.isOpenCover_opensRange.jacobsonSpace_iff]

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↥(Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [JacobsonSpace ↥(Spec R)],
    (∃ S, X = Spec S) → JacobsonSpace ↥X
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↥(Spec R)
⊢ ∀ (i : X.affineCover.I₀), JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case inr
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
⊢ IsClosedImmersion g

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) X.affineCover]

Goal state after:
case inr
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
⊢ ∀ (i : X.affineCover.toPreZeroHypercover.1), IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    ⇑(TopCat.Hom.hom f.base) ''
      (s ∩ Set.range ⇑(TopCat.Hom.hom ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i).base))

Tactic:
simp [IsOpenImmersion.range_pullbackFst, Set.image_inter_preimage]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_1
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ pullback ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField))) (map (CommRingCat.ofHom (algebraMap R S)))

Tactic:
refine pullback.congrHom
      (Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField (.of R) p).symm rfl ≪≫ ?_
    refine asIso <| pullback.map _ _ _ _ (Spec.map <| (Scheme.Spec.residueFieldIso (.of R) _).inv)
      (𝟙 _) (𝟙 _) (by simp) (by simp)

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
s : ↑Γ(Y, U)
hs : (ConcreteCategory.hom (app f U)) s = 0
⊢ s = 0

Tactic:
refine Y.IsSheaf.section_ext fun x hx ↦ ?_

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
s : ↑Γ(Y, U)
hs : (ConcreteCategory.hom (app f U)) s = 0
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op U)),
      x ∈ V ∧
        (ConcreteCategory.hom (Y.presheaf.map (homOfLE hV).op)) s =
          (ConcreteCategory.hom (Y.presheaf.map (homOfLE hV).op)) 0
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: ⊢ @GeometricallyIrreducible = geometrically fun x ↦ IrreducibleSpace ↥x

Tactic:
by
  ext; exact geometricallyIrreducible_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
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

Tactic:
gcongr

Goal state after:
case hUU'
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) := ⋯
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) := ⋯
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) := ⋯
⊢ VX i ≤ iSup VX
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ Surjective (Spec.map (CommRingCat.ofHom C))

Tactic:
exact ⟨MvPolynomial.comap_C_surjective⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (terminal.from (Spec ℤ[n]))

Tactic:
rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C))]

Goal state after:
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
y : Y
z : X
hz : z ∈ Function.support (Pi.single x y)
⊢ z ∈ univ

Tactic:
by tauto

Goal state after:
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
x : X
hx : x ∈ D.support
⊢ x ∈ {x | D x = 0}ᶜ

Tactic:
by tauto

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_1
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
j : Fin n
⊢ (e₂.val j).degree.succ ≤ (e.val j).degree.succ

Tactic:
gcongr

Goal state after:
case hxy
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
degBound_e₁_le : e₁.degBound ≤ e.degBound
j : Fin n
⊢ (e₂.val j).degree ≤ (e.val j).degree
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ (e₂.val i).degree.succ < (e.val i).degree.succ

Tactic:
gcongr

Goal state after:
case hxy
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := ⋯
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := ⋯
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n := ⋯
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⋯
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ (e₂.val i).degree < (e.val i).degree
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z).Finite

Tactic:
obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z).Finite

Tactic:
obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z).Finite
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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h✝ : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
X✝ Y✝ : X.Opens
h : X✝ ⟶ Y✝
⊢ g ⁻¹ᵁ X✝ ⊓ iY ⁻¹ᵁ UT ≤ g ⁻¹ᵁ Y✝ ⊓ iY ⁻¹ᵁ UT

Tactic:
gcongr

Goal state after:
case hUU'
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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := ⋯
h✝ : iSup D.obj = UX
c₀ : Cocone D := ⋯
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat := ⋯
X✝ Y✝ : X.Opens
h : X✝ ⟶ Y✝
⊢ X✝ ≤ Y✝
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
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        (X.presheaf.germ (Scheme.Hom.opensRange (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) x ⋯))

Tactic:
have : Nonempty (X.affineCover.f _).opensRange := ⟨⟨_, X.affineCover.covers x⟩⟩

Goal state after:
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)))
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        (X.presheaf.germ (Scheme.Hom.opensRange (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) x ⋯))