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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (f.toHom ≫ g.toHom) x))

Tactic:
rw [PresheafedSpace.stalkMap.comp]

Goal state after:
X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (g.stalkMap ((ConcreteCategory.hom f.base) x) ≫ f.stalkMap x))
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (𝟙 (sheafedSpaceObj R)).hom.c

Tactic:
ext
    dsimp
    rw [comap_id (by simp)]
    simp
    rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ inv (invApp f U) = f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
rw [← cancel_epi (H.invApp _ U), IsIso.hom_inv_id]
  delta invApp
  simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ IsLocalizedModule p.asIdeal.primeCompl (toPushforwardStalkAlgHom R S p).toLinearMap

Tactic:
apply IsLocalizedModule.mkOfAlgebra

Goal state after:
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ x ∈ p.asIdeal.primeCompl,
    IsUnit
      ((algebraMap ↑R
          ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).obj).stalk
              p))
        x)

case h₂
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀
    (y :
      ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).stalk
          p)),
    ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
R : Presieve X
h : ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))
x : F.obj X
⊢ ∃ Y g, map F R g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
obtain ⟨Y, g, hg, hi⟩ := h x

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
R : Presieve X
h : ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))
x : F.obj X
Y : C
g : Y ⟶ X
hg : R g
hi : x ∈ Set.range ⇑(ConcreteCategory.hom (F.map g))
⊢ ∃ Y g, map F R g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ (basicOpenIsoSpecAway x).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv

Tactic:
subst hx
  rw [← cancel_mono (Scheme.Opens.ι _)]
  simp only [basicOpenIsoSpecAway, Category.assoc, Scheme.homOfLE_ι,
    IsOpenImmersion.isoOfRangeEq_inv_fac]
  simp only [← Spec.map_comp, ← CommRingCat.ofHom_comp]
  congr
  ext x
  exact (IsLocalization.Away.awayToAwayRight_eq f g x (S := Localization.Away f)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (Y.homOfLE ⋯) (resLE iY UT UY ⋯) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (T.homOfLE hUST)

pp: case refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)

Tactic:
· refine (IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_).flip
    simp only [Scheme.opensRange_homOfLE, ← Scheme.Hom.comp_preimage, Scheme.Hom.resLE_comp_ι]
    rw [Scheme.Hom.comp_preimage, ← (g ⁻¹ᵁ UX).ι.image_injective.eq_iff]
    simp only [Scheme.Hom.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]
    simp [hUY]

Goal state after:
case refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)
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

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this : IsAffine ↑U
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f

Tactic:
have : IsAffine U := hU

Goal state after:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    (CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        Y.toΓSpec.c.app (op (basicOpen r))) ≫
      ((𝟭 LocallyRingedSpace).map f).c.app (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r)))))

Tactic:
Y.toΓSpecSheafedSpace_app_spec,

Goal state after:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    Y.toToΓSpecMapBasicOpen r ≫
      ((𝟭 LocallyRingedSpace).map f).c.app (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r)))))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : Function.Bijective ⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ Function.Bijective ⇑((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)

Tactic:
convert! this using 2 with a

Goal state after:
R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : Function.Bijective ⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ ⇑((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x) =
    ⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case convert_15
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s✝ : ↑((structureSheaf R).obj.obj (op U))
p : ↥V
m : R
s : ↥(PrimeSpectrum.comap f ↑p).asIdeal.primeCompl
⊢ Localization.mk (f m) ⟨f ↑s, ⋯⟩ =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (Localization.mk m s)

Tactic:
simp [Localization.mk_eq_mk']

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case convert_15
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (Localization.mk a ⟨b, ⋯⟩) =
    Localization.mk (f a) ⟨f b, ⋯⟩

Tactic:
simp [Localization.mk_eq_mk']

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ (↑U).basicOpen ((hom U.topIso.inv) r) = (↑U).basicOpen ((hom (X.presheaf.map (homOfLE ⋯).op)) r)

Tactic:
rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.ι_preimage_self.symm).op,
    ← ConcreteCategory.comp_apply]

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ (↑U).basicOpen ((hom U.topIso.inv) r) =
    (↑U).basicOpen ((hom (X.presheaf.map (homOfLE ⋯).op ≫ (↑U).presheaf.map (eqToHom ⋯).op)) r)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶ pullback (h.V j k).inclusion' (h.V j i).inclusion'

Tactic:
refine (pullbackIsoProdSubtype _ _).hom ≫ ofHom ⟨?_, ?_⟩ ≫ (pullbackIsoProdSubtype _ _).inv
  · intro x
    refine ⟨⟨⟨(h.t i j x.1.1).1, ?_⟩, h.t i j x.1.1⟩, rfl⟩
    rcases x with ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩
    exact h.t_inter _ ⟨x, hx⟩ hx'
  fun_prop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ fst (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i) = snd (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f j)) ≫ fst f (𝒰.f j)

Tactic:
rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ map (fst f (𝒰.f i) ≫ f)
      (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd _ _) (𝟙 _) (𝟙 _) (by simp) (by simp))]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {Z : Scheme} →
    (f : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inl)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inl) ⋯).fst
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inr)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inr) ⋯).fst)

Tactic:
dsimp
      refine fun {Z} f ↦ (nonempty_isColimit_binaryCofanMk_of_isCompl _ _ ?_).some
      rw [Scheme.Hom.opensRange_pullbackFst, Scheme.Hom.opensRange_pullbackFst]
      convert! (isCompl_range_inl_inr X Y).map (CompleteLatticeHom.setPreimage f)
      simp [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsIso (coprodSpec R S)

Tactic:
rw [isIso_iff_isIso_stalkMap]
  refine ⟨?_, isIso_stalkMap_coprodSpec R S⟩
  convert_to IsIso (TopCat.isoOfHomeo (X := Spec (.of <| R × S)) <|
    PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec <| .of R) (Spec <| .of S))).inv
  · ext x; exact coprodSpec_apply R S x
  · infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ coprod.inr ≫
      coprodComparison Scheme.Spec (op R) (op S) ≫
        Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv) =
    coprod.inr ≫ coprodSpec ↑R ↑S

Tactic:
rw [coprodComparison_inr_assoc, coprodSpec, coprod.inr_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inr,
        limit.isoLimitCone_inv_π]

Goal state after:
case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.right }) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
⊢ IsIso (sigmaSpec R)

Tactic:
by
  have : sigmaSpec R =
      (colimit.isoColimitCocone ⟨_,
        (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm _).symm (isColimitOfPreserves
          Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R)))⟩).hom := by
    ext1
    simp; rfl
  rw [this]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ Function.Injective
    ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.left)))

Tactic:
simpa using! f.isOpenEmbedding.injective

Goal state after:
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 α
this : c.pt ≅ Spec Γ(c.pt, ⊤)
⊢ IsAffine c.pt

Tactic:
exact .of_isIso this.hom

Goal state after:
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)
⊢ IsAffine c.pt

Tactic:
by
  let α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
  have (i : _) : IsIso (α.app i) := IsAffine.affine
  have : IsIso α := NatIso.isIso_of_isIso_app α
  have : c.pt ≅ Spec Γ(c.pt, ⊤) := hc.conePointUniqueUpToIso ((IsLimit.postcomposeHomEquiv
    (asIso α).symm _).symm (isLimitOfPreserves (Scheme.Γ.rightOp ⋙ Scheme.Spec) hc))
  exact .of_isIso this.hom

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

Goal state before:
pp: case h.hU
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U ⊆ Set.range ⇑(ConcreteCategory.hom (D.f i i).base)

Tactic:
Set.range_eq_univ.mpr _

Goal state after:
case h.hU
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U ⊆ Set.univ

C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (D.f i i).base)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S))) =
    (Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))

Tactic:
simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S))) =
    (Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))

Tactic:
simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]

Goal state after:
case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
⊢ P ((algebraMap S Sₜ).comp f)

pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝ :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P ((algebraMap S Sₜ).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
· let e : Localization.Away t ≃+* Sₜ :=
      (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv
    have : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t)) :=
      RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _) _).symm)
    rw [this, RingHom.comp_assoc]
    exact hP.left _ _ (hs t ht)

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝ :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P ((algebraMap S Sₜ).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
inst✝³ : I.IsPrime
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization.AtPrime A I
this : IsLocalRing A
⊢ ringKrullDim A = ↑I.height

Tactic:
rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim,
      ← IsLocalization.height_under I.primeCompl,
      ← IsLocalization.AtPrime.under_maximalIdeal A I]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0

Tactic:
← map_zero (X.presheaf.germ _ x hxU).hom

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
⊢ (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal

Tactic:
refine hs.induction_on _ (by simp) fun {i s} his hs e ↦ ?_
  simp only [iInf_insert, e, ideal_inf]

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

Goal state before:
pp: ⊢ isomorphisms Scheme =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f

Tactic:
rw [isomorphisms_eq_isOpenImmersion_inf_surjective, isOpenImmersion_eq_inf,
    surjective_eq_topologically, inf_right_comm]
  congr 1
  ext X Y f
  exact ⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo
    (H.1.1.toHomeomorphOfSurjective H.2)).hom), fun (_ : IsIso f.base) ↦
    let e := (TopCat.homeoOfIso <| asIso f.base); ⟨e.isOpenEmbedding, e.surjective⟩⟩

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

Goal state before:
pp: case inr
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↥X), IsAffine X ∧ IsAffine Y → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
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
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
← hQ'.arrow_mk_iso_iff (Scheme.Hom.resLEStalkMap f e ⟨x, hx⟩)

Goal state after:
case inr
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
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f → ∀ (x : ↥X), IsAffine X ∧ IsAffine Y → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
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
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.resLE f U V e) ⟨x, hx⟩))