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

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv

Tactic:
gluing_J

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
⊢ U i = Scheme.Hom.opensRange (𝒰.f i)

Tactic:
exact (Scheme.Opens.opensRange_ι _).symm

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
by
  constructor
  · intro ⟨s, hsone, hs⟩
    obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hsone
    exact ⟨s', h₂, fun t ht ↦ hs t (h₁ ht)⟩
  · intro ⟨s, hsone, hs⟩
    use s, hsone, hs

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
⊢ Q.diagonal f

Tactic:
refine (diagonal_iff (targetAffineLocally Q)).mpr ?_

Goal state after:
Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
⊢ (targetAffineLocally Q).diagonal f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case respectsIso.h₁
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
e : X ≅ Y
f✝ : Y ⟶ Z
inst✝ : IsAffine Z
H : CompactSpace ↥Y
⊢ CompactSpace ↥X

pp: case respectsIso.h₂
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
e : Y ≅ Z
f✝ : X ⟶ Y
inst✝ : IsAffine Y
H : CompactSpace ↥X
⊢ CompactSpace ↥X

Tactic:
exacts [@Homeomorph.compactSpace _ _ _ _ H (TopCat.homeoOfIso (asIso e.inv.base)), H]

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

Goal state before:
pp: case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this✝ :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
inst : QuasiCompact (g ≫ f)
this : StableUnderSpecialization (⇑(g ≫ f) '' ⇑g ⁻¹' Z) → (∃ R_1, Spec R = Spec R_1) → IsClosed (⇑(g ≫ f) '' ⇑g ⁻¹' Z)
⊢ IsClosed (⇑f '' Z)

Tactic:
simp_rw [Scheme.Hom.comp_base, TopCat.comp_app, ← Set.image_image,
      Set.image_preimage_eq _ hg] at this

Goal state after:
case inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this✝ :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
inst : QuasiCompact (g ≫ f)
this : StableUnderSpecialization (⇑f '' Z) → (∃ R_1, Spec R = Spec R_1) → IsClosed (⇑f '' Z)
⊢ IsClosed (⇑f '' Z)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n : ℕ
e :
  ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → (((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂

Tactic:
use n

Goal state after:
case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n : ℕ
e :
  ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
⊢ ∀ (m : ℕ), n ≤ m → (((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent f

Tactic:
use n

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
e : I ≤ J
inst✝¹ : J.IsPrime
inst✝ : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
⊢ J ∈ I.minimalPrimes

Tactic:
convert! h₁

Goal state after:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
e : I ≤ J
inst✝¹ : J.IsPrime
inst✝ : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
⊢ J = p
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ ↑(⨆ I, ⨆ (_ : I ≠ ⊤), I.height)

Tactic:
· refine iSup_le fun p => WithBot.coe_le_coe.mpr (le_trans (b := p.last.asIdeal.height) ?_ ?_)
    · rw [height_eq_primeHeight]
      apply le_trans (b := ⨆ (_ : p.last ≤ p.last), ↑p.length)
      · exact le_iSup (fun _ => (↑p.length : ℕ∞)) le_rfl
      · exact le_iSup (fun p' => (⨆ _, p'.length : ℕ∞)) p
    · apply le_trans (b := ⨆ (_ : (p.last).asIdeal ≠ ⊤), p.last.asIdeal.height)
      · exact le_iSup_of_le p.last.isPrime.ne_top' le_rfl
      · exact le_iSup (fun I => ⨆ _, I.height) p.last.asIdeal

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

Goal state before:
pp: X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : ↑Γ(X, U)
hfg : (f |_ X.basicOpen s) ⋯ = (g |_ X.basicOpen s) ⋯
n : ℕ
hc : s ^ n * f = s ^ n * g
⊢ ∃ n, s ^ n * f = s ^ n * g

Tactic:
use n

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this✝ : ∃ x y, x ≠ y
this : NoZeroDivisors ↑(X.presheaf.obj (op U))
⊢ IsDomain ↑Γ(X, U)

Tactic:
exact NoZeroDivisors.to_isDomain _

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
⊢ x✝¹ ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier

Tactic:
have := 𝒰.exists_eq x; simp; grind

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ Hom.app (X.fromSpecStalk x) U =
    X.presheaf.germ U x hxU ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op

Tactic:
rw [← hV.fromSpecStalk_eq_fromSpecStalk hxV, IsAffineOpen.fromSpecStalk, Scheme.Hom.comp_app,
    hV.fromSpec_app_of_le _ hVU, ← X.presheaf.germ_res (homOfLE hVU) x hxV]

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ (X.presheaf.map (homOfLE hVU).op ≫ (ΓSpecIso Γ(X, V)).inv ≫ (Spec Γ(X, V)).presheaf.map (homOfLE ⋯).op) ≫
      Hom.app (Spec.map (X.presheaf.germ V x hxV)) (IsAffineOpen.fromSpec hV ⁻¹ᵁ U) =
    (X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.fst f g) (T.SpecTensorTo p) = T.x

Tactic:
simp only [SpecTensorTo]
  rw [← Scheme.Hom.comp_apply]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.snd f g) (T.SpecTensorTo p) = T.y

Tactic:
simp only [SpecTensorTo]
  rw [← Scheme.Hom.comp_apply]
  simp

Goal state after:
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.fst (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:
pullback.condition_assoc (f := I.glueDataObjι i)

Goal state after:
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.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (↑i).ι
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
⊢ Ideal.span {x | x ∈ s} = ⊤

Tactic:
Set.ofPred_mem_eq,

Goal state after:
case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
⊢ Ideal.span s = ⊤
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : f x = g y
e : P ≅ pullback f g := h.isoPullback
⊢ ∃ p, fst p = x ∧ snd p = y

Tactic:
obtain ⟨z, hzl, hzr⟩ := AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback x y hxy

Goal state after:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : f x = g y
e : P ≅ pullback f g := h.isoPullback
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ ∃ p, fst p = x ∧ snd p = y
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a
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).ι
x : ↥(U ⨿ V)
hx : x ∈ coprod.desc f g ⁻¹ᵁ W
⊢ x ∈ Scheme.Hom.opensRange i

Tactic:
obtain ⟨(x | x), rfl⟩ := (coprodMk U V).surjective x

Goal state after:
case a.inl
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).ι
x : ↥U
hx : (coprodMk U V) (Sum.inl x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ (coprodMk U V) (Sum.inl x) ∈ Scheme.Hom.opensRange i

case a.inr
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).ι
x : ↥V
hx : (coprodMk U V) (Sum.inr x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ (coprodMk U V) (Sum.inr x) ∈ Scheme.Hom.opensRange i
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
x : ↥X
hx : x ∈ ↑I.support
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ Set.range ⇑I.gluedTo

Tactic:
obtain ⟨y, rfl⟩ := (I.range_glueDataObjι_ι_eq_support_inter ⟨U, hU⟩).ge ⟨hx, hxU⟩

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj ⟨U, hU⟩)
hx : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑I.support
hxU : (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ ↑U
⊢ (I.glueDataObjι ⟨U, hU⟩ ≫ (↑⟨U, hU⟩).ι) y ∈ Set.range ⇑I.gluedTo
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ DenseRange ⇑(Hom.toImage f)

Tactic:
rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]

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
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
⊢ P ≤ @IsAffineHom

Tactic:
by
  intro X Y f hf
  wlog hY : IsAffine Y
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]
    intro U
    exact this P hA _ (IsZariskiLocalAtTarget.restrict hf _) U.2
  rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
  rw [HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)]
  exact hf.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
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝ : IsAffineHom f
this : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
⊢ f ⁻¹ᵁ W = Limits.coprod.inl ⁻¹ᵁ Limits.coprod.desc f g ⁻¹ᵁ W

Tactic:
by simp [← Scheme.Hom.comp_preimage]

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
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝ : IsAffineHom f
this : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
⊢ g ⁻¹ᵁ W = Limits.coprod.inr ⁻¹ᵁ Limits.coprod.desc f g ⁻¹ᵁ W

Tactic:
by simp [← Scheme.Hom.comp_preimage]

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

Goal state before:
pp: X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.comap (f ≫ g) = (I.comap g).comap f

Tactic:
by
  let e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
    asIso (pullback.map _ _ _ _ (𝟙 _) (I.comapIso g).hom (𝟙 _) (by simp) (by simp)) ≪≫
      pullbackRightPullbackFstIso _ _ _
  rw [comap, comap, ← Scheme.Hom.ker_comp_of_isIso e.hom]
  simp [e]

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

Goal state before:
pp: Z : Scheme
I : Z.IdealSheafData
⊢ Hom.ker (inv (pullback.snd (𝟙 Z) I.subschemeι) ≫ pullback.fst (𝟙 Z) I.subschemeι) = I

Tactic:
pullback_inv_snd_fst_of_left_isIso,

Goal state after:
Z : Scheme
I : Z.IdealSheafData
⊢ Hom.ker (I.subschemeι ≫ inv (𝟙 Z)) = I
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
hs : IsConstructible s
⊢ ∃ S x f, Set.range (comap f) = s

Tactic:
obtain ⟨s, rfl⟩ := exists_constructibleSetData_iff.mpr hs

Goal state after:
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
⊢ ∃ S x f, Set.range (comap f) = s.toSet
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))
⊢ Injective ⇑ψ

