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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ Set.range ⇑I.gluedTo = ↑I.support

Tactic:
refine subset_antisymm (Set.range_subset_iff.mpr fun x ↦ ?_) ?_
  · obtain ⟨ix, x : I.glueDataObj ix, rfl⟩ :=
      I.glueData.toGlueData.ι_jointly_surjective forget x
    change (I.glueData.ι _ ≫ I.gluedTo) x ∈ I.support
    rw [ι_gluedTo]
    exact ((I.range_glueDataObjι_ι_eq_support_inter ix).le ⟨_, rfl⟩).1
  · intro x hx
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
    obtain ⟨y, rfl⟩ := (I.range_glueDataObjι_ι_eq_support_inter ⟨U, hU⟩).ge ⟨hx, hxU⟩
    rw [← ι_gluedTo]
    exact ⟨_, rfl⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(ConcreteCategory.hom ((I.glueData.ι U).base ≫ I.gluedTo.base)) = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑U

Tactic:
← Scheme.Hom.comp_base,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U ≫ I.gluedTo) = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑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 = ⊤
h : ∀ (r : ↥s), ⊤.FG
⊢ FiniteType R S

Tactic:
choose t ht using h

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) = ⊤
⊢ FiniteType R S
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_1
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
h : 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))

pp: case refine_2
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
h :
  ∀ {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))
⊢ P = targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)

Tactic:
· rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
    lia

Goal state after:
case refine_2
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
h :
  ∀ {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))
⊢ P = targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ closure (Set.range ⇑(ConcreteCategory.hom ((Hom.toImage f).base ≫ (Hom.imageι f).base)))

Tactic:
← Scheme.Hom.comp_base,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ closure (Set.range ⇑(Hom.toImage f ≫ Hom.imageι f))
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'
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid S M) S' := by
    rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]

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'
⊢ (IsLocalization.map S' f ⋯).Finite
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 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 := algebraMap 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 := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
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.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))

Tactic:
simp_rw [Submonoid.map_powers] at hn₂

Goal state after:
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 := algebraMap 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 := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
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))
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    Submodule.span R
      ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
simp_rw [Submonoid.map_powers] at hn₂

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: 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
q : ↥(Spec (unop (F.obj S)))
U : Opens ↥X
hU : U ∈ X.affineOpens
hqU : S.hom q ∈ ↑U
⊢ ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧ Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)

Tactic:
obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hqf, hfU⟩ :=
        PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hqU (S.hom ⁻¹ᵁ U).isOpen

Goal state after:
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
q : ↥(Spec (unop (F.obj S)))
U : Opens ↥X
hU : U ∈ X.affineOpens
hqU : S.hom q ∈ ↑U
f : ↑(unop S.left)
hqf : q ∈ ↑(PrimeSpectrum.basicOpen f)
hfU : ↑(PrimeSpectrum.basicOpen f) ⊆ ↑(S.hom ⁻¹ᵁ U)
⊢ ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧ Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: case h
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
this✝² : Algebra R S := ⋯
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := ⋯
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away (f ↑r))
s₂ : ∀ (r : ↥s), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := ⋯
x : S
r : ↑↑s
n₁ : ℕ
hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑r ^ (n₂ + n₁) • x ∈
    Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))
⊢ ↑r ^ (n₂ + n₁) • x ∈ ⨆ x, Submodule.span R ↑(sf x)

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

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

Goal state before:
pp: case refine_1
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
⊢ ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))

Tactic:
have (q : Spec (F.obj S).unop) : ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧
        Q' Γ(Spec (F.obj S).unop, PrimeSpectrum.basicOpen f) := by
      obtain ⟨_, ⟨U, hU, rfl⟩, hqU, -⟩ :=
        X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ <| S.hom q) isOpen_univ
      obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hqf, hfU⟩ :=
        PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hqU (S.hom ⁻¹ᵁ U).isOpen
      have : LocallyOfFiniteType S.hom := hP _ S.prop
      exact ⟨f, hqf, _, ⟨U, rfl⟩, S.hom.appLE _ _ hfU,
        (S.hom.finiteType_appLE hU (.Spec_basicOpen _)) _⟩

Goal state after:
case refine_1
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
this :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧ Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)
⊢ ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ IsClosedImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
by rw [Scheme.Hom.toImage_imageι]; infer_instance

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ (Opens.map ((𝒰.f i).base ≫ f.base)).obj (Y.basicOpen s) ≤ 𝒰.f i ⁻¹ᵁ U

Tactic:
Opens.map_comp_obj

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ (Opens.map (𝒰.f i).base).obj ((Opens.map f.base).obj (Y.basicOpen s)) ≤ 𝒰.f i ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑(ConcreteCategory.hom ((Scheme.Hom.liftCoborder f).base ≫ (Scheme.Hom.coborderRange f).ι.base)) =
    ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f

Tactic:
← Scheme.Hom.comp_base,

Goal state after:
case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑(Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι) =
    ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f
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
⊢ Function.Injective ⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op))

Tactic:
← ConcreteCategory.mono_iff_injective_of_preservesPullback

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ IsAffine Y ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g)) →
    IsAffine (Limits.pullback f g) ∧
      Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))

Tactic:
⟨ha, hsurj⟩

Goal state after:
X✝ Y✝ Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal fun X x f [IsAffine x] ↦
    IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
ha : IsAffine Y
hsurj : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
⊢ IsAffine (Limits.pullback f g) ∧
    Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Limits.pullback.fst f g)))
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFinitePresentation f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f

Tactic:
locallyOfFinitePresentation_iff,

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FinitePresentation) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := ⋯
i : 𝒰.I₀
⊢ Γ(𝒰.X i, ⊤) ≅ Γ(X, ↑(fS i))

Tactic:
exact IsOpenImmersion.ΓIsoTop (𝒰.f i)

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap)
    (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
dsimp only [Scheme.Cover.pullbackHom]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (pullback.snd f (Y.affineCover.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
algInst✝¹ : Algebra ↑R ↑S := φ.hom'.toAlgebra
algInst✝ : Algebra (Polynomial ↑R) (Polynomial ↑S) := (Polynomial.mapRingHom φ.hom').toAlgebra
⊢ IsClosedMap (PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Tactic:
exact H₁.universally_isClosedMap (Spec.map (CommRingCat.ofHom Polynomial.C))
    (Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map _)
    (isPullback_SpecMap_of_isPushout _ _ _ _
    (CommRingCat.isPushout_of_isPushout R S (Polynomial R) (Polynomial S))).flip

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(ConcreteCategory.hom ((pullback.fst (𝒰.f i) f).base ≫ (𝒰.f i).base)) ⁻¹' s)

Tactic:
← Scheme.Hom.comp_base,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(pullback.fst (𝒰.f i) f ≫ 𝒰.f i) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝ : CompactSpace ↥X
this : X.IsQuasiAffine
⊢ IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))

Tactic:
have (r : Γ(Y, ⊤)) :
      IsPushout f.appTop (Y.presheaf.map (homOfLE le_top).op)
        (X.presheaf.map (homOfLE le_top).op) (f.appLE (Y.basicOpen r)
          (X.basicOpen (f.appTop r)) (Scheme.preimage_basicOpen_top ..).ge) := by
    have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r
    have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ (f.appTop r)
    refine CommRingCat.isPushout_of_isLocalization f.appTop.hom (f.appLE (Y.basicOpen r)
      (X.basicOpen (f.appTop r)) (Scheme.preimage_basicOpen_top ..).ge).hom ?_ (.powers r)
    change CommRingCat.Hom.hom (Y.presheaf.map _ ≫ f.appLE _ _ _) =
      CommRingCat.Hom.hom (f.appTop ≫ X.presheaf.map _)
    rw [f.map_appLE, Scheme.Hom.appLE]

Goal state after:
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)) ⋯)
⊢ IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))