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

Goal state before:
pp: case φ
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
⊢ (colimit.cocone (F ⋙ forget C)).pt ≅ ((forget C).mapCocone (colimitCocone F)).pt

pp: 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
⊢ autoParam
    (∀ (j : J), (colimit.cocone (F ⋙ forget C)).ι.app j ≫ Iso.hom ?φ = ((forget C).mapCocone (colimitCocone F)).ι.app j)
    Cocone.ext._auto_1

Tactic:
· rfl

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
⊢ autoParam
    (∀ (j : J),
      (colimit.cocone (F ⋙ forget C)).ι.app j ≫ (Iso.refl (colimit.cocone (F ⋙ forget C)).pt).hom =
        ((forget C).mapCocone (colimitCocone F)).ι.app j)
    Cocone.ext._auto_1
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
x✝ : ↑↑X
⊢ (ConcreteCategory.hom (X.toRestrictTop ≫ X.ofRestrict ⋯).base) x✝ = (ConcreteCategory.hom (𝟙 X).base) x✝

pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)

Tactic:
· rfl

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case naturality
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X : Jᵒᵖ
⊢ ∀ {Y : Jᵒᵖ} (f : X ⟶ Y),
    ((pushforwardDiagramToColimit F).leftOp ⋙
              (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
                ((Opens.map
                        (colimit.isoColimitCocone
                                { cocone := colimitCocone F,
                                  isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                  (op U))).map
          f ≫
        (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =
      (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f

Tactic:
Y

Goal state after:
case naturality
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
⊢ ∀ (f : X ⟶ Y),
    ((pushforwardDiagramToColimit F).leftOp ⋙
              (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
                ((Opens.map
                        (colimit.isoColimitCocone
                                { cocone := colimitCocone F,
                                  isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                  (op U))).map
          f ≫
        (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =
      (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f
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
V : Opens ↑↑Y
U : Opens ↑↑X
h : V = (opensFunctor f).obj U
⊢ IsIso (f.c.app (op V))

Tactic:
subst h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ IsIso (f.c.app (op ((opensFunctor f).obj U)))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
⊢ f.base = ofHom { toFun := g, continuous_toFun := ⋯ }

Tactic:
subst h

Goal state after:
X Y : Scheme
f : X.Hom Y
⊢ f.base = ofHom { toFun := ⇑f, continuous_toFun := ⋯ }
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
x : ↥X
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := g, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))

Tactic:
subst h

Goal state after:
X Y : Scheme
f : X.Hom Y
x : ↥X
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := ⇑f, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
⊢ f.copyBase g h = f

Tactic:
subst h

Goal state after:
X Y : Scheme
f : X.Hom Y
⊢ f.copyBase ⇑f ⋯ = f
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : Type u_2
⊢ ∀ {Y S : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))

Tactic:
Y

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X Y : Type u_2
⊢ ∀ {S : Type u_2} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison (𝟭 (Type u_2)) f g))
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
⊢ (P ⊓ Q).precoverage = P.precoverage ⊓ Q.precoverage

Tactic:
ext X R

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
X : C
R : Presieve X
⊢ R ∈ (P ⊓ Q).precoverage.coverings X ↔ R ∈ (P.precoverage ⊓ Q.precoverage).coverings X
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
P : MorphismProperty D
F : C ⥤ D
⊢ Precoverage.comap F P.precoverage = (P.inverseImage F).precoverage

Tactic:
ext X R

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
P : MorphismProperty D
F : C ⥤ D
X : C
R : Presieve X
⊢ R ∈ (Precoverage.comap F P.precoverage).coverings X ↔ R ∈ (P.inverseImage F).precoverage.coverings X
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g ⋙ forget) (PresheafedSpace.forget C)

Tactic:
have : PreservesLimit
        (cospan ((cospan f g ⋙ forget).map Hom.inl)
          ((cospan f g ⋙ forget).map Hom.inr)) (PresheafedSpace.forget C) := by
        dsimp
        infer_instance
      apply preservesLimit_of_iso_diagram _ (diagramIsoCospan _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
Y

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (toOpenₗ R M (basicOpen s)) f = const (s ^ n • f) (s ^ n) (basicOpen s) ⋯

Tactic:
dsimp [toOpenₗ]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ const f 1 (basicOpen s) ⋯ = const (s ^ n • f) (s ^ n) (basicOpen s) ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ ↑((resLE f U V e) x) = f ↑x

Tactic:
simp [resLE, morphismRestrict_base]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
⊢ U.toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) = X.homOfLE h ≫ V.toSpecΓ

Tactic:
by
  delta Scheme.Opens.toSpecΓ
  simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

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

Tactic:
dsimp [toOpenₗ]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯)) (const f 1 (basicOpen ↑s) ⋯) =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      (const (↑s • f) (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
a : ↑Γ(Y, U)
⊢ ((CommRingCat.Hom.hom
            (((IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal.primeCompl (↑(Y.presheaf.stalk (f x)))
                        (Localization.AtPrime (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom ≫
                CommRingCat.ofHom
                  (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
                    (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯)) ≫
              (IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl (↑(X.presheaf.stalk x))
                      (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toRingEquiv.toCommRingCatIso.inv)).comp
        (algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk (f x))))
      a =
    ((CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).comp (algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk (f x)))) a

Tactic:
dsimp [← AlgEquiv.symm_toRingEquiv]

Goal state after:
case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
a : ↑Γ(Y, U)
⊢ (IsLocalization.map (↑(X.presheaf.stalk x)) (RingHom.id ↑Γ(X, V)) ⋯)
      ((Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯)
        ((IsLocalization.map (Localization.AtPrime (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal) (RingHom.id ↑Γ(Y, U)) ⋯)
          ((algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk (f x))) a))) =
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)) ((algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk (f x))) a)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ ⨆ f, X.basicOpen ↑f = U

Tactic:
@comm _ Eq

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ U = ⨆ f, X.basicOpen ↑f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ U ≤ ⨆ i ∈ s, X.basicOpen i

Tactic:
· intro x hx
    obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2
    refine SetLike.mem_of_subset ?_ hxV
    rw [← (hV.iSup_basicOpen_eq_self_iff (s := X.presheaf.map (homOfLE hVU).op '' s)).mpr
      (by rw [← Ideal.map_span, hs, Ideal.map_top])]
    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image,
      Set.iUnion_exists, Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res,
      Opens.coe_inf, Opens.coe_mk, Set.iUnion_subset_iff]
    exact fun i hi ↦ (Set.inter_subset_right.trans
      (Set.subset_iUnion₂ (s := fun x _ ↦ (X.basicOpen x : Set X)) i hi))

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.ι i))

Tactic:
by
  intro x y h
  rcases (D.ι_eq_iff_rel _ _ _ _).mp h with ⟨_, e₁, e₂⟩
  · dsimp only at *
    -- Porting note: there were `cases e₁` and `cases e₂`, instead of the `rw`
    rw [← e₁, ← e₂]
    simp

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) =
    ↑((ConcreteCategory.hom (h.t j j)) ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Tactic:
rw [h.t_id] at this

Goal state after:
case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this : ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) = ↑(id ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫ D.isoCarrier.inv =
    (D.ι i).base

Tactic:
delta isoCarrier

Goal state after:
D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
      ((PresheafedSpace.forget CommRingCat).mapIso
            (SheafedSpace.forgetToPresheafedSpace.mapIso
                (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                  D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
              D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace) ≪≫
          D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso
            (PresheafedSpace.forget CommRingCat)).inv =
    (D.ι i).base
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h.hU
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq :
  (ConcreteCategory.hom (D.t i k).base) ((ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) y) =
    (ConcreteCategory.hom (D.t i k).base) ((ConcreteCategory.hom (D.t k i).base) x)
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

Tactic:
change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq

Goal state after:
case h.hU
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq :
  (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y =
    (ConcreteCategory.hom (D.t k i ≫ D.t i k).base) x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
rw [← hy]

Goal state after:
case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ IsIso
    (Scheme.Hom.stalkMap (Sigma.desc α)
      (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
⊢ x ∈ Scheme.Hom.opensRange (Sigma.desc f)

Tactic:
have : x ∈ ⨆ i, (f i).opensRange := by rwa [hcov]

Goal state after:
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this✝ : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
this : x ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ x ∈ Scheme.Hom.opensRange (Sigma.desc f)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
⊢ Nonempty (IsColimit (BinaryCofan.mk f g))

Tactic:
let i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl _) (by rintro (b | b) <;> rfl)

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
⊢ Nonempty (IsColimit (BinaryCofan.mk f g))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
⊢ ⊥ ⊓ U = ⊥

Tactic:
bot_inf_eq

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
⊢ ⊥ = ⊥
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
x✝ : ↑(CommRingCat.of R) × S
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal ↔ x✝ ∈ x.asIdeal.prod ⊤

Tactic:
simp [Ideal.prod, CommRingCat.ofHom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
x✝ : R × ↑(CommRingCat.of S)
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal ↔ x✝ ∈ ⊤.prod x.asIdeal

Tactic:
simp [Ideal.prod, CommRingCat.ofHom]

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
s : PullbackCone f g
i : 𝒰.I₀
⊢ (gluing 𝒰 f g).ι i ≫ p1 𝒰 f g = pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i

Tactic:
by rw [gluing_ι, p1, Multicoequalizer.π_desc]

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
⊢ IsZariskiLocalAtSource P

Tactic:
by
  refine .mk_of_iff_of_zeroHypercover fun {X Y} f 𝒰 ↦ ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
  · rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
    exact restrict _ _ hf
  · refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange <| .ulift 𝒰) fun i ↦ ?_
    dsimp
    rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f _) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f _).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
    exact hf _

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P.toProperty f ↔ P.toProperty f'

Tactic:
P.toProperty.arrow_mk_iso_iff e

Goal state after:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P.toProperty f' ↔ P.toProperty f'
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X : Scheme
⊢ ∀ ⦃Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X},
    IsPullback g' f' f g → P g → P g'

Tactic:
Y

Goal state after:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y : Scheme
⊢ ∀ ⦃S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X},
    IsPullback g' f' f g → P g → P g'