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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.ofHom (toOpenₗ R M ⊤) ≫
      (structurePresheafInModuleCat R M).germ ⊤ x _root_.trivial ≫ stalkToLocalizationₗ R M x =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
germ_stalkToLocalizationₗ

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ openToLocalizationₗ R M ⊤ x _root_.trivial =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
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' i j k ≫ (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom =
    𝟙 (pullback (D.f i j) (D.f i k))

Tactic:
← cancel_mono (pullback.fst (D.f i j) (D.f i k))

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ (D.t' i j k ≫ (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom) ≫
      pullback.fst (D.f i j) (D.f i k) =
    𝟙 (pullback (D.f i j) (D.f i k)) ≫ pullback.fst (D.f i j) (D.f i k)
Module: Mathlib.CategoryTheory.GlueData

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

Tactic:
← cancel_mono (pullback.fst (D.f i j) (D.f i k))

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ inv (D.t' i j k) ≫ pullback.fst (D.f i j) (D.f i k) =
    ((pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom) ≫
      pullback.fst (D.f i j) (D.f i k)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (isLocallyFraction S N).pred (comapFun f U V hUV s)

Tactic:
rintro ⟨p, hpV⟩

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
⊢ ∃ V_1, ∃ (_ : ↑⟨p, hpV⟩ ∈ V_1), ∃ i, (isFractionPrelocal S N).pred fun x ↦ comapFun f U V hUV s (i x)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ ↔ Ideal.span s = ⊤

Tactic:
simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.zeroLocus {↑i})ᶜ = Set.univ ↔ Ideal.span s = ⊤
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ⨆ i ∈ s, X.basicOpen i ≤ U

Tactic:
iSup₂_le_iff

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ∀ i ∈ s, X.basicOpen i ≤ U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this : (ConcreteCategory.hom (colimit.ι diagram one)) x = (ConcreteCategory.hom (colimit.ι diagram one)) y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
have :
    (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ =
      (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ :=
    (congr_arg
        (colim.map (diagramIsoParallelPair diagram).hom ≫
          (colimit.isoColimitCocone (Types.coequalizerColimit _ _)).hom)
        this :
      _)

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this✝ : (ConcreteCategory.hom (colimit.ι diagram one)) x = (ConcreteCategory.hom (colimit.ι diagram one)) y
this :
  (ConcreteCategory.hom
        (colimit.ι diagram one ≫
          colim.map (diagramIsoParallelPair diagram).hom ≫
            (colimit.isoColimitCocone
                (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right))).hom))
      x =
    (ConcreteCategory.hom
        (colimit.ι diagram one ≫
          colim.map (diagramIsoParallelPair diagram).hom ≫
            (colimit.isoColimitCocone
                (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left)
                  (diagram.map WalkingParallelPairHom.right))).hom))
      y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ Ideal.map (ConcreteCategory.hom (X.presheaf.map (homOfLE hVU).op)) (Ideal.span s) = ⊤

Tactic:
hs,

Goal state after:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ Ideal.map (ConcreteCategory.hom (X.presheaf.map (homOfLE hVU).op)) ⊤ = ⊤
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i j)) z = (ConcreteCategory.hom (D.f i j)) z
e₂ :
  (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) =
    (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z)
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z) =
    (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z))

Tactic:
rw [D.glue_condition_apply]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) x)) = x✝

Tactic:
rw [D.glue_condition_apply]

Goal state after:
case mpr
D : GlueData
i j : D.J
x✝ : ↑D.glued
x : ↑(D.V (i, j))
hx : (ConcreteCategory.hom (D.f i j ≫ D.ι i)) x = x✝
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) x) = x✝
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
i j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)

Tactic:
simp only [t'_snd_snd, t'_fst_fst_fst, t'_fst_snd]

Goal state after:
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)

pp: case h.hU
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))
⊢ ↑((Opens.map (D.t k i).base).obj ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ⊆
    Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

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

Goal state after:
case h.hU
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))
⊢ ↑((Opens.map (D.t k i).base).obj ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ⊆
    Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
⊢ f₁ = f₂

Tactic:
by
  rw [← cancel_epi 𝒰.ulift.fromGlued]
  apply Multicoequalizer.hom_ext
  intro x
  rw [fromGlued, Multicoequalizer.π_desc_assoc, Multicoequalizer.π_desc_assoc]
  exact h _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case inv_hom_id
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₀
⊢ autoParam
    (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
      𝟙 (pullback (𝒰.f i ≫ f) g))
    Iso.inv_hom_id._autoParam

Tactic:
apply pullback.hom_ext
    · simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, Category.id_comp]
    · simp [p2]

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsAffine Z
⊢ P (f ≫ g) ↔ P g

Tactic:
← P.toProperty_apply,

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsAffine Z
⊢ P.toProperty (f ≫ g) ↔ P g
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsAffine Z
⊢ P.toProperty (f ≫ g) ↔ P g

Tactic:
← P.toProperty_apply,

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsAffine Z
⊢ P.toProperty (f ≫ g) ↔ P.toProperty g
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝³ : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsIso g
inst✝¹ : IsAffine Z
inst✝ : IsAffine Y
⊢ P (f ≫ g) ↔ P f

Tactic:
← P.toProperty_apply,

Goal state after:
P : AffineTargetMorphismProperty
inst✝³ : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsIso g
inst✝¹ : IsAffine Z
inst✝ : IsAffine Y
⊢ P.toProperty (f ≫ g) ↔ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝³ : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsIso g
inst✝¹ : IsAffine Z
inst✝ : IsAffine Y
⊢ P.toProperty (f ≫ g) ↔ P f

Tactic:
← P.toProperty_apply,

Goal state after:
P : AffineTargetMorphismProperty
inst✝³ : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsIso g
inst✝¹ : IsAffine Z
inst✝ : IsAffine Y
⊢ P.toProperty (f ≫ g) ↔ P.toProperty f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P f ↔ P f'

Tactic:
← P.toProperty_apply,

Goal state after:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P.toProperty f ↔ P f'
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P.toProperty f ↔ P f'

Tactic:
← P.toProperty_apply,

Goal state after:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P.toProperty f ↔ P.toProperty f'
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ (D.vPullbackCone i j).fst ≫ D.ι i = s.fst ≫ D.ι i

Tactic:
IsOpenImmersion.lift_fac_assoc

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ s.fst ≫ D.ι i = s.fst ≫ D.ι i
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: 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
hin : (algebraMap R S) y ∈ map (algebraMap R S) I
⊢ y ∈ J

Tactic:
grw [hle, IsLocalization.algebraMap_mem_map_algebraMap_iff (Submonoid.powers x)] at hin

Goal state after:
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
hin : ∃ m ∈ Submonoid.powers x, m * y ∈ J
⊢ y ∈ J
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
⊢ ∀ t ∈ ⇑e '' s,
    (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp (e.toRingHom.comp f))

Tactic:
· rintro - ⟨a, ha, rfl⟩
      let e' : Localization.Away a ≃+* Localization.Away (e a) :=
        IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a)
      have : (algebraMap T (Localization.Away (e a))).comp e.toRingHom =
          e'.toRingHom.comp (algebraMap S (Localization.Away a)) := by
        ext x
        simp [e']
      rw [← RingHom.comp_assoc, this, RingHom.comp_assoc]
      apply hPi.left
      exact hs a ha

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

Goal state before:
pp: case h₁
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ RingHom.SurjectiveOnStalks

Tactic:
exact (HasRingHomProperty.isLocal_ringHomProperty @SurjectiveOnStalks).respectsIso

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
U : Set ↥Y
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (⇑f ⁻¹' U)

Tactic:
obtain ⟨S, hS, rfl⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU', hU⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
S : Set ↑Y.affineOpens
hS : S.Finite
hU : IsOpen (⋃ i ∈ S, ↑↑i)
hU' : IsCompact (⋃ i ∈ S, ↑↑i)
⊢ IsCompact (⇑f ⁻¹' ⋃ i ∈ S, ↑↑i)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case openCover
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
Scheme.Hom.appLE_map

Goal state after:
case openCover
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen ↑r) ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case hU
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
Scheme.Hom.appLE_map

Goal state after:
case hU
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i)).ι ''ᵁ ⊤) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))
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
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
⊢ P f

Tactic:
refine of_source_openCover (X.openCoverOfIsOpenCover _ hU) fun i ↦ ?_

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
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).f i ≫ f)))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
this : P.IsPrime
⊢ ↑(⨅ J ∈ I.minimalPrimes, J.height) ≤ ringKrullDim R

Tactic:
refine (WithBot.coe_le_coe.mpr (iInf₂_le _ hP)).trans P.height_le_ringKrullDim_of_isPrime

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I < M
⊢ I.IsMaximal

Tactic:
have h1 := Ideal.height_strict_mono_of_isPrime hM'
    have h2 := e ▸ M.height_le_ringKrullDim_of_ne_top hM.ne_top
    simp [← not_lt, h1] at h2

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))
    (comap (algebraMap R S) (Ideal.map (algebraMap R S) p))
⊢ (Ideal.map (algebraMap R S) p).height = p.height

Tactic:
under_map_of_isPrime_disjoint M S _ h

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
⊢ (Ideal.map (algebraMap R S) p).height = p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.refine_1.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ ⨆ (_ : RelSeries.last p ≤ RelSeries.last p), ↑p.length ≤ (RelSeries.last p).asIdeal.primeHeight

Tactic:
· exact le_iSup (fun p' => (⨆ _, p'.length : ℕ∞)) p

Goal state after: