mathlib-initiative/mathlib-tactics huggingface dataset:
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 j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map ((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
        (D.U i).presheaf.map
            ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
          (D.U i).presheaf.map (eqToHom ⋯).op ≫
            (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
              (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
rw [← Functor.map_comp_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map
          (((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
            (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
        (D.U i).presheaf.map (eqToHom ⋯).op ≫
          (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
            (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
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 j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map
          (((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
            (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
        (D.U i).presheaf.map (eqToHom ⋯).op ≫
          (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
            (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
rw [← Functor.map_comp_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map
          ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
              (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
            (eqToHom ⋯).op) ≫
        (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPullback (Spec.map (pushout.inl f g)) (Spec.map (pushout.inr f g)) (Spec.map f) (Spec.map g)

Tactic:
apply isPullback_SpecMap_of_isPushout
  exact IsPushout.of_hasPushout f g

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝¹ : M.Over S
f : T ⟶ S
inst✝ : GrpObj (M.asOver S)
⊢ GrpObj ((pullback (M ↘ S) f).asOver T)

Tactic:
by
  unfold asOver OverClass.asOver at *; exact Over.grpObjMkPullbackSnd

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

Goal state before:
pp: case of_sSup_eq_top.a
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ P (f' ∣_ i₂ ⁻¹ᵁ U i)

Tactic:
refine H _ ((X'.isoOfEq ?_).hom ≫ i₁ ∣_ _) (i₂ ∣_ _) _ ?_

Goal state after:
case of_sSup_eq_top.a.refine_1
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ f' ⁻¹ᵁ i₂ ⁻¹ᵁ U i = i₁ ⁻¹ᵁ f ⁻¹ᵁ U i

case of_sSup_eq_top.a.refine_2
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ IsPullback (f' ∣_ i₂ ⁻¹ᵁ U i) ((X'.isoOfEq ?of_sSup_eq_top.a.refine_1).hom ≫ i₁ ∣_ f ⁻¹ᵁ U i) (i₂ ∣_ U i) (f ∣_ U i)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap S (S ⊗[R] T))

Tactic:
rw [locally_iff_span_eq_top, eq_top_iff, ← Ideal.map_top Algebra.TensorProduct.includeRight,
    ← hf.span_eq_top, Ideal.map_le_iff_le_comap, Ideal.span_le]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
⊢ {g | P ((algebraMap T (Localization.Away g)).comp (algebraMap R T))} ⊆
    ↑(Ideal.comap Algebra.TensorProduct.includeRight
        (Ideal.span {g | P ((algebraMap (S ⊗[R] T) (Localization.Away g)).comp (algebraMap S (S ⊗[R] T)))}))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: 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
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : Ideal ↑S) (x : p.IsPrime),
      P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)

Tactic:
trans ∀ (p : PrimeSpectrum S), P (Localization.localRingHom _ p.asIdeal φ.hom rfl)

Goal state after:
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
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (Spec.map φ) ↔
    ∀ (p : PrimeSpectrum ↑S),
      P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ) ⋯)

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
R S : CommRingCat
φ : R ⟶ S
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ (∀ (p : PrimeSpectrum ↑S),
      P
        (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom φ)
          ⋯)) ↔
    ∀ (p : Ideal ↑S) (x : p.IsPrime),
      P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
⊢ QuasiSeparatedSpace ↥X ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rw [← MorphismProperty.cancel_right_of_respectsIso @QuasiCompact _ (prodIsoPullback X X).hom,
    ← HasAffineProperty.iff_of_isAffine (f := terminal.from X) (P := @QuasiSeparated),
    quasiSeparated_iff]
  congr!
  ext : 1 <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := ⋯
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ringKrullDim R ≤ ↑(RelSeries.last l).asIdeal.height

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := ⋯
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ↑(RelSeries.last l).asIdeal.height ≤ ↑m.height

Tactic:
· rw [Ideal.height_eq_primeHeight]
    exact LTSeries.height_last_longestOf.symm.le

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := ⋯
m : Ideal R
hm : m.IsMaximal
hle : (RelSeries.last l).asIdeal ≤ m
⊢ ↑(RelSeries.last l).asIdeal.height ≤ ↑m.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ ↑(maximalIdeal R).primeHeight = ringKrullDim R

Tactic:
by
  simp [← Ideal.height_eq_primeHeight]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
P : Ideal S := Ideal.map (algebraMap R S) p
this✝ : P.IsPrime
this : IsLocalization.AtPrime (Localization.AtPrime (Ideal.map (algebraMap R S) p)) p
⊢ (Ideal.map (algebraMap R S) p).height = p.height

Tactic:
have := ringKrullDim_eq_of_ringEquiv (IsLocalization.algEquiv p.primeCompl
    (Localization.AtPrime P) (Localization.AtPrime p)).toRingEquiv

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
P : Ideal S := Ideal.map (algebraMap R S) p
this✝¹ : P.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime (Ideal.map (algebraMap R S) p)) p
this : ringKrullDim (Localization.AtPrime P) = ringKrullDim (Localization.AtPrime p)
⊢ (Ideal.map (algebraMap R S) p).height = p.height
Module: Mathlib.RingTheory.Ideal.Height

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

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
h : ¬I = ⊤
⊢ ↑(⨆ (_ : I ≠ ⊤), I.height) ≤ ringKrullDim R

Tactic:
· simp [h, ringKrullDim_nonneg_of_nontrivial]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
h : ¬I = ⊤
⊢ ↑(⨆ (_ : I ≠ ⊤), I.height) ≤ ringKrullDim R
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsReduced (𝒰.X i)
⊢ IsReduced X

Tactic:
have (x : X) : _root_.IsReduced (X.presheaf.stalk x) := by
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    exact isReduced_of_injective _
      (asIso <| (𝒰.f i).stalkMap x).commRingCatIsoToRingEquiv.injective

Goal state after:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsReduced (𝒰.X i)
this : ∀ (x : ↥X), _root_.IsReduced ↑(X.presheaf.stalk x)
⊢ IsReduced X
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
s : Set X.IdealSheafData
⊢ ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (sSup (ideal '' s) U) =
      sSup (ideal '' s) (X.affineBasicOpen f)

Tactic:
have : sSup (ideal '' s) = ⨆ i : s, ideal i.1 := by
        conv_lhs => rw [← Subtype.range_val (s := s), ← Set.range_comp]
        rfl
      simp only [this, iSup_apply, Ideal.map_iSup, map_ideal_basicOpen, implies_true]

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
⊢ P (f ≫ i)

Tactic:
wlog hZ : IsAffine Z generalizing X Y Z
    · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
      intro U
      rw [morphismRestrict_comp]
      exact this _ inferInstance _ (IsZariskiLocalAtTarget.restrict hf _) U.2
    let e : Y ≅ i.opensRange.toScheme := IsOpenImmersion.isoOfRangeEq i i.opensRange.ι (by simp)
    rw [show f ≫ i = f ≫ e.hom ≫ i.opensRange.ι by simp [e], ← Category.assoc]
    exact respects_isOpenImmersion_aux hQ _ (by rwa [P.cancel_right_of_respectsIso])

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : ↑X.affineOpens
this : PrimeSpectrum.zeroLocus ↑(I.ideal U) = ∅
⊢ ⊤.ideal U ≤ I.ideal U

Tactic:
simp [PrimeSpectrum.zeroLocus_empty_iff_eq_top.mp this]

Goal state after:
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) ≫
          (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom)) =
    RingHom.ker (CommRingCat.Hom.hom ((↑U).topIso.hom ≫ φ))

Tactic:
congr 2

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))
⊢ Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫ (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom =
    (↑U).topIso.hom ≫ φ
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ ((CommRingCat.Hom.hom (f.app ↑U)) x |_ f ⁻¹ᵁ Y.basicOpen s) ⋯ = 0

Tactic:
replace hx : (Y.presheaf.map (homOfLE (Y.basicOpen_le s)).op ≫ f.app _).hom x = 0 := by
      trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)
      · simp [-NatTrans.naturality, RingHom.algebraMap_toAlgebra]
      · simp only [Scheme.affineBasicOpen_coe, RingHom.mem_ker] at hx
        rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]

Goal state after:
case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx : (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x = 0
⊢ ((CommRingCat.Hom.hom (f.app ↑U)) x |_ f ⁻¹ᵁ Y.basicOpen s) ⋯ = 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
H : ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
⊢ ↑((I.glueDataObjι ia) a) ∈ X.basicOpen g

Tactic:
← hfg

Goal state after:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
H : ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
⊢ ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U) = ⇑I.gluedTo ⁻¹' ↑↑U

Tactic:
apply I.gluedTo_injective.image_injective

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑I.gluedTo '' Set.range ⇑(I.glueData.ι U) = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U' ≤ U, f ⁻¹ᵁ U' = V

Tactic:
obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
U' : Set ↥Y
hU' : IsOpen U'
e : ⇑f ⁻¹' U' = V.carrier
⊢ ∃ U' ≤ U, f ⁻¹ᵁ U' = V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: 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

Tactic:
rw [← cancel_mono f.imageι]

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) ≫
      imageι f =
    (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) ≫
      imageι f
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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))) ↔ Q (CommRingCat.Hom.hom f)

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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ IsAffine (Spec S)

Tactic:
exacts [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty Q)
    (arrowIsoΓSpecOfIsAffine f).symm, inferInstance]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
this : IsIso (Scheme.Hom.imageι f)
⊢ IsIso f

Tactic:
exact f.toImage_imageι ▸ inferInstance

Goal state after:
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)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ x ∈
    Set.range
      ⇑(pullback.map ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) f f
          ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)

Tactic:
range_map

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)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ x ∈
    ⇑(pullback.fst f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ∩
      ⇑(pullback.snd f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
x✝ : PUnit.{0}
⊢ IsClosedImmersion (pullback.diagonal f ∣_ ⊤)

Tactic:
← diagonalCoverDiagonalRange_eq_top_of_injective f 𝒰 𝒱 hf

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
x✝ : PUnit.{0}
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
inst✝ : Algebra.FinitePresentation R S
f : S
⊢ IsOpen (comap (algebraMap R S) '' ↑(basicOpen f))

Tactic:
exact isOpen_of_stableUnderGeneralization_of_isConstructible
    ((basicOpen f).2.stableUnderGeneralization.image
      (Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp ‹_›))
    (isConstructible_comap_image (RingHom.finitePresentation_algebraMap.mpr ‹_›)
      isConstructible_basicOpen)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case mp
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
⊢ False

Tactic:
let F : (A ⧸ Ideal.span s) ⊗[R] (q.asIdeal.comap (algebraMap R A)).ResidueField →ₐ[A]
        q.asIdeal.ResidueField :=
      Algebra.TensorProduct.lift
        (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A _) hs)
        (Ideal.ResidueField.mapₐ _ _ (Algebra.ofId _ _) rfl)
        fun _ _ ↦ .all _ _

Goal state after:
case mp
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal (Algebra.ofId R A) ⋯) ⋯
⊢ False