mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (pullback.snd f g)

Tactic:
have := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.isEmbedding g.base H

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : IsIso (pullback.snd f.base g.base)
⊢ IsIso (pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ X.presheaf.map (homOfLE ⋯).op = (appIso (X.homOfLE h) W).inv

Tactic:
← Iso.hom_comp_eq_id

Goal state after:
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ (appIso (X.homOfLE h) W).hom ≫ X.presheaf.map (homOfLE ⋯).op =
    𝟙 (X.presheaf.obj (op (⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))))))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U ≤ V
⊢ f ∣_ U ≫ Y.homOfLE e = X.homOfLE ⋯ ≫ f ∣_ V

Tactic:
by
  simp [← cancel_mono V.ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).toSpecΓ ≫ Spec.map (Hom.app f U) = f ∣_ U ≫ U.toSpecΓ

Tactic:
by
  simp only [toSpecΓ, topIso, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv,
    eqToHom_op, Hom.app_eq_appLE, Category.assoc, ← Spec.map_comp, Hom.appLE_map,
    toSpecΓ_naturality_assoc, TopologicalSpace.Opens.map_top, morphismRestrict_appLE, Hom.map_appLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, zeroLocus {i}

Tactic:
rw [← PrimeSpectrum.zeroLocus_iUnion₂]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus (⋃ i ∈ s, {i})
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, h₁, h₂ : _ ≤ U.ι ⁻¹ᵁ V⟩ :=
    (isBasis_basicOpen U).exists_subset_of_mem_open (x.2 : (⟨x, h⟩ : U) ∈ _) (U.ι ⁻¹ᵁ V).isOpen

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)

Tactic:
exact IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (D.f' j k)

Tactic:
simp only [hjk, GlueData'.f', ↓reduceDIte]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (eqToHom ⋯)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
by
      apply +allowSynthFailures pullback_snd_iso_of_left_iso
      simp only [hjk, GlueData'.f', ↓reduceDIte]
      infer_instance

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ InvImage D.Rel (⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) ((sigmaIsoSigma D.U).inv.hom' ⟨i, x⟩)
    ((sigmaIsoSigma D.U).inv.hom' ⟨j, y⟩)

Tactic:
rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ Relation.EqvGen (InvImage D.Rel ⇑(ConcreteCategory.hom (sigmaIsoSigma D.U).hom)) ((sigmaIsoSigma D.U).inv.hom' ⟨i, x⟩)
    ((sigmaIsoSigma D.U).inv.hom' ⟨j, y⟩)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R : CommRingCat
x : PrimeSpectrum ↑R
⊢ (Spec R).presheaf.germ ⊤ x trivial ≫ (stalkIso R x).hom =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal))

Tactic:
by
  simp [← Iso.inv_comp_eq, ← Spec.algebraMap_stalkIso_inv_assoc]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_1
D : GlueData
h : MkCore
i j k : h.J
⊢ { p // (ConcreteCategory.hom (h.V i j).inclusion') p.1 = (ConcreteCategory.hom (h.V i k).inclusion') p.2 } →
    { p // (ConcreteCategory.hom (h.V j k).inclusion') p.1 = (ConcreteCategory.hom (h.V j i).inclusion') p.2 }

pp: case refine_2
D : GlueData
h : MkCore
i j k : h.J
⊢ Continuous ?refine_1

Tactic:
· intro x
    refine ⟨⟨⟨(h.t i j x.1.1).1, ?_⟩, h.t i j x.1.1⟩, rfl⟩
    rcases x with ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩
    exact h.t_inter _ ⟨x, hx⟩ hx'

Goal state after:
case refine_2
D : GlueData
h : MkCore
i j k : h.J
⊢ Continuous fun x ↦ ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯).op ≫
        (D.V (k, i)).presheaf.map ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map (eqToHom ⋯)) ≫
          (D.V (k, i)).presheaf.map
            ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map
              ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op)

Tactic:
simp_rw [← (𝖣.V (k, i)).presheaf.map_comp]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯) ≫
      pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    𝟙 (pullback (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)

Tactic:
· simp_rw [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
⊢ (ConcreteCategory.hom (D.ι i).base) x = (ConcreteCategory.hom (D.ι i).base) y

Tactic:
exact h2.symm

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
⊢ (of P).toProperty.RespectsIso

Tactic:
apply respectsIso_mk
  · intro _ _ _ _ _ _; apply MorphismProperty.RespectsIso.precomp
  · intro _ _ _ _ _ _; apply MorphismProperty.RespectsIso.postcomp

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion g
H : Dense (⇑g '' Set.range ⇑f)
⊢ Set.range ⇑f = ⇑g ⁻¹' ⇑g '' Set.range ⇑f

Tactic:
rw [Set.preimage_image_eq _ g.isOpenEmbedding.injective]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case zero
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
h : x ^ 0 * y ∈ J
⊢ y ∈ J

Tactic:
simpa using h

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x ^ (n + 1) * y ∈ J
⊢ y ∈ J

Tactic:
rw [add_comm, pow_add, pow_one, mul_assoc] at h
    exact ih <| hxJ _ h

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

Goal state before:
pp: case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ ↑U ⋯))

Tactic:
← Scheme.Hom.appLE_comp_appLE _ _ ⊤ (e.hom ''ᵁ U) U.1 le_top (e.hom.preimage_image_eq _).ge,

Goal state after:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (e.hom ''ᵁ ↑U) ⋯ ≫ Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)
x : ↥X
hy : x ∈ iSup U
i : ι
hi : x ∈ U i
⊢ P ((CommRingCat.Hom.hom (Scheme.Hom.stalkMap (U i).ι ⟨x, hi⟩)).comp (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))

Tactic:
simpa [Scheme.Hom.stalkMap_comp] using hf i ⟨x, hi⟩

Goal state after:
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
H : P f
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
by
  rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H
  exact H _ _ _

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → ↑m.height ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
⊢ ↑p.height ≤ n

Tactic:
refine le_trans ?_ (h hm)

Goal state after:
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → ↑m.height ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
⊢ ↑p.height ≤ ↑m.height
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
← Set.range_comp

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

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

Tactic:
simpa using h

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

Goal state before:
pp: case hf
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(X, ⊤) ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)) =
    algebraMap ↑Γ(X, ⊤) ↑Γ(X, X.basicOpen f)

Tactic:
· simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, RingHom.algebraMap_toAlgebra,
      ← Functor.map_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
y : ↥(Spec R)
hsub : f y ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑⊤
⊢ ringKrullDim ↑(X.presheaf.stalk (f y)) = ringKrullDim ↑((Spec R).presheaf.stalk y)

Tactic:
exact Order.krullDim_eq_of_orderIso
      (PrimeSpectrum.comapEquiv (asIso (Scheme.Hom.stalkMap f y)).commRingCatIsoToRingEquiv)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
x : ↥X
h : ∃ R, X = Spec R
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)

Tactic:
obtain ⟨R, rfl⟩ := h

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ ringKrullDim ↑((Spec R).presheaf.stalk x) = ↑(coheight x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

Tactic:
IsAffineOpen.fromSpec_image_zeroLocus

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x✝ : ↑Γ(X, ↑U)
hx : x✝ ∈ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
hxZ : (IsAffineOpen.fromSpec ⋯) x ∈ Z
⊢ (Spec.map (X.presheaf.map (homOfLE ⋯).op)) x ∈ ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z

Tactic:
Set.mem_preimage,

Goal state after:
case a
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x✝ : ↑Γ(X, ↑U)
hx : x✝ ∈ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
hxZ : (IsAffineOpen.fromSpec ⋯) x ∈ Z
⊢ (IsAffineOpen.fromSpec ⋯) ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x) ∈ ↑Z
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Tactic:
by
  obtain ⟨U', h₁, h₂, h₃ : U' ≤ U ⊓ V⟩ :=
    Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens (show x ∈ U ⊓ V from ⟨hxU, hxV⟩)
  transitivity fromSpecStalk h₁ h₂
  · delta fromSpecStalk
    rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
  · delta fromSpecStalk
    rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]

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

Goal state before:
pp: case a
X : Scheme
I✝ : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
hx : x ∈ PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' Z')
I : Ideal ↑Γ(X, ↑U)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')

Tactic:
rw [← vanishingIdeal_closure,
          ← this.isOpenMap.preimage_closure_eq_closure_preimage this.continuous, e] at hx

Goal state after:
case a
X : Scheme
I✝ : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
I : Ideal ↑Γ(X, ↑U)
hx : x ∈ PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' PrimeSpectrum.zeroLocus ↑I)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
I : X.IdealSheafData
⊢ ⊤ ≤ I.support ↔ I = ⊥

Tactic:
le_support_iff_le_vanishingIdeal,

Goal state after:
X : Scheme
inst✝ : IsReduced X
I : X.IdealSheafData
⊢ I ≤ vanishingIdeal ⊤ ↔ I = ⊥
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (X.presheaf.germ V x hxV) ≫ Spec.map (Hom.appLE f U V ⋯) ≫ IsAffineOpen.fromSpec hU =
    Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f

Tactic:
IsAffineOpen.SpecMap_appLE_fromSpec

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec ?hV ≫ f =
    Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f

case hV
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ IsAffineOpen V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U

Tactic:
refine pullback.lift ((F ≫ X.homOfLE inf_le_right ≫
    V.2.isoSpec.hom).liftQuotient _ ?_) (F ≫ X.homOfLE (by simp)) ?_

Goal state after:
case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ I.ideal V ≤
    RingHom.ker
      (CommRingCat.Hom.hom ((ΓSpecIso Γ(X, ↑V)).inv ≫ Hom.appTop (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)))

case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ?refine_1 ≫ I.glueDataObjι V =
    (F ≫ X.homOfLE ⋯) ≫ X.homOfLE ⋯
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 ↦ ?_)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑U))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U
⊢ (CommRingCat.Hom.hom (f.app ↑U)) s = 0

Tactic:
apply X.IsSheaf.section_ext

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U
⊢ ∀ x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U)),
    ∃ V,
      ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
        x ∈ V ∧
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
            (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo) ≫ pullback.fst f g =
    Spec.map (Hom.residueFieldMap (pullback.fst f g) t) ≫ X.fromSpecResidueField ((pullback.fst f g) t)

Tactic:
simp only [Category.assoc, Triplet.specTensorTo_fst]

Goal state after:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInl ≫ X.fromSpecResidueField (Triplet.ofPoint t).x =
    Spec.map (Hom.residueFieldMap (pullback.fst f g) t) ≫ X.fromSpecResidueField ((pullback.fst f g) t)
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)
this : QuasiSeparatedSpace ↥X
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ ∀ i ∈ s', IsCompact ↑(X.basicOpen i)

Tactic:
exact fun i hi ↦ (hs₂ _ (hs' hi)).isCompact

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ (pullback.fst f g) a ∈ ⇑f ⁻¹' Set.range ⇑g

Tactic:
simp only [Set.mem_preimage, Set.mem_range, ← Scheme.Hom.comp_apply, pullback.condition]

Goal state after:
case refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ ∃ y, g y = (pullback.snd f g ≫ g) a
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

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

Tactic:
apply isAffine_of_isAffineOpen_basicOpen (U.topIso.inv '' s)
  · rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]
  · rintro _ ⟨j, hj, rfl⟩
    rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]
    simpa [Scheme.Opens.toScheme_presheaf_obj] using hs₂ j hj

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi
    ((CategoryTheory.forget TopCat).map (pullbackComparison forgetToTop f g) ≫
      pullbackComparison (CategoryTheory.forget TopCat) (forgetToTop.map f) (forgetToTop.map g))

Tactic:
← _root_.CategoryTheory.Limits.pullbackComparison_comp,

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (pullbackComparison (forgetToTop ⋙ CategoryTheory.forget TopCat) f g)