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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
⊢ IsIso
    ((colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).c.app
      (op (H.functor.obj U)))

Tactic:
rw [PresheafedSpace.comp_c_app,
      ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
⊢ IsIso
    ((preservesColimitIso forgetToPresheafedSpace F).inv.c.app (op (H.functor.obj U)) ≫
      (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj
              (unop (op (H.functor.obj U))))).hom ≫
        limit.π
          (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (unop (op (H.functor.obj U)))))
          (op i))
Module: Mathlib.AlgebraicGeometry.Cover.Open

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

Tactic:
by
  cases nonempty_fintype 𝒰.I₀
  rw [← isCompact_univ_iff, ← 𝒰.iUnion_range]
  apply isCompact_iUnion
  intro i
  rw [isCompact_iff_compactSpace]
  exact
    @Homeomorph.compactSpace _ _ _ _ (H i)
      (TopCat.homeoOfIso
        (asIso
          (IsOpenImmersion.isoOfRangeEq (𝒰.f i)
            (X.ofRestrict (Opens.isOpenEmbedding ⟨_, (𝒰.map_prop i).base_open.isOpen_range⟩))
            Subtype.range_coe.symm).hom.base))

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ Set.range ⇑(ConcreteCategory.hom (lift f g H').base) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
have := pullback_snd_isIso_of_range_subset f g H'
  dsimp only [lift]
  have : _ = (pullback.fst f g).base :=
    PreservesPullback.iso_hom_fst
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
  rw [LocallyRingedSpace.comp_base, ← this, ← Category.assoc, TopCat.coe_comp, Set.range_comp,
      Set.range_eq_univ.mpr, Set.image_univ]
  · rw [TopCat.pullback_fst_range]
    ext
    constructor
    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
  · rw [← TopCat.epi_iff_surjective, show (inv (pullback.snd f g)).base = _ from
        (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _).map_inv _]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen
      ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op))
        ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r))

Tactic:
rw [← CommRingCat.comp_apply, ← CategoryTheory.Functor.map_comp, ← op_comp, eqToHom_trans,
    eqToHom_refl, op_id]

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (𝟙 (op (⋯.functor.obj ⊤))))) r)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ ↑(f ⁻¹ᵁ U) ≅ ↑U

Tactic:
by
  apply IsOpenImmersion.isoOfRangeEq (f := (f ⁻¹ᵁ U).ι ≫ f) U.ι _
  dsimp
  rw [Set.range_comp, Opens.range_ι, Opens.range_ι]
  refine @Set.image_preimage_eq _ _ f U.1 f.homeomorph.surjective

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
⊢ Arrow.mk (f ∣_ Scheme.Hom.opensRange g) ≅ Arrow.mk (pullback.snd f g)

Tactic:
let V : Y.Opens := g.opensRange

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
⊢ Arrow.mk (f ∣_ Scheme.Hom.opensRange g) ≅ Arrow.mk (pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Set.range ⇑f = Set.range ⇑(Y.ofRestrict ⋯)

Tactic:
exact Subtype.range_val.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Tactic:
have : IsAffine U := hU
  have : IsAffine _ := hV
  conv_rhs =>
    rw [fromSpec, ← X.homOfLE_ι (V := U) f.unop.le, isoSpec_inv, Category.assoc,
      ← Scheme.isoSpec_inv_naturality_assoc,
      ← Spec.map_comp_assoc, Scheme.homOfLE_appTop, ← Functor.map_comp]
  rw [fromSpec, isoSpec_inv, Category.assoc, ← Spec.map_comp_assoc, ← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ ⋯.fromSpec = X.isoSpec.inv

Tactic:
rw [fromSpec, Iso.inv_comp_eq]

Goal state after:
X : Scheme
inst✝ : IsAffine X
⊢ ⊤.ι = ⋯.isoSpec.hom ≫ X.isoSpec.inv
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) = PrimeSpectrum.basicOpen f

Tactic:
rw [← hU.fromSpec_preimage_basicOpen, Scheme.preimage_basicOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ⨆ f, X.basicOpen ↑f = U
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier

Tactic:
rw [h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ Arrow.mk (Spec.map f ∣_ basicOpen r) ≅
    Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))

Tactic:
by
  refine Arrow.isoMk ?_ ?_ ?_
  · exact (Spec _).isoOfEq (comap_basicOpen _ _) ≪≫ basicOpenIsoSpecAway (f.hom r)
  · exact basicOpenIsoSpecAway r
  · have hcomp : CommRingCat.ofHom (algebraMap R (Localization.Away r)) ≫
        CommRingCat.ofHom (Localization.awayMap f.hom r) =
        f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away (f.hom r))) := by
      ext x
      simp [Localization.awayMap, IsLocalization.Away.map]
    rw [← cancel_mono (Spec.map (CommRingCat.ofHom (algebraMap R _)))]
    simp only [Arrow.mk_hom, Category.assoc, ← Spec.map_comp]
    simp [hcomp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫ pullback.snd (pullback.fst gA gB ≫ gA) f =
    pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f

Tactic:
rw [← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,
    Over.hom_left_inv_left_assoc]
  simp [CartesianMonoidalCategory.prodComparison]

Goal state after:
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₂
x : (MultispanShape.prod (ulift 𝒰).gluedCover.J).R
⊢ Multicoequalizer.π (ulift 𝒰).gluedCover.diagram x ≫ (ulift 𝒰).fromGlued ≫ f₁ =
    Multicoequalizer.π (ulift 𝒰).gluedCover.diagram x ≫ (ulift 𝒰).fromGlued ≫ f₂

Tactic:
fromGlued,

Goal state after:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
x : (MultispanShape.prod (ulift 𝒰).gluedCover.J).R
⊢ Multicoequalizer.π (ulift 𝒰).gluedCover.diagram x ≫
      Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram X (fun x ↦ (ulift 𝒰).f x) ⋯ ≫ f₁ =
    Multicoequalizer.π (ulift 𝒰).gluedCover.diagram x ≫
      Multicoequalizer.desc (ulift 𝒰).gluedCover.diagram X (fun x ↦ (ulift 𝒰).f x) ⋯ ≫ f₂
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
⊢ (Disjoint on fun x ↦ Set.range ⇑(U x).ι) i j ↔ (Disjoint on U) i j

Tactic:
simp [← Opens.coe_disjoint]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
f : i ⟶ j
⊢ F.map f ≫ F.map (eqToHom ⋯) ≫ (glueData F).ι ((equivShrink J) j) =
    (F.map (eqToHom ⋯) ≫ (glueData F).ι ((equivShrink J) i)) ≫ ((Functor.const J).obj (glueData F).glued).map f

Tactic:
simp only [← IsIso.inv_comp_eq, ← Functor.map_inv, ← Functor.map_comp_assoc,
      glueDataι_naturality, Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id]

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

Goal state before:
pp: case h.left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))

Tactic:
apply π_ιInvApp_eq_id

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj ↔ ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
constructor; swap
  · rintro ⟨k, fi, fj, x, rfl, rfl⟩; simp only [← Scheme.Hom.comp_apply, colimit.w]
  obtain ⟨i, rfl⟩ := (equivShrink J).symm.surjective i
  obtain ⟨j, rfl⟩ := (equivShrink J).symm.surjective j
  rw [← ((isColimit F).coconePointUniqueUpToIso
    (colimit.isColimit F)).inv.isOpenEmbedding.injective.eq_iff]
  simp only [Limits.colimit, ← Scheme.Hom.comp_apply,
    colimit.comp_coconePointUniqueUpToIso_inv, cocone, glueDataι_naturality]
  refine ?_ ∘ ((glueData F).ι_eq_iff _ _ _ _).mp
  dsimp +instances only [GlueData.Rel]
  rintro ⟨x, rfl, rfl⟩
  obtain ⟨⟨k, ki, kj⟩, y, hy : F.map ki y = (glueData F).f i j x⟩ := mem_iSup.mp x.2
  refine ⟨k, ki, kj, y, hy, ?_⟩
  obtain ⟨k, rfl⟩ := (equivShrink J).symm.surjective k
  apply ((glueData F).ι _).isOpenEmbedding.injective
  simp only [← Scheme.Hom.comp_apply, Category.assoc, GlueData.glue_condition]
  trans (glueData F).ι k y
  · simp [← glueDataι_naturality F kj]; rfl
  · simp [← glueDataι_naturality F ki, ← hy]; rfl

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ Q (pullback.mapDesc f₁ f₂ (pullback.snd f g))

Tactic:
← Q.cancel_left_of_respectsIso (pullbackDiagonalMapIso f _ f₁ f₂).hom

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := isLocal_affineProperty P
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ Q ((pullbackDiagonalMapIso f g f₁ f₂).hom ≫ pullback.mapDesc f₁ f₂ (pullback.snd f g))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: ⊢ @SurjectiveOnStalks = stalkwise fun {R S} [CommRing R] [CommRing S] x ↦ Function.Surjective ⇑x

Tactic:
by
  ext; exact surjectiveOnStalks_iff _

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ SurjectiveOnStalks (Spec.map f) ∧ IsEmbedding ⇑(Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)

Tactic:
and_comm

Goal state after:
R S : CommRingCat
f : R ⟶ S
⊢ IsEmbedding ⇑(Spec.map f) ∧ SurjectiveOnStalks (Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
heq : Q = Q'
⊢ HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q'

Tactic:
← heq

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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
e' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
heq : Q = Q'
⊢ HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ P (𝟙 X ∣_ ↑U)

Tactic:
morphismRestrict_id,

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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ P (𝟙 ↑(𝟙 X ⁻¹ᵁ ↑U))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I J : Ideal S
h : J ∈ I.minimalPrimes
⊢ (↑e.idealComapOrderIso J).primeHeight = J.primeHeight

Tactic:
have : J.IsPrime := h.isPrime
    simp only [EquivLike.coe_coe, RingEquiv.idealComapOrderIso_apply,
      ← Ideal.height_eq_primeHeight, RingEquiv.height_comap_of_isPrime]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
⊢ Order.krullDim (PrimeSpectrum R) ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n

Tactic:
Order.krullDim_eq_iSup_height,

Goal state after:
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
⊢ ⨆ a, ↑(Order.height a) ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n
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 P) (comap (algebraMap R S) P)
⊢ (Ideal.map (algebraMap R S) p).height = p.height

Tactic:
simp_rw [P, under_map_of_isPrime_disjoint M S _ h] at this

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 pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : I = ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height

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:
· exact ⟨⊥, by simp [I_top]⟩

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ ⊥ = ⋂ U, X.zeroLocus ↑(⊤ U)

Tactic:
ext x
    simpa using X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ((I.ideal ⊓ J.ideal) U) =
    (I.ideal ⊓ J.ideal) (X.affineBasicOpen f)

Tactic:
dsimp
      have : (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom = algebraMap _ _ := rfl
      have inst := U.2.isLocalization_basicOpen f
      rw [← I.map_ideal_basicOpen U f, ← J.map_ideal_basicOpen U f, this]
      ext x
      obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (.powers f) x
      simp only [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff, Ideal.mem_inf,
        exists_exists_eq_and]
      refine ⟨fun ⟨n, h₁, h₂⟩ ↦ ⟨⟨n, h₁⟩, ⟨n, h₂⟩⟩, ?_⟩
      rintro ⟨⟨n₁, h₁⟩, ⟨n₂, h₂⟩⟩
      refine ⟨n₁ + n₂, ?_, ?_⟩
      · rw [add_comm, pow_add, mul_assoc]; exact Ideal.mul_mem_left _ _ h₁
      · rw [pow_add, mul_assoc]; exact Ideal.mul_mem_left _ _ h₂

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hs : Ideal.span ↑s = ⊤
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
apply iSup_basicOpen_of_span_eq_top at hs

Goal state after:
case refine_1
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
⊢ ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
x : ↥X
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)

Tactic:
by
  wlog h : ∃ R, X = Spec R
  · obtain ⟨R, f, hf, hsub⟩ := Scheme.exists_affine_mem_range_and_range_subset
      (show x ∈ ⊤ from trivial)
    obtain ⟨y, rfl⟩ := Set.mem_range.mp hsub.1
    rw [coheight_eq_of_isOpenImmersion, ← this _ ⟨R, rfl⟩]
    exact Order.krullDim_eq_of_orderIso
      (PrimeSpectrum.comapEquiv (asIso (Scheme.Hom.stalkMap f y)).commRingCatIsoToRingEquiv)
  obtain ⟨R, rfl⟩ := h
  let k : Algebra ↑R ↑((Spec R).presheaf.stalk x) := StructureSheaf.stalkAlgebra (↑R) x
  have : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x)) x.asIdeal :=
    StructureSheaf.IsLocalization.to_stalk R x
  rw [IsLocalization.AtPrime.ringKrullDim_eq_height x.asIdeal ((Spec R).presheaf.stalk x)]
  apply WithBot.coe_eq_coe.mpr
  exact idealHeight_eq_coheight R x

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 (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

Tactic:
← Ideal.mk_ker (I := I.ideal _)

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))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (Ideal.Quotient.mk (I.ideal U)))