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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      CommRingCat.ofHom
          (comap (CommRingCat.Hom.hom f) (unop (op ⊤)) ((TopologicalSpace.Opens.map (Spec.topMap f)).obj (unop (op ⊤)))
            ⋯) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial

Tactic:
toOpen_comp_comap_assoc

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      CommRingCat.ofHom
          (algebraMap ↑S
            ↑((structureSheaf ↑S).obj.obj
                (op
                  ((TopologicalSpace.Opens.comap
                      { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                    ⊤)))) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ app f U ≫ X.presheaf.map (homOfLE e).op = appLE f U' V ⋯

Tactic:
f.naturality_assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ app f U' ≫ X.presheaf.map ((Opens.map f.base).map i.unop).op ≫ X.presheaf.map (homOfLE e).op = appLE f U' V ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ app g U ≫ Y.presheaf.map (homOfLE e₁).op ≫ app f V ≫ X.presheaf.map (homOfLE e₂).op =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
f.naturality_assoc,

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ app g U ≫
      app f (g ⁻¹ᵁ U) ≫
        X.presheaf.map ((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ X.presheaf.map (homOfLE e₂).op =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) W = eqToHom ⋯

Tactic:
refine (Scheme.Hom.congr_app this _).trans ?_

Goal state after:
case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫ (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (eqToHom ⋯).op = eqToHom ⋯
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (opensFunctor f).IsCocontinuous (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)

Tactic:
f.opensFunctorAdjunction.isCocontinuous_iff_coverPreserving

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ CoverPreserving (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X) (Opens.map f.base)
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
⊢ ∃ a, (pullback.snd f g) a = y

Tactic:
let iso := pullbackSymmetry f g

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
⊢ ∃ a, (pullback.snd f g) a = y
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X : Scheme
inst✝ : JointlySurjective K
𝒰 : Cover K X
x : ↥X
Y : Scheme
i : 𝒰.I₀
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = x
⊢ ∃ i y, (𝒰.f i) y = x

Tactic:
use i, y

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace C
Y : SheafedSpace C
f : X ⟶ Y.toPresheafedSpace
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (Y.restrict ⋯).presheaf.IsSheaf

Tactic:
exact (Y.restrict H.base_open).IsSheaf

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

Goal state before:
pp: K : Precoverage Scheme
X✝ Y✝ Z : Scheme
𝒰 : Cover K X✝
f : X✝ ⟶ Z
g✝ : Y✝ ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g✝
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : ∀ (x : forget.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map f))
right✝ : R ∈ P.precoverage.coverings X
Y : Scheme
g : Y ⟶ X
hg : R g
heq : x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map g))
⊢ ∃ Y g, R g ∧ x ∈ Set.range ⇑g

Tactic:
use Y, g, hg

Goal state after:
case right
K : Precoverage Scheme
X✝ Y✝ Z : Scheme
𝒰 : Cover K X✝
f : X✝ ⟶ Z
g✝ : Y✝ ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g✝
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : ∀ (x : forget.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map f))
right✝ : R ∈ P.precoverage.coverings X
Y : Scheme
g : Y ⟶ X
hg : R g
heq : x ∈ Set.range ⇑(ConcreteCategory.hom (forget.map g))
⊢ x ∈ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      ⇑(ConcreteCategory.hom (pullback.snd g.base f.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
erw [TopCat.pullback_fst_image_snd_preimage]
    rw [Set.image_univ]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ (Scheme.Hom.opensRange f).carrier ∩ Set.range ⇑g = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
Opens.carrier_eq_coe,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ↑(Scheme.Hom.opensRange f) ∩ Set.range ⇑g = Set.range ⇑f ∩ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑g ∩ (Scheme.Hom.opensRange f).carrier = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
Opens.carrier_eq_coe,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑g ∩ ↑(Scheme.Hom.opensRange f) = Set.range ⇑g ∩ Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = U.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op

Tactic:
f.naturality_assoc,

Goal state after:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V =
    Scheme.Hom.app f V ≫ Y.presheaf.map ((Opens.map f.base).map (eqToHom ⋯).op.unop).op ≫ Y.presheaf.map (eqToHom ⋯).op
Module: Mathlib.CategoryTheory.Comma.Over.OverClass

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ autoParam (f ≫ Y ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam

Tactic:
← comp_over (Y ↘ S),

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ autoParam (f ≫ Y ↘ S ≫ S ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
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
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⟩
Vb : Opens ↑(PrimeSpectrum.Top R)
mb : ↑x✝ ∈ Vb
ib : Vb ⟶ U
rb : A
sb : R
wb : ∀ (x : ↥Vb), ∃ (hs : sb ∉ (↑x).asIdeal), (fun x ↦ b (ib x)) x = LocalizedModule.mk rb ⟨sb, hs⟩
x : ↥(Va ⊓ Vb)
hsax : sa ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsa : (fun x ↦ a (ia x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk ra ⟨sa, hsax⟩
hsbx : sb ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsb : (fun x ↦ b (ib x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk rb ⟨sb, hsbx⟩
⊢ ∃ (hs : sa * sb ∉ (↑x).asIdeal),
    (fun x ↦ (a * b) ((Va.infLELeft Vb ≫ ia) x)) x = LocalizedModule.mk (ra * rb) ⟨sa * sb, hs⟩

Tactic:
exact ⟨x.1.asIdeal.primeCompl.mul_mem hsax hsbx,
      congr($hsa * $hsb).trans (LocalizedModule.mk_mul_mk ..)⟩

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)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ const (g i • f j) (g i * g j) (basicOpen (g i * g j)) ⋯ = const (g j • f i) (g i * g j) (basicOpen (g i * g j)) ⋯

Tactic:
trans (structureSheafInType R M).obj.map (homOfLE ?_).op s

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ const (g i • f j) (g i * g j) (basicOpen (g i * g j)) ⋯ =
    (ConcreteCategory.hom ((structureSheafInType R M).obj.map (homOfLE ?m.192).op)) s

R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ (ConcreteCategory.hom ((structureSheafInType R M).obj.map (homOfLE ?m.192).op)) s =
    const (g j • f i) (g i * g j) (basicOpen (g i * g j)) ⋯

R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ basicOpen (g i * g j) ≤ 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 V i
      dsimp
      rw [X.homOfLE_appTop, ← Functor.map_comp, ← Functor.map_comp]
      congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ ((↑U).toSpecΓ ≫ Spec.map U.topIso.inv) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) = U.ι ≫ X.toSpecΓ

Tactic:
simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, (basicOpen i).carrierᶜ

Tactic:
Opens.carrier_eq_coe,

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, (↑(basicOpen i))ᶜ
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
        { hom := (Spec.sheafedSpaceMap f).hom }.hom.c.app (op U) ≫
          { hom := X.toΓSpecSheafedSpace.hom }.hom.c.app
            (op ((Opens.map { hom := (Spec.sheafedSpaceMap f).hom }.hom.base).obj (unop (op U))))) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
toOpen_comp_comap_assoc

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CommRingCat.ofHom
            (algebraMap ↑(Γ.obj (op X))
              ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          { hom := X.toΓSpecSheafedSpace.hom }.hom.c.app
            (op ((Opens.map { hom := (Spec.sheafedSpaceMap f).hom }.hom.base).obj (unop (op U))))) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)
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
this : IsAffine ↑U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ Spec.map (Y.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ X.homOfLE i ≫ (f ⁻¹ᵁ U).ι ≫ f

Tactic:
← morphismRestrict_ι,

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) ≫ Spec.map (Y.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ X.homOfLE i ≫ f ∣_ U ≫ U.ι
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
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
r : R
m : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ ↑⟨comapFun f U V hUV ↑(r • m), ⋯⟩ x✝ = ↑(σ r • ⟨comapFun f U V hUV ↑m, ⋯⟩) x✝

Tactic:
dsimp [comapFun]
    rw [map_smulₛₗ, ← IsScalarTower.algebraMap_smul S]

Goal state after:
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 j k : D.J
hij : i = j
⊢ IsIso (D.f' i j)

Tactic:
simp only [GlueData'.f', dif_pos hij]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : i = j
⊢ IsIso (eqToHom ⋯)
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 j k : D.J
hij : ¬i = j
hik : ¬i = k
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]

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:
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:
dsimp [pullbackZeroZeroIso]
  simp

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
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
this : IsOpenImmersion α
⊢ α y = x

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map, Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.comp_apply] at hy₁

Goal state after:
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
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom (↾⇑(F.map hli))) y =
    (TopCat.Hom.hom (Hom.isoOpensRange (F.map k₁.snd.1)).inv.base)
      ((TopCat.Hom.hom (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).base) x)
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
this : IsOpenImmersion α
⊢ α y = x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))

Tactic:
have := Scheme.Hom.stalkMap_comp coprod.inl (coprodSpec R S) x

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this :
  Scheme.Hom.stalkMap (coprod.inl ≫ coprodSpec R S) x =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x) ≫ Scheme.Hom.stalkMap coprod.inl x
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case H.mp
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
x y : (a : ι) → R a
⊢ (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y →
    Function.update 0 i 1 * x = Function.update 0 i 1 * y

Tactic:
intro e; ext j; by_cases h : j = i <;> aesop

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

Goal state before:
pp: case inl
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit))

Tactic:
← MorphismProperty.cancel_left_of_respectsIso P
      (isPullback_inl_inl_coprodMap f g).flip.isoPullback.hom

Goal state after:
case inl
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
hf : P f
hg : P g
⊢ P (⋯.isoPullback.hom ≫ Scheme.Cover.pullbackHom (coprodOpenCover X' Y') (coprod.map f g) (Sum.inl PUnit.unit))