mathlib-initiative/mathlib-tactics huggingface dataset:
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
j : J
⊢ (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j

Tactic:
ext U

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
j : J
U : ↑↑(F.obj j)
⊢ (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ desc F s).base) U = (ConcreteCategory.hom (s.ι.app j).base) U

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
j : J
U : Opens ↑↑s.pt
⊢ (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ locallyRingedSpaceMap (g.unop ≫ f.unop) = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop

Tactic:
rw [Spec.locallyRingedSpaceMap_comp]

Goal state after:
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
x : (Opens ↑↑Y)ᵒᵖ
⊢ (((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c ≫
          𝟙 ((Opens.map ((isoRestrict f).hom ≫ Y.ofRestrict ⋯).base).op ⋙ X.presheaf)).app
      x =
    f.c.app x

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ ((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c.app x = f.c.app x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
induction V

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ appLE f U V e ≫ (appIso f V).inv = Y.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [appLE, Category.assoc, appIso_inv_naturality, Functor.op_obj, Functor.op_map,
    Quiver.Hom.unop_op, opensFunctor_map_homOfLE, app_appIso_inv_assoc, Opens.carrier_eq_coe]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ Y.presheaf.map (homOfLE ⋯).op = Y.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
rw [← IsIso.comp_inv_eq] at this

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
this :
  (f.c.app (op ((opensFunctor f).obj x)) ≫ s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x)))) ≫
      inv (s.pt.presheaf.map (eqToHom ⋯)) =
    g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x)))
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
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
  simp only [pretopology_toPrecoverage, precoverage_inf]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
by
  rw [isIso_iff_isOpenImmersion_and_epi_base,
    IsOpenImmersion.iff_isIso_stalkMap, and_comm, ← and_assoc]
  refine and_congr ⟨?_, ?_⟩ Iff.rfl
  · rintro ⟨h₁, h₂⟩
    convert_to!
      IsIso
        (TopCat.isoOfHomeo
          (Equiv.toHomeomorphOfContinuousOpen
            (.ofBijective _ ⟨h₂.injective, (TopCat.epi_iff_surjective _).mp h₁⟩) h₂.continuous
            h₂.isOpenMap)).hom
    infer_instance
  · intro H; exact ⟨inferInstance, (TopCat.homeoOfIso (asIso f.base)).isOpenEmbedding⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Epi f.base

Tactic:
rw [TopCat.epi_iff_surjective, ← Set.range_eq_univ]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Set.range ⇑f = Set.univ
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ fn i = 0
this : Fintype 𝒰.I₀
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) (s ^ N) = 0

Tactic:
simp only [map_pow]

Goal state after:
case h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ fn i = 0
this : Fintype 𝒰.I₀
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ N = 0
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 M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
hb : b ∈ {f | (isLocallyFraction R M).pred f}
x : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x ∈ Va
ia : Va ⟶ U
ra : M
sa : R
wa : ∀ (x : ↥Va), ∃ (hs : sa ∉ (↑x).asIdeal), (fun x ↦ a (ia x)) x = LocalizedModule.mk ra ⟨sa, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (a + b) (i x)

Tactic:
obtain ⟨Vb, mb, ib, rb, sb, wb⟩ := hb x

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
hb : b ∈ {f | (isLocallyFraction R M).pred f}
x : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x ∈ Va
ia : Va ⟶ U
ra : M
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 : M
sb : R
wb : ∀ (x : ↥Vb), ∃ (hs : sb ∉ (↑x).asIdeal), (fun x ↦ b (ib x)) x = LocalizedModule.mk rb ⟨sb, hs⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (a + b) (i x)
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⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R A).pred fun x ↦ (a * b) (i x)

Tactic:
obtain ⟨Vb, mb, ib, rb, sb, wb⟩ := hb x

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
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⟩
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R A).pred fun x ↦ (a * b) (i x)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (F.presheaf.toTotalQuotientPresheaf.app U))

Tactic:
dsimp [toTotalQuotientPresheaf]

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).toLocalizationPresheaf.app U))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι ≫ 𝟙 X = 𝟙 ↑(𝟙 X ⁻¹ᵁ U) ≫ U.ι

Tactic:
Category.comp_id,

Goal state after:
X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = 𝟙 ↑(𝟙 X ⁻¹ᵁ U) ≫ U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ 𝟙 X ∣_ U = 𝟙 ↑(𝟙 X ⁻¹ᵁ U)

Tactic:
rw [← cancel_mono U.ι, morphismRestrict_ι, Category.comp_id, Category.id_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : Opens ↥↑V
⊢ X.homOfLE e ∣_ W ≫ (Scheme.Hom.isoImage V.ι W).hom = (Scheme.Hom.isoImage U.ι (X.homOfLE e ⁻¹ᵁ W)).hom ≫ X.homOfLE ⋯

Tactic:
simp [← cancel_mono (V.ι ''ᵁ W).ι]

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.ι ⋯
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
Category.comp_id,

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.ι ⋯
⊢ f = 𝟙 X ≫ 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.ι ⋯
⊢ g ≫ 𝟙 Y = e.hom ≫ V.ι

Tactic:
Category.comp_id,

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.ι ⋯
⊢ g = e.hom ≫ V.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
⊢ W ≤ resLE f U V e ⁻¹ᵁ O ↔ V.ι ''ᵁ W ≤ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
by
  simp [resLE_preimage, ← image_le_image_iff V.ι, image_preimage_eq_opensRange_inf, V.ι_image_le]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e_6
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (U.stalkIso x).inv) (closedPoint ↑((↑U).presheaf.stalk x)) = closedPoint ↑(X.presheaf.stalk ↑x)

Tactic:
exact IsLocalRing.comap_closedPoint (U.stalkIso x).inv.hom

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom (openToLocalizationₗ R M U x hxU ≫ localizationtoStalkₗ R M x)) s =
    (ModuleCat.Hom.hom
        ((structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)))
      s

Tactic:
Category.comp_id,

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ModuleCat.Hom.hom (openToLocalizationₗ R M U x hxU ≫ localizationtoStalkₗ R M x)) s =
    (ModuleCat.Hom.hom ((structurePresheafInModuleCat R M).germ U x hxU)) s
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.fst (D.f i i) (D.f i j) ≫ 𝟙 (D.V (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)
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom

Tactic:
Category.comp_id,

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.fst (D.f i i) (D.f i j)
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)
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
⊢ s ∈ I

Tactic:
let (x : _) : Algebra Γ(X, U) (X.presheaf.stalk (hU.fromSpec x)) :=
    TopCat.Presheaf.algebra_section_stalk X.presheaf _

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
⊢ s ∈ I
Module: Mathlib.Topology.Gluing

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

Tactic:
rw [← (homeoOfIso (Multicoequalizer.isoCoequalizer 𝖣.diagram).symm).isOpen_preimage]

Goal state after:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen (⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case e
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ ↾⇑(ConcreteCategory.hom f.base) ≫ ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) =
    ↾⇑(ConcreteCategory.hom g.base) ≫ ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base)

Tactic:
ext
    simp only [TypeCat.Fun.toFun_apply, comp_apply, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, ← TopCat.comp_app, ← PresheafedSpace.comp_base]
    congr 3
    exact SheafedSpace.forgetToPresheafedSpace.congr_map
      (coequalizer.condition f.toShHom g.toShHom)

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✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).snd i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)

Tactic:
sigmaIsoSigma_hom_ι_apply,

Goal state after:
case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel ⟨(MultispanShape.prod D.J).fst { as := (i, j) }.as, (D.diagram.fst { as := (i, j) }.as).hom' y⟩
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).snd i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ ↑U

Tactic:
← hU.fromSpec_preimage_zeroLocus,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec '' ⇑hU.fromSpec ⁻¹' X.zeroLocus s = X.zeroLocus s ∩ ↑U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : (ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩ ∈ U j
⊢ (ofOpenSubsets U).Rel ⟨i, ⟨x, hx⟩⟩ ⟨j, ⟨(ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩, hy⟩⟩

Tactic:
exact ⟨⟨⟨x, hx⟩, hy⟩, rfl, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
Category.comp_id,

Goal state after:
case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g = 𝟙 Y ≫ g
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₀
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i

Tactic:
have : HasPullback (pullback.snd _ _ ≫ 𝒰.f i ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f j) (𝒰.f i) (𝒰.f i ≫ f) g
  have : HasPullback (pullback.snd _ _ ≫ 𝒰.f j ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f i) (𝒰.f j) (𝒰.f j ≫ f) g
  refine (pullbackSymmetry ..).hom ≫ (pullbackAssoc ..).inv ≫ ?_
  refine ?_ ≫ (pullbackAssoc ..).hom ≫ (pullbackSymmetry ..).hom
  refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_
  · rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]
  · rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
Category.comp_id,

Goal state after:
case refine_1
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i = t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ 𝒰.f k ≫ 𝟙 X = 𝟙 (𝒰.X k) ≫ 𝒰.f k

Tactic:
Category.comp_id,

Goal state after:
case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ 𝒰.f k = 𝟙 (𝒰.X k) ≫ 𝒰.f k
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 k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.fst (𝒰.f i ≫ f) g =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
simp only [pullback.condition_assoc, t'_snd_fst_fst, t'_fst_snd, t'_snd_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
⊢ (Disjoint on fun x ↦ Set.range ⇑(U x).ι) i j

Tactic:
convert hU' e; simp [← Opens.coe_disjoint]

Goal state after: