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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact ↑V
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this✝¹ : IsAffine ↑U
this✝ : IsAffine ↑W
this : CompactSpace ↥↑V
f' : ↑U ⟶ ↑W := Scheme.Hom.resLE f W U hUW
q : ↑V ⟶ ↑W := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
p : pullback f' q ⟶ pullback f g := pullback.map f' q f g U.ι V.ι W.ι ⋯ ⋯
⊢ IsCompact (↑(pullback.fst f g ⁻¹ᵁ U) ⊓ ↑(pullback.snd f g ⁻¹ᵁ V))

Tactic:
convert! isCompact_range p.continuous

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact ↑V
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this✝¹ : IsAffine ↑U
this✝ : IsAffine ↑W
this : CompactSpace ↥↑V
f' : ↑U ⟶ ↑W := Scheme.Hom.resLE f W U hUW
q : ↑V ⟶ ↑W := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
p : pullback f' q ⟶ pullback f g := pullback.map f' q f g U.ι V.ι W.ι ⋯ ⋯
⊢ ↑(pullback.fst f g ⁻¹ᵁ U) ⊓ ↑(pullback.snd f g ⁻¹ᵁ V) = Set.range ⇑p
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R✝ S✝ T✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
inst✝² : CommRing T✝
inst✝¹ : Algebra R✝ S✝
inst✝ : Algebra R✝ T✝
a✝ : Module.Finite R✝ T✝
⊢ Module.Finite S✝ (S✝ ⊗[R✝] T✝)

Tactic:
infer_instance

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

Goal state before:
pp: case h₂
R S T : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.FiniteType R T
⊢ Algebra.FiniteType S (S ⊗[R] T)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : LocallyOfFiniteType f
⊢ LocallyOfFiniteType (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance

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

Goal state before:
pp: case refine_1.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
· dsimp
      exact fun q ↦ ⟨_, hf q, ⟨(IsLocalization.algEquiv (.powers (f q)) _
        ((Spec.structureSheaf _).obj.obj (op _))).toRingEquiv.toCommRingCatIso⟩⟩

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

Goal state before:
pp: case hprecomp
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
hf : IsClosedImmersion f
⊢ IsClosedImmersion (e.hom ≫ f)

Tactic:
infer_instance

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

Goal state before:
pp: case hpostcomp
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hf : IsClosedImmersion f
⊢ IsClosedImmersion (f ≫ e.hom)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsClosedImmersion f

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (MorphismProperty.diagonal @IsClosedImmersion).RespectsIso

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderComposition

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderBaseChange

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (MorphismProperty.diagonal @IsClosedImmersion)

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : IsSeparated f
⊢ IsSeparated (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsClosedImmersion (pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))))

Tactic:
rw [diagonal_SpecMap, MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion]

Goal state after:
W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsClosedImmersion (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' ↑R).toRingHom))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated (Spec.map (Scheme.Hom.appTop f))

Tactic:
infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsPreimmersion f

Tactic:
infer_instance

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

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
⊢ ∀ {g' : Y' ⟶ X}, IsPullback f' g' g f → IsImmersion g → IsImmersion g'

Tactic:
g'

Goal state after:
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
⊢ IsPullback f' g' g f → IsImmersion g → IsImmersion g'
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✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
x : S
hx : x ∈ ↑s
this : FinitePresentation R (Localization.Away ↑⟨x, hx⟩)
⊢ FiniteType R (Localization.Away x)

Tactic:
infer_instance

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✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ 1 ∈ Ideal.span ↑s

Tactic:
rw [hs]; trivial

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

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ IsImmersion (pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯ ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι)

Tactic:
infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : IsImmersion f
⊢ IsImmersion (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)

Tactic:
infer_instance

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

Goal state before:
pp: case hf
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ Mono (X.presheaf.map (eqToHom ⋯).op)

Tactic:
infer_instance

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

Goal state before:
pp: case h₂
R✝ S✝ T✝ : Type u_1
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
inst✝² : CommRing T✝
inst✝¹ : Algebra R✝ S✝
inst✝ : Algebra R✝ T✝
a✝ : Algebra.FinitePresentation R✝ T✝
⊢ Algebra.FinitePresentation S✝ (S✝ ⊗[R✝] T✝)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i ↦ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.I₀) × (𝒱 i).I₀),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.I₀) × (𝒱 i).I₀
⊢ IsClosedImmersion (pullback.diagonal ((𝒱 i.fst).f i.snd ≫ pullback.snd f (𝒰.f i.fst)))

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
⊢ IsClosedImmersion J.subschemeι

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
X : Scheme
R : CommRingCat
I : Ideal ↑R
e : X ≅ Spec (CommRingCat.of (↑R ⧸ I))
⊢ IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : X.IsSeparated
⊢ IsSeparated (terminal.from X)

Tactic:
infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ HasAffineProperty @IsSeparated fun X x x_1 x_2 ↦ X.IsSeparated

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsSeparated with X Y f hY
  rw [Scheme.isSeparated_iff, ← terminal.comp_from f, IsSeparated.comp_iff]
  rfl

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

Goal state before:
pp: case neg
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
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
this : IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom X.affineCover g i)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : LocallyOfFinitePresentation f
⊢ LocallyOfFinitePresentation (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

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

Tactic:
infer_instance

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

Goal state before:
pp: P Q : ObjectProperty Scheme
⊢ geometrically (P ⊓ Q) = geometrically P ⊓ geometrically Q

Tactic:
simp only [geometrically_eq_universally, ← MorphismProperty.universally_inf]

Goal state after:
P Q : ObjectProperty Scheme
⊢ (MorphismProperty.universally fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → (P ⊓ Q) X) =
    ((fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X) ⊓ fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → Q X).universally
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
⊢ (MorphismProperty.universally fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X).IsStableUnderBaseChange

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
⊢ NoetherianSpace ↥X

Tactic:
apply TopologicalSpace.noetherian_univ_iff.mp

Goal state after:
X : Scheme
inst✝ : IsNoetherian X
⊢ NoetherianSpace ↑Set.univ
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : IsNoetherianRing ↑(CommRingCat.of R)
⊢ IsNoetherian (Spec (CommRingCat.of R))

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsOpenMap).universally.IsStableUnderComposition

Tactic:
infer_instance

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ S
g : Y ⟶ S
pX : Z ⟶ X
pY : Z ⟶ Y
H : IsPullback pX pY f g
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
⊢ IsSchemeTheoreticallyDominant (H.isoPullback.hom ≫ pullback.snd f g)

Tactic:
infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyIrreducible f
inst✝² : GeometricallyIrreducible g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ IrreducibleSpace ↥(pullback f (pullback.fst g x))

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsClosedMap).universally.IsStableUnderComposition

Tactic:
infer_instance

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

Goal state before:
pp: R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
int : Algebra.IsIntegral R T
⊢ Algebra.IsIntegral S (S ⊗[R] T)

Tactic:
infer_instance

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsAffine (Spec S)

Tactic:
infer_instance

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

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ 1 ∈ ↑(coeffSubmodule R₀ e)

Tactic:
exact one_mem_coeffSubmodule

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
h : Mono (Scheme.Hom.app f ⊤).op
⊢ Epi (Scheme.Hom.app f ⊤).op.unop

Tactic:
infer_instance

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

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

Tactic:
have inst := X.isoSpec.inv.isOpenEmbedding.injective.subsingleton

Goal state after:
case inr
X : Scheme
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst✝ : JacobsonSpace ↥(Spec S)
this :
  ∀ {X : Scheme} [Subsingleton ↥X] [IsReduced X] {f : X ⟶ Spec S},
    (∃ R, X = Spec R) → (IsFinite f ↔ LocallyOfFiniteType f)
hX : ¬∃ R, X = Spec R
inst : Subsingleton ↥(Spec Γ(X, ⊤))
⊢ IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
φ : S ⟶ R
⊢ T1Space ↥(Spec R)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsSeparated (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsIso ⊥.subschemeι

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ IsImmersion (f ≫ Y.toSpecΓ)

Tactic:
infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : Flat f
⊢ Flat (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance

Goal state after:
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
⊢ QuasiSeparatedSpace ↥X

Tactic:
choose r hr hxr using H

Goal state after:
X : Scheme
inst✝ : CompactSpace ↥X
r : ↥X → ↑Γ(X, ⊤)
hr : ∀ (x : ↥X), IsAffineOpen (X.basicOpen (r x))
hxr : ∀ (x : ↥X), x ∈ X.basicOpen (r x)
⊢ QuasiSeparatedSpace ↥X
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
eval₂_X

Goal state after:
n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
⊢ Scheme.Spec.map (Hom.appLE f (Y.basicOpen ↑r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) ⋯).op ≫
      ⋯.isoSpec.symm.hom =
    e.symm.hom ≫ Cover.pullbackHom Y.openCoverBasicOpenTop f r

Tactic:
simp only [Iso.symm_hom, Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]
    dsimp [e, Scheme.Cover.pullbackHom, IsAffineOpen.isoSpec_hom, Scheme.Hom.appLE]
    simp only [homOfLE_leOfHom, Spec.map_comp, Category.assoc,
      Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Scheme.Opens.toSpecΓ_naturality]
    simp_rw [← Category.assoc]
    congr 1
    rw [← cancel_mono (Scheme.Opens.ι _)]
    simp [pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f g : X ⟶ 𝔸(n; S)
h₁ : f ≫ 𝔸(n; S) ↘ S = g ≫ 𝔸(n; S) ↘ S
h₂ :
  ∀ (i : n),
    (ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)
⊢ f = g

Tactic:
apply pullback.hom_ext h₁
  change f ≫ toSpecMvPoly _ _ = g ≫ toSpecMvPoly _ _
  apply (toSpecMvPolyIntEquiv n).injective
  ext i
  rw [toSpecMvPolyIntEquiv_comp, toSpecMvPolyIntEquiv_comp]
  exact h₂ i

Goal state after:
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 ↥(Spec (CommRingCat.of (MvPolynomial n ↑(CommRingCat.of K))))

Tactic:
infer_instance

Goal state after:
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 (Spec (CommRingCat.of (MvPolynomial n ↑(CommRingCat.of K))))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mpr.inl
n : Type u
S : Scheme
h✝ : IsEmpty ↥S
⊢ IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mpr.inr
n : Type u
S : Scheme
h✝ : IsEmpty n
⊢ IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosedImmersion (X.fromSpecResidueField x)
⊢ LocallyOfFiniteType (X.fromSpecResidueField x ≫ f)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ IsIntegralHom (X.fromSpecResidueField x ≫ f)

Tactic:
infer_instance

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
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)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
i : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ D.obj (unop i) ≤ iX ⁻¹ᵁ US

Tactic:
grw [← hUSX, ← h]; exact le_iSup D.obj i.unop

Goal state after: