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

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom = 𝟙 Y

Tactic:
ext : 1

Goal state after:
X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom).toHom = (𝟙 Y).toHom
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
h : x ∈ U
h✝ : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x h)) f)
⊢ x ∈ U

Tactic:
exact h

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
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
⊢ m = desc F s

Tactic:
ext : 1

Goal state after:
case w
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
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
⊢ m.base = (desc F s).base

case h
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
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
⊢ m.c ≫ whiskerRight (eqToHom ⋯) (colimitCocone F).pt.presheaf = (desc F s).c
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
⊢ sheafedSpaceMap (𝟙 R) = 𝟙 (sheafedSpaceObj R)

Tactic:
ext : 1

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

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

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

Tactic:
ext : 1

Goal state after:
case w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base

case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α = β

Tactic:
ext : 1

Goal state after:
case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.base = β.hom.base

case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.toHom = toLRSHom'✝.toHom

Tactic:
ext : 1

Goal state after:
case mk.mk.w
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.base = toLRSHom'✝.base

case h
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
have (x : X) : ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U := fun _ _ h ↦ X.basicOpen_le _ h
  simpa [codisjoint_iff_le_sup, Set.ext_iff, or_iff_not_imp_left]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ f ''ᵁ ⨆ i, s i = ⨆ i, f ''ᵁ s i

Tactic:
ext : 1

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ ↑(f ''ᵁ ⨆ i, s i) = ↑(⨆ i, f ''ᵁ s i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ f ''ᵁ ⨆ i, ⨆ j, s i j = ⨆ i, ⨆ j, f ''ᵁ s i j

Tactic:
ext : 1

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ ↑(f ''ᵁ ⨆ i, ⨆ j, s i j) = ↑(⨆ i, ⨆ j, f ''ᵁ s i j)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : X.Opens
⊢ appIso (f ≫ g) U = Functor.mapIso Z.presheaf (eqToIso ⋯).op ≪≫ appIso g (f ''ᵁ U) ≪≫ appIso f U

Tactic:
ext : 1

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : X.Opens
⊢ (appIso (f ≫ g) U).hom = (Functor.mapIso Z.presheaf (eqToIso ⋯).op ≪≫ appIso g (f ''ᵁ U) ≪≫ appIso f U).hom
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.IsMultiplicative
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : Q.IsMultiplicative
inst✝ : Q.IsStableUnderBaseChange
⊢ (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology

Tactic:
ext : 1

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.IsMultiplicative
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : Q.IsMultiplicative
inst✝ : Q.IsStableUnderBaseChange
⊢ (P ⊓ Q).pretopology.coverings = (P.pretopology ⊓ Q.pretopology).coverings
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
⊢ ∀ (S : Scheme) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)

Tactic:
Z

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
⊢ ∀ (f : X ⟶ Z) (g : Y ⟶ Z) [inst : HasPullback f g], IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)
Module: Mathlib.Topology.Sheaves.CommRingCat

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

Tactic:
ext : 1

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ CommRingCat.Hom.hom
      (ConcreteCategory.ofHom
        (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map i ≫ F.map j)) ⋯)) =
    CommRingCat.Hom.hom
      (ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
        ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯))
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)
this : f ∈ (⊥.colon {d • a - b • c}).radical
⊢ LocalizedModule.mk a b = LocalizedModule.mk c d

Tactic:
LocalizedModule.mk_eq

Goal state after:
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)
this : f ∈ (⊥.colon {d • a - b • c}).radical
⊢ ∃ u, u • d • a = u • b • c
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝¹ x✝ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
⊢ (x✝¹ + x✝) ≫ (forget₂ TopCommRingCat TopCat).map φ =
    x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ + x✝ ≫ (forget₂ TopCommRingCat TopCat).map φ

Tactic:
by ext; exact φ.1.map_add _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ Hom.appTop (X.homOfLE ⋯) ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map i

Tactic:
rw [X.homOfLE_appTop, ← Functor.map_comp, ← Functor.map_comp]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map ((eqToHom ⋯).op ≫ i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ IsIso (f ∣_ U)

Tactic:
by
  delta morphismRestrict; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsUnit ((ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r)

Tactic:
by
  convert!
    (X.presheaf.map <| (eqToHom <| X.toΓSpecMapBasicOpen_eq r).op).hom.isUnit_map
      (X.toRingedSpace.isUnit_res_basicOpen r)
  rw [← CommRingCat.comp_apply, ← Functor.map_comp]
  congr

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
h :
  ConcreteCategory.hom
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
        f) =
    (IsLocalization.Away.lift r ⋯).comp
      (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r))))
⊢ f = X.toΓSpecCApp r

Tactic:
ext : 1

Goal state after:
case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
h :
  ConcreteCategory.hom
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
        f) =
    (IsLocalization.Away.lift r ⋯).comp
      (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r))))
⊢ CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.Γgerm x

Tactic:
Γgerm,

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.germ ⊤ x True.intro
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.fst ≫ g

Tactic:
have H₁ : s.fst ≫ f = s.snd := by simpa using congr($s.condition ≫ prod.fst)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ f = s.fst ≫ g
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
        (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)

Tactic:
ext : 1

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := ⋯
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) := ⋯
⊢ CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
          (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r))
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)
X Y✝ : C
f : X ⟶ Y✝
𝒰 : K.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Y : C
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
apply h

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
ext : 1

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
            (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (eqToHom ⋯).op)
Module: Mathlib.CategoryTheory.GlueData

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

Tactic:
trans inv (D.t' i j k)
  · exact IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)
  · rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]
    simp [t_fac, t_fac_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : f x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g) = 0 →
      (ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g = 0
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, hx⟩) := ⋯
⊢ ∀ (x_1 : ↑Γ(Y, U)),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨f x, hx⟩)) x_1) = 0 →
      (algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨f x, hx⟩)) x_1 = 0

Tactic:
exact h

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

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

Tactic:
induction m using LocalizedModule.induction_on with | h m s =>
  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.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⋃ i, ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i) = ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier

Tactic:
refine congr_arg (Set.iUnion ·) ?_

Goal state after:
case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ (fun i ↦ ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i)) = fun i ↦ (PrimeSpectrum.basicOpen ↑i).carrier
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom x))
      ((ConcreteCategory.hom
          ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
            ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
        s))
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)

Tactic:
rw [PresheafedSpace.stalkMap_germ_apply (coequalizer.π f.toShHom g.toShHom).hom U _ hU] at ha

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)
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 : C
⊢ (prodZeroIso X).inv ≫ prod.fst = 𝟙 X

Tactic:
dsimp [prodZeroIso, binaryFanZeroRight]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
⊢ t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
by
  simp only [t, Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackAssoc_hom_snd_fst,
    pullback.lift_fst_assoc, pullbackSymmetry_hom_comp_snd, pullbackAssoc_inv_fst_fst,
    pullbackSymmetry_hom_comp_fst]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y

Tactic:
let e :=
    (TopCat.pullbackConeIsLimit _ _).conePointUniqueUpToIso
      (isLimitOfHasPullbackOfPreservesLimit Scheme.forgetToTop (𝒰.f i) (𝒰.f j))

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y