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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource P

Tactic:
refine .mk_of_small (fun {X Y f} 𝒰 hf ↦ ?_) (fun {X Y f} 𝒰 hf ↦ ?_)

Goal state after:
case refine_1
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)

case refine_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀) (i_1 : ↑Y.affineOpens), Q (𝒰.f i ∣_ f ⁻¹ᵁ ↑i_1 ≫ f ∣_ ↑i_1)
U : ↑Y.affineOpens
⊢ Q (f ∣_ ↑U)

Tactic:
H (f ∣_ U.1) (Scheme.OpenCover.restrict 𝒰 _)

Goal state after:
case refine_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀) (i_1 : ↑Y.affineOpens), Q (𝒰.f i ∣_ f ⁻¹ᵁ ↑i_1 ≫ f ∣_ ↑i_1)
U : ↑Y.affineOpens
⊢ ∀ (i : (Scheme.OpenCover.restrict 𝒰 (f ⁻¹ᵁ ↑U)).I₀), Q ((Scheme.OpenCover.restrict 𝒰 (f ⁻¹ᵁ ↑U)).f i ≫ f ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: ⊢ (topologically @SpecializingMap).RespectsIso

Tactic:
apply topologically_respectsIso

Goal state after:
case hP₁
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), SpecializingMap ⇑f

case hP₂
⊢ ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
    (f : α → β) (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
intro R S _ _ f s hsone hs

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P)
      ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case convert_6
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
⊢ Q
    (((pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫
        pullback.map (pullback.diagonal f)
          (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
            ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
          (pullback.diagonal f)
          (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))
              (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) ((𝒰' i).f j) ((𝒰' i).f k) (𝟙 (𝒰.X i)) ⋯ ⋯ ≫
            pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
              (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
          (𝟙 X) (𝟙 (pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))))
          (𝟙 (pullback.diagonalObj f)) ⋯ ⋯) ≫
      pullback.snd (pullback.diagonal f)
        (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))
            (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) ((𝒰' i).f j) ((𝒰' i).f k) (𝟙 (𝒰.X i)) ⋯ ⋯ ≫
          pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
            (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯))

Tactic:
· simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
      Category.comp_id]
    convert! h𝒰' i j k
    ext1 <;> simp [Scheme.Cover.pullbackHom]

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

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g f
i : (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰).I₀
⊢ P (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ pullback.fst g f)

Tactic:
rw [← pullbackLeftPullbackSndIso_hom_fst, P.cancel_left_of_respectsIso]

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g f
i : (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰).I₀
⊢ P (pullback.fst g (𝒰.f i ≫ f))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : SurjectiveOnStalks (f ≫ g)
⊢ SurjectiveOnStalks f

Tactic:
by
  refine ⟨fun x ↦ ?_⟩
  have := (f ≫ g).stalkMap_surjective x
  rw [Scheme.Hom.stalkMap_comp] at this
  exact Function.Surjective.of_comp this

Goal state after:
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 V : ↑X.affineOpens
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ Set.range ⇑(↑V).ι)
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
Scheme.Opens.range_ι

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
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
e : ↥(pullback (↑U).ι (↑V).ι) ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
⊢ X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r

Tactic:
hBss',

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
⊢ X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal R
⊢ (comap e.symm I).height = I.height

Tactic:
height_comap

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal R
⊢ I.height = I.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case refine_1
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), ↑(Order.height i) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ ↑p.height ≤ n

pp: case refine_2
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n
p : PrimeSpectrum R
⊢ ↑(Order.height p) ≤ n

Tactic:
· rw [Ideal.height_eq_primeHeight]
    exact h ⟨p, hp⟩

Goal state after:
case refine_2
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n
p : PrimeSpectrum R
⊢ ↑(Order.height p) ≤ n
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
⊢ IsReduced (Spec R)

Tactic:
apply +allowSynthFailures isReduced_of_isReduced_stalk
  intro x
  have : _root_.IsReduced (CommRingCat.of <| Localization.AtPrime (PrimeSpectrum.asIdeal x)) := by
    dsimp; infer_instance
  exact isReduced_of_injective (Spec.stalkIso R x).hom.hom
    (Spec.stalkIso R x).commRingCatIsoToRingEquiv.injective

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

