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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
⊢ ∀ ⦃X_1 Y_1 : (Opens ↑↑X)ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
    X.presheaf.map f_1 ≫ invApp f (unop Y_1) ≫ g.c.app (op (⋯.functor.obj (unop Y_1))) ≫ Y.presheaf.map (eqToHom ⋯) =
      (invApp f (unop X_1) ≫ g.c.app (op (⋯.functor.obj (unop X_1))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map f_1

Tactic:
intro U

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ ∀ ⦃Y_1 : (Opens ↑↑X)ᵒᵖ⦄ (f_1 : U ⟶ Y_1),
    X.presheaf.map f_1 ≫ invApp f (unop Y_1) ≫ g.c.app (op (⋯.functor.obj (unop Y_1))) ≫ Y.presheaf.map (eqToHom ⋯) =
      (invApp f (unop U) ≫ g.c.app (op (⋯.functor.obj (unop U))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map f_1
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Function.Injective fun x ↦ f ''ᵁ x

Tactic:
intro U

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ ∀ ⦃a₂ : X.Opens⦄, (fun x ↦ f ''ᵁ x) U = (fun x ↦ f ''ᵁ x) a₂ → U = a₂
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map ((Opens.map s.snd.base).op.map (⋯.functor.op.map i) ≫ eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i

Tactic:
← s.pt.presheaf.map_comp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map ((Opens.map s.snd.base).op.map (⋯.functor.op.map i) ≫ eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯ ≫ (Opens.map (pullback.lift s.fst.base s.snd.base ⋯)).op.map i)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑X)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.fst.c.app x

Tactic:
induction x with

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      (op x) =
    s.fst.c.app (op x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        Y.presheaf.map (eqToHom ⋯) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app (op x) =
    s.fst.c.app (op x)

Tactic:
← s.pt.presheaf.map_comp

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        Y.presheaf.map (eqToHom ⋯) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.adjunction.counit.app (unop x)).op ≫
        s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app x) =
    s.snd.c.app x

Tactic:
← s.pt.presheaf.map_comp

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ eqToHom ⋯ ≫ (eqToHom ⋯).app x) =
    s.snd.c.app x
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion ((pullbackSymmetry g f).hom ≫ pullback.snd f g)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsOpenImmersion ((pullbackSymmetry g f).hom ≫ pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U

Tactic:
· exact (X.basicOpen_le r).trans (f.preimage_image_eq _).ge

Goal state after:
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
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom
          (colimit.ι (F ⋙ forgetToPresheafedSpace) j ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
        x)
⊢ False

Tactic:
ι_preservesColimitIso_inv

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)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (forgetToPresheafedSpace.map (colimit.ι F j)).base) x)
⊢ False
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0

Tactic:
exact h i

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion ((pullbackSymmetry g f).hom ≫ pullback.snd f g)
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
X : (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ
⊢ Module ↑((structurePresheafInCommRingCat R ⋙ forget₂ CommRingCat RingCat).obj X)
    ↑((structurePresheafInModuleCat R M ⋙ forget₂ (ModuleCat R) Ab).obj X)

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ ∃ g,
    ∃ (_ : x ∈ basicOpen g) (i : basicOpen g ≤ U),
      ∃ f, const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map i.hom.op)) s

Tactic:
refine ⟨g' * g, ?_, ?_, g' • f, Subtype.ext <| funext fun ⟨y, hy⟩ ↦ ?_⟩

Goal state after:
case refine_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ x ∈ basicOpen (g' * g)

case refine_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
⊢ basicOpen (g' * g) ≤ U

case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ unop (op (basicOpen (g' * g)))
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map (LE.le.hom ?refine_2).op)) s) ⟨y, hy⟩
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_1
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩)

Tactic:
rw [affineBasisCover_map_range]

Goal state after:
case h_nhds.refine_1
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ a ∈ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ Set.range ⇑(X.affineBasisCover.f ⟨Cover.idx X.affineCover a, s⟩) ⊆ U

Tactic:
rw [affineBasisCover_map_range]

Goal state after:
case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) '' (PrimeSpectrum.basicOpen s).carrier ⊆ U
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
F : Sheaf CommRingCat X
⊢ ∀ (X_1 : (Opens ↑X)ᵒᵖ), Mono (F.presheaf.toTotalQuotientPresheaf.app X_1)

Tactic:
intro U

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Mono (F.presheaf.toTotalQuotientPresheaf.app U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ ∀ {X_1 Y : X.Opensᵒᵖ} (f : X_1 ⟶ Y),
    (X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map f ≫ (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom =
      (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom ≫ X.presheaf.map f

Tactic:
intro U

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U : X.Opensᵒᵖ
⊢ ∀ {Y : X.Opensᵒᵖ} (f : U ⟶ Y),
    (X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map f ≫ (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom =
      (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom ≫ X.presheaf.map f
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
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ t ≫ pullback.fst f V.ι ≫ f = pullback.fst f g ≫ f

Tactic:
pullback.lift_fst_assoc,

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
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (pullback.fst f g ≫ 𝟙 X) ≫ f = pullback.fst f g ≫ f
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)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ (Ideal.span (Set.range b)).radical

Tactic:
rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span,
      PrimeSpectrum.mem_vanishingIdeal]

Goal state after:
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)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus (Set.range b), f ∈ x.asIdeal
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)) ⋯
n : ℕ
hn : f ^ (n + 1) ∈ Submodule.span R (Set.range b)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s

Tactic:
Finsupp.mem_span_range_iff_exists_finsupp

Goal state after:
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)) ⋯
n : ℕ
hn : ∃ c, (c.sum fun i a ↦ a • b i) = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
i : (Scheme.coverOfIsIso (𝟙 X)).I₀
⊢ IsAffine ((Scheme.coverOfIsIso (𝟙 X)).X i)

Tactic:
dsimp; infer_instance

Goal state after:
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✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ equalizer.ι f g ≫ prod.lift f g = (equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)

Tactic:
by ext <;> simp [equalizer.condition f g]

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
x : ↑(PrimeSpectrum.Top R)
⊢ ∀ (U : Opens ↑(PrimeSpectrum.Top R)) (hxU : x ∈ U),
    (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
      (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)

Tactic:
intro U

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
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
⊢ ∀ (hxU : x ∈ U),
    (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
      (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
X Y✝ : C
f : X ⟶ Y✝
𝒰 : PreZeroHypercover Y✝
hR : 𝒰.presieve₀ ∈ K.coverings Y✝
x✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i) f
h :
  ∀ (i : { toPreZeroHypercover := 𝒰, mem₀ := hR }.I₀), P (pullback.snd f ({ toPreZeroHypercover := 𝒰, mem₀ := hR }.f i))
Y : C
i : 𝒰.I₀
hfg : HasPullback f (𝒰.f i)
⊢ P (pullback.snd f (𝒰.f i))

Tactic:
exact h i

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P.IsLocalAtSource K

Tactic:
refine .mk_of_iff fun {X Y} f R hR ↦ ?_
  rw [Precoverage.mem_iff_exists_zeroHypercover] at hR
  obtain ⟨𝒰, rfl⟩ := hR
  rw [H _ 𝒰]
  refine ⟨fun h U g ↦ ?_, fun h i ↦ h ⟨i⟩⟩
  rintro ⟨i⟩
  apply h

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (D.ι i)) y = x

Tactic:
delta CategoryTheory.GlueData.ι

Goal state after:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) y = x
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i)) ⁻¹' U)

Tactic:
delta CategoryTheory.GlueData.ι

Goal state after:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) ⁻¹' U)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i : D.J
⊢ IsIso (D.f' i i)

Tactic:
by simp only [↓reduceDIte, GlueData'.f']; infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
⊢ Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π

Tactic:
simp only [← comp_toShHom, s.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).inv ≫ pullback.fst 0 0 = prod.fst

Tactic:
by
  dsimp [pullbackZeroZeroIso]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).inv ≫ pullback.snd 0 0 = prod.snd

Tactic:
by
  dsimp [pullbackZeroZeroIso]
  simp

Goal state after: