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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coequalizerCoforkIsColimit _ _)

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ IsColimit
    (forgetToSheafedSpace.mapCocone
      (coequalizerCofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).base = (D.ι i).base

Tactic:
rw [D.ι_isoLocallyRingedSpace_inv i]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ (gluedCover 𝒰).Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
use e.hom ⟨⟨x, y⟩, h⟩

Goal state after:
case h
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt := ⋯
⊢ ((gluedCover 𝒰).f ⟨i, x⟩.fst ⟨j, y⟩.fst) ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) = ⟨i, x⟩.snd ∧
    ((gluedCover 𝒰).t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ (gluedCover 𝒰).f ⟨j, y⟩.fst ⟨i, x⟩.fst)
        ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) =
      ⟨j, y⟩.snd
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
⊢ (gluing 𝒰 f g).glued ⟶ X

Tactic:
apply Multicoequalizer.desc (gluing 𝒰 f g).diagram _ fun i ↦ pullback.fst _ _ ≫ 𝒰.f i

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ ∀ (a : (MultispanShape.prod (gluing 𝒰 f g).J).L),
    (gluing 𝒰 f g).diagram.fst a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) =
      (gluing 𝒰 f g).diagram.snd a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Function.Injective (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

Tactic:
rintro ⟨ix, x⟩ ⟨iy, y⟩ e
      have : α ix x = α iy y := by
        simpa [← Scheme.Hom.comp_apply] using e
      obtain rfl : ix = iy := by
        by_contra h
        exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl
      rw [(α ix).isOpenEmbedding.injective this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))

Tactic:
apply isOpenImmersion_sigmaDesc_aux

Goal state after:
σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α (e.symm x)))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
⊢ ∀ (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

Tactic:
αX

Goal state after:
case refine_1
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
⊢ ∀ (αY : Y' ⟶ Y) (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))
⊢ (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) x) =
    (PrimeSpectrum.primeSpectrumProd R S).symm x

Tactic:
apply PrimeSpectrum.ext
  obtain (x | x) := x <;>
    simp only [coprodMk_inl, coprodMk_inr, ← Scheme.Hom.comp_apply,
      coprodSpec, coprod.inl_desc, coprod.inr_desc]
  · change Ideal.comap _ _ = x.asIdeal.prod ⊤
    ext; simp [Ideal.prod, CommRingCat.ofHom]
  · change Ideal.comap _ _ = Ideal.prod ⊤ x.asIdeal
    ext; simp [Ideal.prod, CommRingCat.ofHom]

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

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.snd (D.f j i) (D.f j k)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
      (pullbackSymmetry (D.f j k) (D.f j i)).hom.c.app
          (op
            ((Opens.map (pullback.snd (D.f j i) (D.f j k)).base).obj
              ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
                ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U)))) ≫
        ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                (pullback (D.f j k) (D.f j i)).presheaf).map
            (eqToHom ⋯) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
rw [← PresheafedSpace.comp_c_app_assoc, congr_app (pullbackSymmetry_hom_comp_snd _ _)]

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    ((pullback.fst (D.f j k) (D.f j i)).c.app
          (op
            ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
              ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
              (pullback (D.f j k) (D.f j i)).presheaf).map
          (eqToHom ⋯) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f j k) (D.f j i))
              ((Opens.map (D.t' j k i).base).1
                ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)
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
⊢ IsZariskiLocalAtTarget P

Tactic:
apply IsZariskiLocalAtTarget.mk'

Goal state after:
case restrict
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)

case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
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
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.snd ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
        ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.fst ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
        ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)

Tactic:
rw [← cancel_mono ((𝒱 i).f _)]

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
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        pullback.snd ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
          ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)) ≫
      (𝒱 i).f ⟨i, (j, j)⟩.snd.2 =
    (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        pullback.fst ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
          ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)) ≫
      (𝒱 i).f ⟨i, (j, j)⟩.snd.2
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
⊢ IsZariskiLocalAtTarget P.universally

Tactic:
apply IsZariskiLocalAtTarget.mk'

Goal state after:
case restrict
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) (U : Y.Opens), P.universally f → P.universally (f ∣_ U)

case of_sSup_eq_top
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),
    iSup U = ⊤ → (∀ (i : ι), P.universally (f ∣_ U i)) → P.universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) g
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ≫ g)

Tactic:
simp only [topologically, Scheme.Hom.comp_base, TopCat.coe_comp]

Goal state after:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) g
⊢ P (⇑g ∘ ⇑f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
apply IsZariskiLocalAtTarget.mk'

Goal state after:
case restrict
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
      topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)

case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
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
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (e x) ≫ Scheme.Hom.stalkMap e x))

Tactic:
exact (RingHom.RespectsIso.cancel_right_isIso hP _ _).mpr <| hf (e x)

Goal state after:
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
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
⊢ IsZariskiLocalAtTarget (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P)

Tactic:
apply IsZariskiLocalAtTarget.mk'

Goal state after:
case restrict
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
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f → stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U)

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
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsQuasiSeparated ↑U
⊢ IsQuasiSeparated ↑(f ⁻¹ᵁ U)

Tactic:
by
  have : QuasiSeparatedSpace U := (isQuasiSeparated_iff_quasiSeparatedSpace _ U.2).mp hU
  exact (isQuasiSeparated_iff_quasiSeparatedSpace _ (f ⁻¹ᵁ U).2).mpr
    (quasiSeparatedSpace_of_quasiSeparated (f ∣_ U))

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ (comap (algebraMap R A) J).primeHeight = J.primeHeight

Tactic:
simpa [Ideal.height_eq_primeHeight] using IsLocalization.height_under_eq_of_isPrime S J

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this✝ : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec S), (∃ R, X = Spec R) → (P f ↔ Q f)
hX : ¬∃ R, X = Spec R
⊢ P f ↔ Q f

pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S : CommRingCat
X : Scheme
f : X ⟶ Spec S
hX : ∃ R, X = Spec R
⊢ P f ↔ Q f

Tactic:
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover,
        IsZariskiLocalAtSource.iff_of_openCover (P := Q) X.affineCover]
      refine forall_congr' fun _ ↦ this _ ⟨_, rfl⟩

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S : CommRingCat
X : Scheme
f : X ⟶ Spec S
hX : ∃ R, X = Spec R
⊢ P f ↔ Q f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f✝ ∧
      affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q') f✝ ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] f ↦ Q f ∧ Q' f) f✝

Tactic:
simp_rw [affineLocally_iff_affineOpens_le]

Goal state after:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ ((∀ (U : ↑Y✝.affineOpens) (V : ↑X✝.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))) ∧
      ∀ (U : ↑Y✝.affineOpens) (V : ↑X✝.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
        Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))) ↔
    ∀ (U : ↑Y✝.affineOpens) (V : ↑X✝.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e)) ∧
        Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ (RelSeries.last p).asIdeal.height ≤ ⨆ I, ⨆ (_ : I ≠ ⊤), I.height

Tactic:
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.RingTheory.Ideal.Height

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height

Tactic:
· obtain ⟨P, hP⟩ := Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)
      refine ⟨P, iSup_pos (α := ℕ∞) I_top ▸ le_iSup_of_le (hP.left.left) ?_⟩
      have := hP.isPrime
      exact iInf_le_of_le P (iInf_le_of_le hP (ge_of_eq (Ideal.height_eq_primeHeight P)))

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (x : I.IsMaximal), I.primeHeight) = ringKrullDim R

Tactic:
simp_rw [← Ideal.height_eq_primeHeight, Ideal.sup_isMaximal_height_eq_ringKrullDim]

Goal state after: