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

Goal state before:
pp: case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ (IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal.primeCompl (↑(Y.presheaf.stalk (f x)))
              (Localization.AtPrime (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom ≫
      CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯) =
    Scheme.Hom.stalkMap f x ≫
      (IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl (↑(X.presheaf.stalk x))
              (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom

Tactic:
· rw [← Iso.comp_inv_eq]
    ext1
    apply IsLocalization.ringHom_ext
      (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal.primeCompl
    ext a
    dsimp [← AlgEquiv.symm_toRingEquiv]
    simp only [IsLocalization.map_eq, RingHom.id_apply, Localization.localRingHom_to_map,
      RingHomCompTriple.comp_apply]
    simp only [RingHom.algebraMap_toAlgebra, Scheme.Hom.germ_stalkMap_apply, Scheme.Hom.appLE,
      homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
      X.presheaf.germ_res_apply]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i)) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.f j i ≫ D.ι j))

Tactic:
← image_inter,

Goal state after:
D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i)) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹'
      (Set.range ⇑(ConcreteCategory.hom (D.ι j)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι i)))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R✝ S✝ : CommRingCat
f✝ : R✝ ⟶ S✝
p✝ : PrimeSpectrum ↑S✝
x : PrimeSpectrum ↑R✝
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
      (Arrow.mk
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk (Hom.stalkMap (Spec.map f) p)).hom ≫ (Spec.stalkIso S p).hom

Tactic:
rw [← Scheme.localRingHom_comp_stalkIso]

Goal state after:
R✝ S✝ : CommRingCat
f✝ : R✝ ⟶ S✝
p✝ : PrimeSpectrum ↑S✝
x : PrimeSpectrum ↑R✝
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
      (Arrow.mk
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk
          ((Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
            CommRingCat.ofHom
                (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                  (CommRingCat.Hom.hom f) ⋯) ≫
              (Spec.stalkIso S p).inv)).hom ≫
      (Spec.stalkIso S p).hom
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ Scheme

Tactic:
apply LocallyRingedSpace.IsOpenImmersion.scheme
    D.toLocallyRingedSpaceGlueData.toGlueData.glued

Goal state after:
D : GlueData
⊢ ∀ (x : ↑D.toLocallyRingedSpaceGlueData.glued.toTopCat),
    ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ LocallyRingedSpace.IsOpenImmersion f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.refine_2
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))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f k i) (D.f k j))
⊢ (TopCat.Hom.hom (inv (D.t' k i j)).base) ((ConcreteCategory.hom (D.t' k i j).base) x) = x

Tactic:
rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.hom_inv_id, id_base,
        ConcreteCategory.id_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ (ConcreteCategory.hom (((gluedCover 𝒰).ι (idx 𝒰 x)).base ≫ (fromGlued 𝒰).base)) y = x

Tactic:
rw [← 𝒰.ι_fromGlued (𝒰.idx x)] at h

Goal state after:
case h
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : ((gluedCover 𝒰).ι (idx 𝒰 x) ≫ fromGlued 𝒰) y = x
⊢ (ConcreteCategory.hom (((gluedCover 𝒰).ι (idx 𝒰 x)).base ≫ (fromGlued 𝒰).base)) y = x
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
⊢ X ⟶ Y

Tactic:
refine inv 𝒰.ulift.fromGlued ≫ ?_
  fapply Multicoequalizer.desc
  · exact fun i ↦ f _
  rintro ⟨i, j⟩
  dsimp
  change pullback.fst _ _ ≫ f _ = (_ ≫ _) ≫ f _
  simpa [pullbackSymmetry_hom_comp_fst] using hf _ _

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
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      (gluing 𝒰 f g).openCover.f j ≫ p2 𝒰 f g =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.f j ≫ f) g

Tactic:
GlueData.openCover_f,

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ (gluing 𝒰 f g).ι j ≫ p2 𝒰 f g =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: I : Type u_1
inst✝¹ : Category.{v_1, u_1} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝ : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ IsAffine c.pt

Tactic:
have : c.pt ≅ Spec Γ(c.pt, ⊤) := hc.conePointUniqueUpToIso ((IsLimit.postcomposeHomEquiv
    (asIso α).symm _).symm (isLimitOfPreserves (Scheme.Γ.rightOp ⋙ Scheme.Spec) hc))

Goal state after:
I : Type u_1
inst✝¹ : Category.{v_1, u_1} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝¹ : ∀ (i : I), IsIso (α.app i)
this✝ : IsIso α
this : c.pt ≅ Spec Γ(c.pt, ⊤)
⊢ IsAffine c.pt
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
GlueData.openCover_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✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv
Module: Mathlib.AlgebraicGeometry.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)) ≫
        (𝒱 i).f ⟨i, (j, j)⟩.snd.2) ≫
      pullback.fst f (𝒰.f i) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.snd f f

Tactic:
simp [diagonalCover_map]

Goal state after:
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.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) ≫
      pullback.fst f (𝒰.f i) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.fst f f

