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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x'

Tactic:
subst hfg

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x : ↑X.toTopCat
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x

Tactic:
subst hfg

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
⊢ (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
    X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)

Tactic:
ext x

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) ↔
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
have h : _ ≫ _ = _ ≫ _ ≫ _ :=
      congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
h :
  (X.restrict hf).presheaf.map (eqToHom hV).op ≫
      g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    (X.restrict hf).presheaf.map (eqToHom hV).op ≫
      g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) = unop V ⊓ X.basicOpen f

Tactic:
ext x

Goal state after:
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) ↔ x ∈ ↑(unop V ⊓ X.basicOpen f)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

Tactic:
ext x

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (locallyRingedSpaceMap (f ≫ g)).toHom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom

Tactic:
by
    rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_comp]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ X.zeroLocus ↑(Ideal.span s) = X.zeroLocus s

Tactic:
ext x

Goal state after:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥X
⊢ x ∈ X.zeroLocus ↑(Ideal.span s) ↔ x ∈ X.zeroLocus s
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
⊢ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) = X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
ext x

Goal state after:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↥X
⊢ x ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) ↔ x ∈ X.zeroLocus s ∪ (↑U)ᶜ
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.zeroLocus Set.univ = (↑U)ᶜ

Tactic:
ext x

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
⊢ x ∈ X.zeroLocus Set.univ ↔ x ∈ (↑U)ᶜ
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
⊢ (Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f) = PrimeSpectrum.basicOpen f

Tactic:
ext x

Goal state after:
R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ x ∈ ↑((Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔ x ∈ ↑(PrimeSpectrum.basicOpen f)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑R
⊢ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) = PrimeSpectrum.zeroLocus s

Tactic:
ext x

Goal state after:
R : CommRingCat
s : Set ↑R
x : ↥(Spec R)
⊢ x ∈ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) ↔ x ∈ PrimeSpectrum.zeroLocus s
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
⊢ (P ⊓ Q).precoverage = P.precoverage ⊓ Q.precoverage

Tactic:
by
  ext X R
  exact ⟨fun hS ↦ ⟨fun _ _ hf ↦ (hS hf).left, fun _ _ hf ↦ (hS hf).right⟩,
    fun h ↦ fun _ _ hf ↦ ⟨h.left hf, h.right hf⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
⊢ iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W

Tactic:
ext x

Goal state after:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
⊢ IsPullback g iU iV f

Tactic:
let e := IsOpenImmersion.isoOfRangeEq (pullback.snd iV f) iU
    (by simpa [range_pullbackSnd] using congr(($H').1))

Goal state after:
U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ IsPullback g iU iV f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑f '' X.zeroLocus s = Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑f

Tactic:
ext x

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥Y
⊢ x ∈ ⇑f '' X.zeroLocus s ↔ x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑f
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 j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
⊢ (Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj
      ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)) =
    ⊥

Tactic:
ext x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
⊢ x ∈
      ↑((Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj
          ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U))) ↔
    x ∈ ↑⊥
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
h : ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
⊢ { I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
by
        rw [presieve₀_mem_precoverage_iff]
        exact ⟨h, inferInstance⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
H : CompactSpace ↥X
⊢ Fintype 𝒰.finiteSubcover.I₀

Tactic:
delta OpenCover.finiteSubcover; infer_instance

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

Goal state before:
pp: case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
this :
  f.stalkMap ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x) ≫
      PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x =
    eqToHom ⋯ ≫
      g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x) ≫ PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))

Tactic:
← IsIso.eq_inv_comp

Goal state after:
case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x =
    inv
        (f.stalkMap
          ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x)) ≫
      eqToHom ⋯ ≫
        g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x) ≫ PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : ↑↑s.pt.toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd
        ((ConcreteCategory.hom
            (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)).base)
          x) ≫
      PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x =
    eqToHom ⋯ ≫ s.snd.stalkMap x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))

Tactic:
← IsIso.eq_inv_comp

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : ↑↑s.pt.toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap
      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
        (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
      x =
    inv
        (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd
          ((ConcreteCategory.hom
              (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                  (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)).base)
            x)) ≫
      eqToHom ⋯ ≫ s.snd.stalkMap x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))
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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
hb : b ∈ {f | (isLocallyFraction R M).pred f}
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (a + b) (i x)

Tactic:
obtain ⟨Va, ma, ia, ra, sa, wa⟩ := ha x

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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
hb : b ∈ {f | (isLocallyFraction R M).pred f}
x : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa : ∀ (x : ↥Va), ∃ (hs : sa ∉ (↑x).asIdeal), (fun x ↦ a (ia x)) x = LocalizedModule.mk ra ⟨sa, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (a + b) (i x)
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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations A ↑x
ha : a ∈ (sectionsSubmodule A U).carrier
hb : b ∈ (sectionsSubmodule A U).carrier
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R A).pred fun x ↦ (a * b) (i x)

Tactic:
obtain ⟨Va, ma, ia, ra, sa, wa⟩ := ha x

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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations A ↑x
ha : a ∈ (sectionsSubmodule A U).carrier
hb : b ∈ (sectionsSubmodule A U).carrier
x : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa : ∀ (x : ↥Va), ∃ (hs : sa ∉ (↑x).asIdeal), (fun x ↦ a (ia x)) x = LocalizedModule.mk ra ⟨sa, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R A).pred fun x ↦ (a * b) (i x)
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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)

Tactic:
obtain ⟨V, hxV, hVU, rx, rs, hr⟩ := r.2 x

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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V
hVU : V ⟶ U
rx rs : R
hr : ∀ (x : ↥V), ∃ (hs : rs ∉ (↑x).asIdeal), (fun x ↦ ↑r (hVU x)) x = LocalizedModule.mk rx ⟨rs, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ f ≫ ⟨↑e_Ring.symm, ⋯⟩ = 𝟙 X

Tactic:
ext x

Goal state after:
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
x : X.α
⊢ ↑(ConcreteCategory.hom (f ≫ ⟨↑e_Ring.symm, ⋯⟩)) x = ↑(ConcreteCategory.hom (𝟙 X)) x
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ ⟨↑e_Ring.symm, ⋯⟩ ≫ f = 𝟙 Y

Tactic:
ext x

Goal state after:
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
x : Y.α
⊢ ↑(ConcreteCategory.hom (⟨↑e_Ring.symm, ⋯⟩ ≫ f)) x = ↑(ConcreteCategory.hom (𝟙 Y)) x
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))

Tactic:
ext x

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
x : ↑(CommRingCat.of (Localization (G.obj U)))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (𝟙 (F.obj U))) ⋯)))
      x =
    (CommRingCat.Hom.hom (𝟙 (CommRingCat.of (Localization (G.obj U))))) x
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 : R
f : M
g : ↥(Submonoid.powers s)
⊢ basicOpen s ≤ basicOpen ↑g

Tactic:
by
    have := PrimeSpectrum.le_basicOpen_pow s; aesop (add simp [Submonoid.mem_powers_iff])

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ ↑((X.homOfLE e) x) = ↑x

Tactic:
Scheme.homOfLE_apply'

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥U
⊢ ↑⟨↑x, ⋯⟩ = ↑x
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W = V.ι ''ᵁ W ⊓ U

Tactic:
ext x

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
x : ↥X
⊢ x ∈ ↑(U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W) ↔ x ∈ ↑(V.ι ''ᵁ W ⊓ U)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
n : ℕ
hn : f ^ n ∈ ⊥.colon {d • a - b • c}
⊢ ⟨f ^ n, ⋯⟩ • d • a = ⟨f ^ n, ⋯⟩ • b • c

Tactic:
simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f g : ↑R
⊢ algebraMap (↑R) (Localization.Away (f * g)) =
    (IsLocalization.Away.awayToAwayRight f g).comp (algebraMap (↑R) (Localization.Away f))

Tactic:
ext x

Goal state after:
R : CommRingCat
f g x : ↑R
⊢ (algebraMap (↑R) (Localization.Away (f * g))) x =
    ((IsLocalization.Away.awayToAwayRight f g).comp (algebraMap (↑R) (Localization.Away f))) x
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
⊢ f ∈ (Ideal.span (Set.range b)).radical

Tactic:
have : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f} := by
      simpa [← SetLike.coe_subset_coe, ← Set.compl_iInter,
        ← PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.Top] using iU
    rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span,
      PrimeSpectrum.mem_vanishingIdeal]
    exact fun x hx ↦ by simpa using this hx

Goal state after:
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
f : R
⊢ toOpenₗ R M (basicOpen f) =
    ↑(LinearEquiv.ofBijective (toBasicOpenₗ R M f) ⋯) ∘ₗ LocalizedModule.mkLinearMap (Submonoid.powers f) M

Tactic:
ext x

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
f : R
x : M
⊢ (toOpenₗ R M (basicOpen f)) x =
    (↑(LinearEquiv.ofBijective (toBasicOpenₗ R M f) ⋯) ∘ₗ LocalizedModule.mkLinearMap (Submonoid.powers f) M) x
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ IsPushout (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X)) (coequalizer.π f g) (f ≫ coequalizer.π f g)

Tactic:
by
  refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
  · refine fun s ↦ coequalizer.desc s.inl ?_
    have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)
    have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)
    exact H₁.trans H₂.symm
  · exact fun s ↦ by simp
  · exact fun s ↦ by simpa using congr(coprod.inl ≫ $s.condition)
  · exact fun s m hm _ ↦ by ext; simp [*]

Goal state after: