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

Goal state before:
pp: X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U : Set ↥X
⊢ ∀ (V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
V

Goal state after:
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U V : Set ↥X
⊢ IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
⊢ ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier

Tactic:
V

Goal state after:
case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
⊢ IsCompact V.carrier → IsCompact (U ⊓ V).carrier
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
S : X.Opens
x✝ : IsCompact S.carrier
⊢ ∀ (U_1 : ↑X.affineOpens), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ ↑U_1)).carrier

Tactic:
V

Goal state after:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ ↑V)).carrier
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
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)

Tactic:
let U (ijk : Σ i, (𝒱 i).I₀ × (𝒲 i).I₀) : TopologicalSpace.Opens (X.carrier × Y) :=
    ⟨{ P | P.1 ∈ ((𝒱 ijk.1).f ijk.2.1 ≫ (𝒰.pullback₁ f).f ijk.1).opensRange ∧
          P.2 ∈ ((𝒲 ijk.1).f ijk.2.2 ≫ (𝒰.pullback₁ g).f ijk.1).opensRange },
      (continuous_fst.1 _ ((𝒱 ijk.1).f ijk.2.1 ≫
      (𝒰.pullback₁ f).f ijk.1).opensRange.2).inter (continuous_snd.1 _
      ((𝒲 ijk.1).f ijk.2.2 ≫ (𝒰.pullback₁ g).f ijk.1).opensRange.2)⟩

Goal state after:
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' := ⋯ }
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U : ↑X.affineOpens
⊢ ∀ (V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
V

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
⊢ IsCompact (↑↑U ∩ ↑↑V)
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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
⊢ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))

Tactic:
V

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
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
⊢ ∀ (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
⊢ IsQuasiSeparated ⊥.carrier →
    ∀ (f : ↑Γ(X, ⊥)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
intro _ f x

Goal state after:
case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU'✝ : IsQuasiSeparated ⊥.carrier
f : ↑Γ(X, ⊥)
x : ↑Γ(X, X.basicOpen f)
⊢ ∃ n y,
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
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
R S : CommRingCat
φ : R ⟶ S
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
have H := (isLocal_ringHomProperty P).respectsIso

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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

Tactic:
Ideal.height_le_iff

Goal state after:
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ))

Tactic:
← RingHom.ker_equiv_comp _ (Scheme.ΓSpecIso _).commRingCatIsoToRingEquiv,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker
      ((ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).commRingCatIsoToRingEquiv.toRingHom.comp
        (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv)))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑((IsAffineOpen.isoSpec ⋯).inv ≫ (↑U).ι) '' PrimeSpectrum.zeroLocus ↑(I.ideal U) = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
IsAffineOpen.isoSpec_inv_ι,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.fromSpec ⋯) '' PrimeSpectrum.zeroLocus ↑(I.ideal U) = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U
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
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
wlog h : IsAffine X ∧ IsAffine Y generalizing X Y f
  · obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)
    obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ U from hfx)
    rw [← hQ'.arrow_mk_iso_iff (Scheme.Hom.resLEStalkMap f e ⟨x, hx⟩)]
    exact this (IsZariskiLocalAtSource.resLE _ hf) _ ⟨hV, hU⟩
  obtain ⟨hX, hY⟩ := h
  wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
  · have : Q' ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom).stalkMap (X.isoSpec.hom x)).hom := by
      refine this ?_ (X.isoSpec.hom x) inferInstance inferInstance ?_
      · rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
      · use Γ(Y, ⊤), Γ(X, ⊤)
    rw [Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp,
      hQ'.cancel_right_isIso, CommRingCat.hom_comp, hQ'.cancel_left_isIso] at this
    have heq : (X.isoSpec.inv (X.isoSpec.hom x)) = x := by simp
    rwa [hQ'.arrow_mk_iso_iff (f.arrowStalkMapIsoOfEq heq)] at this
  obtain ⟨R, S, rfl, rfl⟩ := hXY
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  rw [hQ'.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)]
  rw [Spec_iff (P := P)] at hf
  apply hQ _ hf

Goal state after:
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 : ↑X.affineOpens
⊢ ∀ (V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
V

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
⊢ IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ (↑i ⊓ ↑j).ι =
    pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i).ι

Tactic:
rw [← pullback.condition_assoc, pullback.condition_assoc (f := I.glueDataObjι i),
          X.homOfLE_ι]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
a : ↥I.glueData.glued
⊢ ∀ ⦃a₂ : ↥I.glueData.glued⦄, I.gluedTo a = I.gluedTo a₂ → a = a₂

Tactic:
b

Goal state after:
X : Scheme
I : X.IdealSheafData
a b : ↥I.glueData.glued
⊢ I.gluedTo a = I.gluedTo b → a = b
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
U : J.subschemeCover.openCover.I₀
⊢ ∀ (y : J.subschemeCover.openCover.I₀),
    pullback.fst (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f y) ≫
        glueDataObjHom h U ≫ I.subschemeCover.f U =
      pullback.snd (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f y) ≫
        glueDataObjHom h y ≫ I.subschemeCover.f y

Tactic:
V

Goal state after:
X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ pullback.fst (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f V) ≫
      glueDataObjHom h U ≫ I.subschemeCover.f U =
    pullback.snd (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f V) ≫
      glueDataObjHom h V ≫ I.subschemeCover.f V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U✝ : ↑Y.affineOpens
U : (Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).I₀
⊢ ∀ (y : (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 y) ≫
        liftQuotient (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ) ((ker f).ideal U) ⋯ ≫ (ker f).subschemeCover.f U =
      pullback.snd ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f U)
          ((Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯)).f y) ≫
        liftQuotient (pullback.snd f (↑y).ι ≫ (↑y).toSpecΓ) ((ker f).ideal y) ⋯ ≫ (ker f).subschemeCover.f y

Tactic:
V

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

Goal state before:
pp: case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme),
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffine Y → IsAffineHom f
hY : ¬IsAffine Y
⊢ IsAffineHom f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]

Goal state after:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme),
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), P f → IsAffine Y → IsAffineHom f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), IsAffineHom (f ∣_ ↑i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U : X.Opens
⊢ ∀ (V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

Tactic:
V

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : X.Opens
⊢ IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : R →+* S
s : ConstructibleSetData R
⊢ map (f.comp g) s = map f (map g s)

Tactic:
by
  simp [map, image_image, Function.comp_def, BasicConstructibleSetData.map_comp']

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

Goal state before:
pp: case mp
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsClosedImmersion f → ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

pp: case mpr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ (∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) → IsClosedImmersion f

Tactic:
· intro H
    obtain ⟨h₁, h₂⟩ := IsClosedImmersion.isAffine_surjective_of_isAffine f
    let φ := (Scheme.ΓSpecIso R).inv ≫ f.appTop
    refine ⟨RingHom.ker φ.1, Scheme.isoSpec _ ≪≫ Scheme.Spec.mapIso
        (.op (RingEquiv.ofBijective φ.1.kerLift ?_).toCommRingCatIso), ?_⟩
    · exact ⟨φ.1.kerLift_injective, Ideal.Quotient.lift_surjective_of_surjective _ _
        (h₂.comp (Scheme.ΓSpecIso R).commRingCatIsoToRingEquiv.symm.surjective)⟩
    · simp only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map,
        Quiver.Hom.unop_op, Category.assoc, ← Spec.map_comp]
      change f = X.isoSpec.hom ≫ Spec.map φ
      simp only [Scheme.isoSpec, asIso_hom, Spec.map_comp, ← Scheme.toSpecΓ_naturality_assoc,
        ← SpecMap_ΓSpecIso_hom, φ]
      simp

Goal state after:
case mpr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ (∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) → IsClosedImmersion f
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ Y✝ Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
⊢ LocallyOfFiniteType f

Tactic:
HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType,

Goal state after:
X✝ Y✝ Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ NoetherianSpace ↑?m.46

Tactic:
convert! noetherianSpace_of_isAffineOpen U hU
      apply IsLocallyNoetherian.component_noetherian ⟨U, hU⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U : ↑X.affineOpens
⊢ ∀ (V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
V

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
⊢ IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ (∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)) → IsNoetherian X

Tactic:
intro hNoeth
    convert! IsNoetherian.mk
    · exact (isLocallyNoetherian_iff_of_affine_openCover _).mpr hNoeth
    · exact Scheme.OpenCover.compactSpace 𝒰

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

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Function.Injective ⇑(ConcreteCategory.hom (pushoutSection ⋯ hVU ⋯ ⋯))
⊢ x ∈ ⊥

Tactic:
refine CommRingCat.inr_injective_of_flat (f.appLE U (f ⁻¹ᵁ U) le_rfl) (g.appLE U V hVU)
    (by simpa [Scheme.Hom.appLE] using f.app_injective U) (g.flat_appLE hU hV hVU) ?_

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Function.Injective ⇑(ConcreteCategory.hom (pushoutSection ⋯ hVU ⋯ ⋯))
⊢ (ConcreteCategory.hom (pushout.inr (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU))) x =
    (ConcreteCategory.hom (pushout.inr (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯) (Scheme.Hom.appLE g U V hVU))) 0