Goal state before:
pp: X : Scheme
s : Set X.IdealSheafData
| sSup (ideal '' s)

Tactic:
← Subtype.range_val (s := s),

Goal state after:
X : Scheme
s : Set X.IdealSheafData
| sSup (ideal '' Set.range Subtype.val)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
inst✝ : IsReduced X
this :
  ∀ (X : Scheme) (x : ↥X),
    closure {x} ∈ irreducibleComponents ↥X → ∀ [IsReduced X], (∃ R, X = Spec R) → IsField ↑(X.presheaf.stalk x)
hX : ¬∃ R, X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx : closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥X
inst : IsReduced (X.affineCover.X i)
⊢ closure {x} ∈ irreducibleComponents ↥(X.affineCover.X i)

Tactic:
(X.affineCover.f i).isOpenEmbedding.closure_eq_preimage_closure_image,

Goal state after:
case inr
X : Scheme
inst✝ : IsReduced X
this :
  ∀ (X : Scheme) (x : ↥X),
    closure {x} ∈ irreducibleComponents ↥X → ∀ [IsReduced X], (∃ R, X = Spec R) → IsField ↑(X.presheaf.stalk x)
hX : ¬∃ R, X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx : closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥X
inst : IsReduced (X.affineCover.X i)
⊢ ⇑(X.affineCover.f i) ⁻¹' closure (⇑(X.affineCover.f i) '' {x}) ∈ irreducibleComponents ↥(X.affineCover.X i)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * (x - y) = 0

Tactic:
generalize x - y = z

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0 → ∃ c, ↑c * z = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ x.asIdeal.height = coheight x

Tactic:
PrimeSpectrum.height_eq_orderHeight,

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ height x = coheight x
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsOpenImmersion f ∧ Surjective f

Tactic:
by
  rw [surjective_iff, ← TopCat.epi_iff_surjective, isIso_iff_isOpenImmersion_and_epi_base]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ vanishingIdeal I.support = I.radical

Tactic:
by
  ext U : 2
  dsimp
  rw [← vanishingIdeal_zeroLocus_eq_radical]
  congr 1
  apply U.2.fromSpec.isOpenEmbedding.injective.image_injective
  rw [Set.image_preimage_eq_inter_range, IsAffineOpen.range_fromSpec,
    IsAffineOpen.fromSpec_image_zeroLocus, coe_support_inter]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ (Hom.stalkMap g (f (closedPoint ↑R)) ≫ Hom.stalkMap f (closedPoint ↑R)) ≫ (stalkClosedPointIso R).hom =
    Hom.stalkMap g (f (closedPoint ↑R)) ≫ stalkClosedPointTo f

Tactic:
exact Category.assoc _ _ _

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ Hom.ker f = ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))

Tactic:
refine (le_of_isAffine ((f.ideal_ker_le _).trans (by simp))).antisymm
    (le_ofIdeals_iff.mpr fun U ↦ ?_)
  simp only [ofIdealTop_ideal, homOfLE_leOfHom, Ideal.map_le_iff_le_comap, RingHom.comap_ker,
    ← CommRingCat.hom_comp, f.naturality]
  intro x
  simp +contextual

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
e : f x = g y
z : ↥(pullback f g)
⊢ Nonempty ↥(pullback f g)

Tactic:
exact ⟨z⟩

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q],
  Q.IsLocal :=
  HasAffineProperty.isLocal_affineProperty
⊢ ∀ ⦃X Y S : Scheme⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), IsAffine Y → IsAffine (pullback f g)

Tactic:
introv X hX H

Goal state after:
X✝¹ Y✝ Z : Scheme
f✝ : X✝¹ ⟶ Y✝
g✝ : Y✝ ⟶ Z
this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q],
  Q.IsLocal :=
  HasAffineProperty.isLocal_affineProperty
X✝ Y S : Scheme
X : IsAffine S
hX : IsAffine X✝
f : X✝ ⟶ S
g : Y ⟶ S
H : IsAffine Y
⊢ IsAffine (pullback f g)
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
hPi : 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
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
⊢ IsLocalization.Away ((CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ↑a)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))

Tactic:
exact (isAffineOpen_top X).isLocalization_basicOpen (f.appTop a.val)

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ IsPreimmersion I.gluedTo

Tactic:
IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsPreimmersion)
    _ (iSup_affineOpens_eq_top X)

Goal state after:
X : Scheme
I : X.IdealSheafData
⊢ ∀ (i : ↑X.affineOpens), IsPreimmersion (I.gluedTo ∣_ ↑i)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ Hom.ker ⊤.subschemeι = ⊤

Tactic:
ker_subschemeι

Goal state after:
X : Scheme
I : X.IdealSheafData
⊢ ⊤ = ⊤
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: Z : Scheme
I : Z.IdealSheafData
⊢ Hom.ker I.subschemeι = I

Tactic:
ker_subschemeι

Goal state after:
Z : Scheme
I : Z.IdealSheafData
⊢ I = I
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
⊢ (pullback.fst f f ≫ f) x = (pullback.snd f f ≫ f) x

Tactic:
pullback.condition

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
⊢ (pullback.snd f f ≫ f) x = (pullback.snd f f ≫ f) x
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Dense (Set.range ⇑(Scheme.Hom.coborderRange f).ι)

Tactic:
Scheme.Opens.range_ι

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Dense ↑(Scheme.Hom.coborderRange f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ Subtype.val ⁻¹' ⇑f '' s =
    ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
      ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
apply Set.image_injective.mpr Subtype.val_injective

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ Subtype.val '' Subtype.val ⁻¹' ⇑f '' s =
    Subtype.val ''
      ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
        ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
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
⊢ IsSchemeTheoreticallyDominant (pullback.snd f g)

Tactic:
by
  rw [isSchemeTheoreticallyDominant_iff]
  let h𝒰 := Y.isBasis_affineOpens.isOpenCover_mem_and_le
    (S.isBasis_affineOpens.isOpenCover.comap g.base.hom)
  refine Scheme.IdealSheafData.ext_of_iSup_eq_top (fun U ↦ ⟨_, by exact U.2.1⟩) h𝒰 ?_
  rintro ⟨⟨V, ⟨U, hU⟩⟩, hV, hVU : V ≤ g ⁻¹ᵁ U⟩
  simp only [Scheme.Hom.ker_apply, Scheme.IdealSheafData.ideal_bot, Pi.bot_apply, ← le_bot_iff]
  intro x hx
  have := mono_pushoutSection_of_isCompact_of_flat_right
    (.of_hasPullback f g) (UY := pullback.snd f g ⁻¹ᵁ V) hVU le_rfl (by
      grw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage, right_eq_inf,
        hVU]) hU hV (f.isCompact_preimage hU.isCompact)
  rw [@ConcreteCategory.mono_iff_injective_of_preservesPullback] at this
  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) ?_
  apply this
  simpa [← CommRingCat.comp_apply, ← Scheme.Hom.app_eq_appLE] using hx

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

Goal state before:
pp: case convert_7
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.FinitePresentation ↑R ↑S

Tactic:
apply (HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)).mp inferInstance

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

Goal state before:
pp: X S : Scheme
f : X ⟶ S
⊢ GeometricallyIntegral f ↔ ∀ (s : ↥S), GeometricallyIntegral (Scheme.Hom.fiberToSpecResidueField f s)

Tactic:
simp only [GeometricallyIntegral.eq_geometrically,
    ← geometrically_iff_forall_fiberToSpecResidueField]

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

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

Tactic:
rw [universallyClosed_eq]
  intro X' Y' i₁ i₂ f' hf
  have hf' : IsClosedImmersion f' :=
    MorphismProperty.of_isPullback hf.flip inferInstance
  exact f'.isClosedEmbedding.isClosedMap

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
⊢ CompactSpace ↥X

Tactic:
let Ti (i : 𝒰.I₀) : T.Opens := basicOpen (MvPolynomial.X i)

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
⊢ CompactSpace ↥X