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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
inst✝³ : I.IsPrime
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization.AtPrime A I
this : IsLocalRing A
⊢ ↑(IsLocalRing.maximalIdeal A).height = ↑I.height

Tactic:
← IsLocalization.height_under I.primeCompl,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
inst✝³ : I.IsPrime
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization.AtPrime A I
this : IsLocalRing A
⊢ ↑(under R (IsLocalRing.maximalIdeal A)).height = ↑I.height
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R : Type u
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f

Tactic:
S

Goal state after:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R : Type u
⊢ ∀ ⦃S : Type u⦄ (T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra S T]
    (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)

Tactic:
S

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
⊢ ∀ (T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra S T] (s : S)
    [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y : Scheme
⊢ ∀ ⦃S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)

Tactic:
S

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
⊢ ∀ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).affineOpenCover.openCover
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) :=
  fun ijk ↦
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).f ijk.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f ijk.fst) ∧
            P.2 ∈
              Scheme.Hom.opensRange ((𝒲 ijk.fst).f ijk.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f ijk.fst)},
      is_open' := ⋯ }
this : Set.range L ⊆ ↑(iSup U)
𝓤 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f g) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))
i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀
⊢ ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst) ≫ 𝒰.f i.fst =
    ((𝒱 i.fst).f i.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst) ≫ f

Tactic:
by simp [pullback.condition]

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

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).affineOpenCover.openCover
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) :=
  fun ijk ↦
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).f ijk.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f ijk.fst) ∧
            P.2 ∈
              Scheme.Hom.opensRange ((𝒲 ijk.fst).f ijk.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f ijk.fst)},
      is_open' := ⋯ }
this : Set.range L ⊆ ↑(iSup U)
𝓤 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f g) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))
i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀
⊢ ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst) ≫ 𝒰.f i.fst =
    ((𝒲 i.fst).f i.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f i.fst) ≫ g

Tactic:
by simp [pullback.condition]

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
this : Ideal.span (Set.range r) = ⊤
inst : ∀ (f : ↑Γ(X, ↑V)), IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ I.ideal V ≤ J.ideal V

Tactic:
refine Submodule.le_of_isLocalized_span _ this (fun i ↦ Γ(X, X.basicOpen i.1))
    (fun i ↦ Algebra.linearMap Γ(X, V.1) Γ(X, X.basicOpen i.1)) ?_

Goal state after:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
this : Ideal.span (Set.range r) = ⊤
inst : ∀ (f : ↑Γ(X, ↑V)), IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ ∀ (r_1 : ↑(Set.range r)),
    Submodule.localized₀ (Submonoid.powers ↑r_1) (Algebra.linearMap ↑Γ(X, ↑V) ↑Γ(X, X.basicOpen ↑r_1)) (I.ideal V) ≤
      Submodule.localized₀ (Submonoid.powers ↑r_1) (Algebra.linearMap ↑Γ(X, ↑V) ↑Γ(X, X.basicOpen ↑r_1)) (J.ideal V)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
R : Type u
⊢ ∀ {S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
S

Goal state after:
case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
hx : x ∈ ↑U
⊢ x ∈ I.supportSet ↔ x ∈ X.zeroLocus ↑(I.ideal U).radical

Tactic:
simp only [mem_supportSet_iff_of_mem hx, AlgebraicGeometry.Scheme.zeroLocus_radical]

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

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

Tactic:
by
  simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_glueDataObjι]
  rw [← Set.image_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsAffineOpen.isoSpec_inv_ι,
    IsAffineOpen.fromSpec_image_zeroLocus]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
⊢ IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f) (↑Γ(X, ↑U) ⧸ I.ideal U)

Tactic:
let := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal h)).toAlgebra

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

Goal state before:
pp: case e'_2.e'_6
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ x ∈
    Ideal.comap
      (CommRingCat.Hom.hom
        (X.presheaf.map
          ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ ((Hom.opensFunctor (X.basicOpen f).ι).map (eqToHom ⋯)).op ≫ eqToHom ⋯)))
      (I.ideal (X.affineBasicOpen f))

Tactic:
exact I.ideal_le_comap_ideal (U := X.affineBasicOpen f) (V := V)
    (hfg.trans_le (X.basicOpen_le g)) hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv = (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial ≫ (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom

Tactic:
← ΓSpecIso_hom_stalkClosedPointIso_inv,

Goal state after:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ ((Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv) ≫ (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i) ∩ (↑↑V ∩ ↑(X.basicOpen ↑i)))

Tactic:
refine (hs₂ i (hs' i.2)).isQuasiSeparated _ _ Set.inter_subset_right
    (U.1.2.inter (X.basicOpen _).2) ?_ Set.inter_subset_right (V.1.2.inter (X.basicOpen _).2) ?_

Goal state after:
case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i))

case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ ∀ i ∈ ⇑(ConcreteCategory.hom U.topIso.inv) '' s, IsAffineOpen ((↑U).basicOpen i)

Tactic:
rintro _ ⟨j, hj, rfl⟩

Goal state after:
case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen ((↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) j))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ ∀ (s : Finset ↑Γ(Y, ⊤)), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X

Tactic:
S

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
⊢ Ideal.span ↑S = ⊤ → (∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
⊢ IsAffineOpen (coprod.desc f g ⁻¹ᵁ W)

Tactic:
convert! isAffineOpen_opensRange i

Goal state after:
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
⊢ coprod.desc f g ⁻¹ᵁ W = Scheme.Hom.opensRange i
Module: Mathlib.RingTheory.RingHom.EssFiniteType

Goal state before:
pp: R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R T).EssFiniteType
⊢ (algebraMap S (TensorProduct R S T)).EssFiniteType

Tactic:
rw [essFiniteType_algebraMap] at h ⊢
    infer_instance

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

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
x : ↥I.glueData.glued
⊢ I.gluedTo x ∈ ↑I.support

Tactic:
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

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y : Scheme
⊢ ∀ ⦃S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)

Tactic:
S

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
hQb : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
⊢ ∀ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) g →
      affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (Limits.pullback.fst f g)
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
⊢ JacobsonSpace ↥X

Tactic:
have inst : JacobsonSpace (Spec R) := ‹_› -- TC gets stuck on the WLOG hypothesis without it.
    rw [X.affineCover.isOpenCover_opensRange.jacobsonSpace_iff]
    intro i
    have := this _ (X.affineCover.f i ≫ f) ⟨_, rfl⟩
    let e := (X.affineCover.f i).isOpenEmbedding.isEmbedding.toHomeomorph
    exact .of_isClosedEmbedding e.symm.isClosedEmbedding

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
⊢ IsClosedEmbedding ⇑f

Tactic:
by
    have h := (f ≫ g).isClosedEmbedding
    simp only [Scheme.Hom.comp_base, TopCat.coe_comp] at h
    refine .of_continuous_injective_isClosedMap (Scheme.Hom.continuous f) h.injective.of_comp ?_
    intro Z hZ
    rw [IsClosedEmbedding.isClosed_iff_image_isClosed g.isClosedEmbedding,
      ← Set.image_comp]
    exact h.isClosedMap _ hZ

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

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

Tactic:
S

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.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ comap (Ideal.Quotient.mk I) ''
      ⇑{ toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ } ⁻¹' ↑(basicOpen (↑C).f) =
    (↑C).toSet

Tactic:
ContinuousMap.coe_mk,

Goal state after:
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ comap (Ideal.Quotient.mk I) '' comap (Ideal.Quotient.mk I) ⁻¹' ↑(basicOpen (↑C).f) = (↑C).toSet
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 f ∣_ Hom.opensRange ((diagonalCover f 𝒰 𝒱).f ⟨i.fst, (i.snd, i.snd)⟩))

Tactic:
MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (diagonalRestrictIsoDiagonal ..)

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
this : IsClosedImmersion (pullback.diagonal (f ≫ g))
⊢ IsSeparated f

Tactic:
rw [pullback.diagonal_comp] at this

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
this :
  IsClosedImmersion
    (pullback.diagonal f ≫
      (pullbackDiagonalMapIdIso f f g).inv ≫
        pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))
⊢ IsSeparated f