Tactic:
simp [diagonalCover_map]

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

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

Tactic:
introv R _

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R S)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top.x
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
⊢ IsOpenCover fun i ↦ i₂ ⁻¹ᵁ U i

Tactic:
simp only [IsOpenCover, ← top_le_iff] at hU ⊢

Goal state after:
case of_sSup_eq_top.x
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
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
hU : ⊤ ≤ iSup U
⊢ ⊤ ≤ ⨆ i, i₂ ⁻¹ᵁ U i
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this✝² : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
this✝¹ :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H : ∀ (a : ↑s), Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))
this✝ : (a : ↑s) → Algebra S' (Sₐ a) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
a : ↑s
⊢ P ((algebraMap S' (Sₐ a)).comp (IsLocalization.Away.map R' S' f r))

Tactic:
rw [algebraMap_toAlgebra, IsLocalization.Away.map, IsLocalization.map_comp_map]
    exact hPl ((algebraMap _ (Localization.Away a.val)).comp f) r R' (Sₐ a) (hs _ a.2)

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))

Tactic:
have hM (a : s) : M.map ((algebraMap S (Localization.Away a.val)).comp f) = Mₐ a :=
    (M.map_map _ _).symm

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.map S' f ⋯))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.primeHeight = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

Tactic:
rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_ringKrullDim_iff]

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

Goal state before:
pp: case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
      ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ P (Spec.map (CommRingCat.ofHom f))

Tactic:
apply IsZariskiLocalAtSource.of_openCover (Scheme.affineOpenCoverOfSpanRangeEqTop
      (fun i : s ↦ (i : S)) (by simpa)).openCover

Goal state after:
case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝³ : IsZariskiLocalAtTarget P
inst✝² : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
      ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ ∀ (i : (Scheme.affineOpenCoverOfSpanRangeEqTop (fun i ↦ ↑i) ⋯).openCover.I₀),
    P ((Scheme.affineOpenCoverOfSpanRangeEqTop (fun i ↦ ↑i) ⋯).openCover.f i ≫ Spec.map (CommRingCat.ofHom f))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑(r + 1) ∧ ↑(r + 1) ≤ J.height

Tactic:
have : ¬(I : Set R) ⊆ ⋃ K ∈ hS.toFinset, (K : Set R) := by
      refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
      · rintro K hK - -
        rw [Set.Finite.mem_toFinset] at hK
        exact hK.1.isPrime
      · push Not
        intro K hK e
        have := hr.trans (Ideal.height_mono e)
        rw [Set.Finite.mem_toFinset] at hK
        rw [hK.2, ← not_lt] at this
        norm_cast at this
        exact this r.lt_succ_self

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
this : ¬↑I ⊆ ⋃ K ∈ hS.toFinset, ↑K
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑(r + 1) ∧ ↑(r + 1) ≤ J.height
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝⁶ : IsZariskiLocalAtTarget P
inst✝⁵ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom f))

Tactic:
exact IsZariskiLocalAtSource.comp hf ..

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
⊢ I.ideal V ≤ J.ideal V

Tactic:
have : ∀ x : V.1, ∃ (i : ι) (r : Γ(X, V.1)) (rU : Γ(X, U i)),
      X.basicOpen r = X.basicOpen rU ∧ x.1 ∈ X.basicOpen r := by
    intro ⟨x, hxV⟩
    obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp (hU.ge (Set.mem_univ x))
    exact ⟨i, exists_basicOpen_le_affine_inter V.2 (U i).2 _ ⟨hxV, hi⟩⟩

Goal state after:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
this : ∀ (x : ↥↑V), ∃ i r rU, X.basicOpen r = X.basicOpen rU ∧ ↑x ∈ X.basicOpen r
⊢ I.ideal V ≤ J.ideal V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ I.ideal U ≤ J.ideal U

Tactic:
rw [← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) I (le_top (a := U.1)),
    ← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) J (le_top (a := U.1))]

Goal state after:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal ⟨⊤, ⋯⟩) ≤
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (J.ideal ⟨⊤, ⋯⟩)
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
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ ∀ (J : Ideal ↑S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Q)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) J) J (CommRingCat.Hom.hom φ) ⋯)

Tactic:
intro P

Goal state after:
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
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
P : Ideal ↑S
⊢ ∀ (x : P.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Q)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ residueFieldCongr e ≪≫ residueFieldCongr e' = residueFieldCongr ⋯

Tactic:
by
  subst e e'
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ (residueFieldCongr e).hom ≫ (residueFieldCongr e').hom = (residueFieldCongr ⋯).hom

Tactic:
by
  subst e e'
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ tensorCongr e ≪≫ tensorCongr e' = tensorCongr ⋯

Tactic:
by
  subst e e'
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ (tensorCongr e).hom ≫ (tensorCongr e').hom = (tensorCongr ⋯).hom

Tactic:
by
  subst e e'
  rfl

Goal state after: