mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
⊢ Sheaf.pullback A f ≅ sheafPullback A hf

Tactic:
by
  refine Sheaf.pullbackIso A f ≪≫ NatIso.ofComponents (fun F ↦ ?_) (fun u ↦ ?_)
  · exact (presheafToSheaf (Opens.grothendieckTopology ↑X) A).mapIso
      (hf.isOpenMap.pullbackIso.app _) ≪≫
      (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology X) A).preimageIso
      (isoSheafify (Opens.grothendieckTopology X)
      (TopCat.Presheaf.isSheaf_of_isOpenEmbedding hf F.2)).symm
  · dsimp
    rw [← Functor.map_comp_assoc, hf.isOpenMap.pullbackIso.hom.naturality, Sheaf.hom_ext_iff]
    simp only [Functor.whiskeringLeft_obj_obj, Functor.whiskeringLeft_obj_map, Functor.map_comp,
      isoSheafify_inv, Category.assoc]
    rw [ObjectProperty.FullSubcategory.comp_hom, ObjectProperty.FullSubcategory.comp_hom,
      ObjectProperty.FullSubcategory.comp_hom, ObjectProperty.FullSubcategory.comp_hom]
    dsimp [sheafPullback, Functor.sheafPushforwardContinuous, Sheaf.forget]
    simp only [sheafifyMap_sheafifyLift, Category.comp_id, sheafifyMap_sheafifyLift_assoc]
    rw [CategoryTheory.sheafifyLift_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Hom.stalkMap β x'

Tactic:
ext
  subst h₁ h₂
  simp

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

Goal state before:
pp: case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
V : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
simpa using hv4

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

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
⊢ s.pt.presheaf.obj U ⟶
    ((pushforward C (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj
          (limit (pushforwardDiagramToColimit F).leftOp)).obj
      U

Tactic:
refine
    limit.lift _
        { pt := s.pt.presheaf.obj U
          π :=
            { app := fun j => ?_
              naturality := fun j j' f => ?_ } } ≫
      (limitObjIsoLimitCompEvaluation _ _).inv
  -- We still need to construct the `app` and `naturality'` fields omitted above.
  · refine (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ?_)
    dsimp
    rw [← Opens.map_comp_obj]
    simp
  · dsimp
    rw [PresheafedSpace.congr_app (s.w f.unop).symm U]
    have w :=
      Functor.congr_obj
        (congr_arg Opens.map (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j)))
        (unop U)
    simp only [Opens.map_comp_obj_unop] at w
    replace w := congr_arg op w
    have w' := NatTrans.congr (F.map f.unop).c w
    rw [w']
    simp

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
h : P.pred f
x : ↥U
⊢ P.pred fun x ↦ f ((𝟙 U) x)

Tactic:
by convert! h

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case h
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥↑U) → T ↑y
h : P.pred f
⊢ (ConcreteCategory.hom (stalkToFiber P x))
      ((ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑U) x ⋯)) ⟨f, h⟩) =
    f ⟨x, ⋯⟩

Tactic:
· exact stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case w
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.base = (𝟙 (sheafedSpaceObj R)).hom.base

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

Tactic:
· exact Spec.topMap_id R

Goal state after:
case h
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf =
    (𝟙 (sheafedSpaceObj R)).hom.c
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ (Y.presheaf.stalkCongr ⋯).hom ≫ (Arrow.mk (stalkMap f y)).hom =
    (Arrow.mk (stalkMap f x)).hom ≫ (X.presheaf.stalkCongr ⋯).hom

Tactic:
simp only [Arrow.mk_left, Arrow.mk_right, TopCat.Presheaf.stalkCongr_hom,
      Arrow.mk_hom]

Goal state after:
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f y = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
hf✝ :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom.base)
⊢ ∀ (x : ↥(Spec (CommRingCat.of (Localization.Away f)))),
    IsIso
      (PresheafedSpace.Hom.stalkMap
        (LocallyRingedSpace.Hom.toShHom
            (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom
        x)

Tactic:
intro x
    exact isIso_SpecMap_stakMap_localization R (Submonoid.powers f) x

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

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
              TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
                (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
← Category.assoc

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        ((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
                TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as) ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))
Module: Mathlib.AlgebraicGeometry.Cover.Open

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

Tactic:
by
  fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ (𝒰.f (𝒰.idx i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)
  · intro x hx
    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.mem_mk,
      Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
    refine ⟨?_, hx⟩
    simpa using ⟨_, 𝒰.covers x⟩
  · intro x
    replace h := h (𝒰.idx x)
    rw [← IsOpenImmersion.map_ΓIso_inv] at h
    exact (IsOpenImmersion.ΓIso (𝒰.f (𝒰.idx x)) U).commRingCatIsoToRingEquiv.symm.injective h

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ * (f * g₁) = g₁ * g₂ * f

Tactic:
ring

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
U : Opens ↑(PrimeSpectrum.Top R)
x✝¹ x✝ : M
⊢ const (x✝¹ + x✝) 1 U ⋯ = const x✝¹ 1 U ⋯ + const x✝ 1 U ⋯

Tactic:
by simp [const_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)

Tactic:
refine (Scheme.image_basicOpen (X.ofRestrict U.isOpenEmbedding) r).trans ?_

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r)
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}
⊢ ∃ u, u • d • a = u • b • c

Tactic:
exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
W' : (↑U).Opens
e' : W' ≤ X.homOfLE e ⁻¹ᵁ W
⊢ Hom.appLE (X.homOfLE e) W W' e' = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp [Scheme.Hom.appLE, Scheme.homOfLE_app, ← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
← Category.assoc

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.snd g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.snd g (Scheme.Opens.ι U)
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 ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (pullback.snd f g)).hom ≫ e.hom

Tactic:
← Iso.comp_inv_eq,

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) ⋯ ⋯
⊢ ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom) ≫ e.inv =
    (Arrow.mk (pullback.snd f g)).hom
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x =
    ((U.stalkIso ((resLE f U V e) x)).inv ≫ stalkMap (resLE f U V e) x) ≫ (V.stalkIso x).hom

Tactic:
← Iso.comp_inv_eq,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ (V.stalkIso x).inv =
    (U.stalkIso ((resLE f U V e) x)).inv ≫ stalkMap (resLE f U V e) x
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom
        (toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ≫
          PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))
      r)

Tactic:
CommRingCat.comp_apply

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))
      ((ConcreteCategory.hom
          (toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x)))
        r))
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)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx =
    ModuleCat.ofHom (toOpenₗ R M ⊤) ≫
      (structurePresheafInModuleCat R M).map (homOfLE ⋯).op ≫ (structurePresheafInModuleCat R M).germ U x hx

Tactic:
← Category.assoc

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx =
    (ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).map (homOfLE ⋯).op) ≫
      (structurePresheafInModuleCat R M).germ U x hx
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:
← Category.assoc

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 =
    (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)))))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (localizationtoStalkₗ R M x)) (LocalizedModule.mk f s) =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯)) (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
apply ((Module.End.isUnit_iff _).mp (isUnit_toStalkₗ' _ s.1 s.2)).1 ?_
  dsimp [localizationtoStalkₗ]
  rw [← map_smul, LocalizedModule.smul'_mk, ← Submonoid.smul_def, LocalizedModule.mk_cancel,
    ← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply, ← map_smul,
    ← toOpenₗ_germ (basicOpen ↑s) _ s.2, smul_const]
  dsimp [toOpenₗ]
  congr 1
  exact const_eq_const_of_smul_eq_smul (H := by simp) ..

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
R : CommRingCat
⊢ ∀ (r : ↑(unop (op ((𝟭 CommRingCat).obj R)))),
    (SpecΓIdentity.inv.app R).op.unop ≫
        ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom
          (algebraMap (↑(unop (op ((𝟭 CommRingCat).obj R))))
            ((structureSheafInType ↑(unop (op ((𝟭 CommRingCat).obj R))) ↑(unop (op ((𝟭 CommRingCat).obj R)))).obj.obj
              (op (basicOpen r)))) ≫
        (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).c.app (op (basicOpen r))

Tactic:
· intro r; rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₃ : D.t' i i j ≫ pullback.fst (D.f i j) (D.f i i) ≫ D.f i j = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom

Tactic:
← Category.assoc

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₃ : (D.t' i i j ≫ pullback.fst (D.f i j) (D.f i i)) ≫ D.f i j = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h
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
⊢ (Localizations.comapFun f.toSemilinearMap ↑p) (LocalizedModule.mk m s) =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (LocalizedModule.mk m s)

Tactic:
trans LocalizedModule.mk (f m) ⟨f ↑s, s.2⟩
  · simp
  convert_to! Localization.mk _ _ = Localization.localRingHom _ _ _ _ (Localization.mk _ _)
  simp [Localization.mk_eq_mk']

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) x =
      (ConcreteCategory.hom (Multicoequalizer.π D.diagram j)) y →
    D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ]

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
      (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y →
    D.Rel ⟨i, x⟩ ⟨j, y⟩
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Spec.homEquiv (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) ≫ φ =
    Spec.homEquiv (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom) ≫ φ

Tactic:
← Spec.map_injective.eq_iff

Goal state after:
case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Spec.map (Spec.homEquiv (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) ≫ φ) =
    Spec.map (Spec.homEquiv (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom) ≫ φ)