mathlib-initiative/mathlib-tactics huggingface dataset:
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 :
  X.presheaf.map (⋯.adjunction.counit.app (unop (op (hf.functor.obj V)))).op ≫
      g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    (X.presheaf.map (⋯.adjunction.counit.app (unop (op (hf.functor.obj V)))).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)

Tactic:
Category.assoc,

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 :
  X.presheaf.map (⋯.adjunction.counit.app (unop (op (hf.functor.obj V)))).op ≫
      g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    X.presheaf.map (⋯.adjunction.counit.app (unop (op (hf.functor.obj V)))).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.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑R).germ ⊤ p trivial) ≫
      (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).hom.c

Tactic:
Category.assoc,

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat ↑R).germ ⊤ p trivial ≫
        (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).hom.c
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
Category.assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ app f U ≫ X.presheaf.map (homOfLE e).op ≫ X.presheaf.map i = 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:
Category.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 ≫ 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
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))) ≫ f.c.app (op ((opensFunctor f).obj U)) =
    X.presheaf.map (eqToHom ⋯)
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 =
    (Scheme.Hom.appIso g V).inv ≫
      (Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V)) ≫ Y.presheaf.map (eqToHom ⋯).op

Tactic:
Category.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.appIso g V).inv ≫
      Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
hy : y ∈ ↑U
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
this :
  IsIso
    (((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
        TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y) ≫
      inv (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y))
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.hom.base) y, ⋯⟩).map
      (have this := { hom := f.hom.c };
        this).hom)

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasLimits C
inst✝⁴ : HasColimits C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)
X Y : SheafedSpace C
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f.hom.base)
U : Opens ↑↑X.toPresheafedSpace
y : ↑↑X.toPresheafedSpace
H :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
hy : y ∈ ↑U
H' : IsIso (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
this :
  IsIso
    ((TopCat.Presheaf.stalkFunctor C ((ConcreteCategory.hom f.hom.base) y)).map f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y ≫
        inv (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y))
⊢ IsIso
    ((TopCat.Presheaf.stalkFunctor C ↑⟨(ConcreteCategory.hom f.hom.base) y, ⋯⟩).map
      (have this := { hom := f.hom.c };
        this).hom)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
have := Set.preimage_image_eq U.1 H.base_open.injective
          dsimp at this
          simp [Opens.map_def, this]

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✝¹ : R
x✝ : M
⊢ const (x✝¹ • x✝) 1 U ⋯ = (RingHom.id R) x✝¹ • const x✝ 1 U ⋯

Tactic:
by simp [smul_const]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ (X.homOfLE e₁ ≫ X.homOfLE e₂) ≫ W.ι = X.homOfLE ⋯ ≫ W.ι

Tactic:
Category.assoc,

Goal state after:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ ≫ W.ι = X.homOfLE ⋯ ≫ W.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
⊢ (X.homOfLE e).base = (Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e)

Tactic:
ext a; refine Subtype.ext ?_ -- Porting note: `ext` did not pick up `Subtype.ext`
  exact congr($(X.homOfLE_ι e) a)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      inv (X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
← Functor.map_inv,

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
Category.assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ 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.ι ⋯
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
by rw [Category.comp_id, Category.id_comp]

Goal state after:
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) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g

Tactic:
Category.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) ⋯ ⋯
⊢ ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g
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) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv ≫ g = pullback.snd f g ≫ g

Tactic:
Category.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) ⋯ ⋯
⊢ (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
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) ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g

Tactic:
Category.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) ⋯ ⋯
⊢ t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g
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
⊢ ((U.stalkIso ((resLE f U V e) x)).hom ≫ Y.presheaf.stalkSpecializes ⋯) ≫ stalkMap f ↑x =
    stalkMap (resLE f U V e) x ≫ (V.stalkIso x).hom

Tactic:
Category.assoc,

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
⊢ (U.stalkIso ((resLE f U V e) x)).hom ≫ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x =
    stalkMap (resLE f U V e) x ≫ (V.stalkIso x).hom
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
i : X.affineBasisCover.I₀
hxS : x ∈ Set.range ⇑(X.affineBasisCover.f i)
hSU : Set.range ⇑(X.affineBasisCover.f i) ⊆ ↑U
⊢ { carrier := Set.range ⇑(X.affineBasisCover.f i), is_open' := ⋯ } ∈ X.affineOpens

Tactic:
exact isAffineOpen_opensRange _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
hUV : V ≤ f ⁻¹ᵁ U
⊢ V.toSpecΓ ≫ Spec.map (Hom.appLE f U V hUV) = Hom.resLE f U V hUV ≫ U.toSpecΓ

Tactic:
by
  simp [Hom.appLE, Hom.resLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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

Tactic:
Opens.carrier_eq_coe

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ↑(basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
Category.assoc,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.isoSpec.inv ≫ U.ι ≫ X.toSpecΓ = Spec.map (X.presheaf.map (homOfLE ⋯).op)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
| (Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv) ≫ X.homOfLE ⋯ ≫ U.ι

Tactic:
Category.assoc,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
| Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑V).isoSpec.inv ≫ X.homOfLE ⋯ ≫ U.ι
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map f) ≫ (Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv) ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
Category.assoc,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map f) ≫ Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ 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:
Category.assoc,

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).ι ≫ f
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)
⊢ (ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).germ ⊤ x _root_.trivial) ≫
      stalkToLocalizationₗ R M x =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
Category.assoc,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.ofHom (toOpenₗ R M ⊤) ≫
      (structurePresheafInModuleCat R M).germ ⊤ x _root_.trivial ≫ stalkToLocalizationₗ R M x =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f) = PrimeSpectrum.basicOpen f

Tactic:
← basicOpen_eq_of_affine

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)
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)
⊢ localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x = 𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))

Tactic:
ext1
    refine IsLocalizedModule.ext x.asIdeal.primeCompl (LocalizedModule.mkLinearMap ..)
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap ..)) ?_
    ext
    dsimp [localizationtoStalkₗ]
    rw [← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply,
      elementwise_of% toStalkₗ'_stalkToFiberRingHom (M := M) x]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (CommRingCat.ofHom
          (algebraMap (↑(unop (op (CommRingCat.of R))))
            ((structureSheafInType ↑(unop (op (CommRingCat.of R))) ↑(unop (op (CommRingCat.of R)))).obj.obj (op ⊤))) ≫
        (structureSheaf ↑(unop (op (CommRingCat.of R)))).obj.map (homOfLE ⋯).op) ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app U =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
Category.assoc,

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ CommRingCat.ofHom
        (algebraMap (↑(unop (op (CommRingCat.of R))))
          ((structureSheafInType ↑(unop (op (CommRingCat.of R))) ↑(unop (op (CommRingCat.of R)))).obj.obj (op ⊤))) ≫
      (structureSheaf ↑(unop (op (CommRingCat.of R)))).obj.map (homOfLE ⋯).op ≫
        ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app U =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
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.snd (D.f i j) (D.f i i)) ≫ D.f i i = 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.snd (D.f i j) (D.f i i) ≫ D.f i i = 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.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom

Tactic:
by
  have eq₁ := D.t_fac i i j
  have eq₂ := (IsIso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _)
  rw [D.t_id, Category.comp_id, eq₂] at eq₁
  have eq₃ := (IsIso.eq_comp_inv (D.f i i)).mp eq₁
  rw [Category.assoc, ← pullback.condition, ← Category.assoc] at eq₃
  exact
    Mono.right_cancellation _ _
      ((Mono.right_cancellation _ _ eq₃).trans (pullbackSymmetry_hom_comp_fst _ _).symm)

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
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
have eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom =
      pullback.snd _ _ ≫ inv (pullback.fst _ _) := by simp
  have := D.cocycle i j i
  rw [D.t'_iij, D.t'_jii, D.t'_iji, fst_eq_snd_of_mono_eq, eq] at this
  simp only [Category.assoc, IsIso.inv_hom_id_assoc] at this
  rw [← IsIso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq] at this
  simpa using this

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq : (ConcreteCategory.hom ((D.mapGlueData F).ι i ≫ e.inv)) y = (ConcreteCategory.hom (𝟙 (F.obj D.glued))) x
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x

Tactic:
D.ι_gluedIso_inv

Goal state after:
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq : (ConcreteCategory.hom (F.map (D.ι i))) y = (ConcreteCategory.hom (𝟙 (F.obj D.glued))) x
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x