Tactic:
hψeq

Goal state after:
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))
⊢ Injective
    ⇑((↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
        ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
          ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
            ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
              ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField)))))
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
by
  wlog hY : ∃ R, Y = Spec R
  · refine .of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_
    have inst : LocallyOfFinitePresentation (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    have inst : QuasiCompact (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
    convert!
      (this (Y.affineCover.pullbackHom f i)
            (hs.preimage_of_isOpenEmbedding ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding)
            ⟨_, rfl⟩).preimage_of_isOpenEmbedding
        (Y.affineCover.f i).isoOpensRange.inv.isOpenEmbedding
    refine .trans ?_
      ((Scheme.homeoOfIso (Y.affineCover.f i).isoOpensRange).image_eq_preimage_symm _)
    apply Set.image_injective.mpr Subtype.val_injective
    rw [Set.image_preimage_eq_inter_range, ← Set.image_comp, ← Set.image_comp,
      Subtype.range_coe_subtype, Set.ofPred_mem_eq]
    change _ = (Y.affineCover.pullbackHom f i ≫
      (Y.affineCover.f i).isoOpensRange.hom ≫ Opens.ι _).base.hom '' _
    rw [Scheme.Hom.isoOpensRange_hom_ι, Cover.pullbackHom_map, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range]
    simp [IsOpenImmersion.range_pullbackFst, Set.image_inter_preimage]
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
    let 𝒰 := X.affineCover.finiteSubcover
    rw [← 𝒰.isOpenCover_opensRange.iUnion_inter s, Set.image_iUnion]
    refine .iUnion fun i ↦ ?_
    have inst : QuasiCompact (𝒰.f i ≫ f) :=
      HasAffineProperty.iff_of_isAffine.mpr (inferInstanceAs (CompactSpace (Spec _)))
    convert! this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩
    rw [Scheme.Hom.comp_base, ← TopCat.Hom.hom, ← TopCat.Hom.hom, TopCat.hom_comp,
      ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range, coe_opensRange]
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)] at hf
  exact (PrimeSpectrum.isConstructible_comap_image hf hs.isConstructible).isLocallyConstructible

Goal state after: