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

Goal state before:
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)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫
        { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).base =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
        ((Functor.const J).obj (colimit F)).map f).base

pp: 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)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).c ≫
      whiskerRight (eqToHom ⋯) (F.obj j).presheaf =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
        ((Functor.const J).obj (colimit F)).map f).c

Tactic:
· ext x
          exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x

Goal state after:
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)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).c ≫
      whiskerRight (eqToHom ⋯) (F.obj j).presheaf =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
        ((Functor.const J).obj (colimit F)).map f).c
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

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

Tactic:
← InducedCategory.comp_hom,

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

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

Tactic:
← InducedCategory.comp_hom,

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

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
cases n.eq_zero_or_pos with
  | inr h =>
    rw [← X.toRingedSpace.basicOpen_pow f n h, hn]
    simp [basicOpen_zero]
  | inl h =>
    rw [h, pow_zero] at hn
    simp [eq_zero_of_zero_eq_one hn.symm f, basicOpen_zero]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
h : 0 < n
⊢ X.basicOpen (f ^ n) = X.basicOpen f

Tactic:
by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h
  induction k with
  | zero => simp
  | succ n hn => rw [pow_add]; simp_all

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑X
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
by simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑X
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
by simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

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
h' : Epi f.base
⊢ IsIso f

Tactic:
have : ∀ (U : (Opens Y)ᵒᵖ), IsIso (f.c.app U) := by
    intro U
    have : U = op (opensFunctor f |>.obj ((Opens.map f.base).obj (unop U))) := by
      induction U with | op U => ?_
      cases U
      dsimp only [Functor.op, Opens.map]
      congr
      exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm
    convert! H.c_iso (Opens.map f.base |>.obj <| unop U)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
⊢ IsIso f
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:
by
  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]
  rw [← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
⊢ E.Small

Tactic:
choose i y hy using ofArrows_mem_jointlySurjectivePrecoverage_iff.mp E.mem₀
    refine ⟨X, i, ?_⟩
    rw [ofArrows_mem_jointlySurjectivePrecoverage_iff]
    intro x
    use x, y x, hy x

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

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

Tactic:
by simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

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

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

Tactic:
by simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

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

Goal state before:
pp: X✝ : TopCat
R : TopCommRingCat
X : TopCommRingCat
⊢ { app := fun X_1 ↦ continuousFunctions.map X_1 (𝟙 X), naturality := ⋯ } =
    𝟙
      { obj := fun X_1 ↦ continuousFunctions X_1 X, map := fun {x x_1} f ↦ continuousFunctions.pullback f X,
        map_id := ⋯, map_comp := ⋯ }

Tactic:
by
    ext
    rfl

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
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ 1 • ⟨g i * g j, ⋯⟩ • f i = 1 • ⟨g i, ⋯⟩ • g j • f i

Tactic:
by simp [Submonoid.smul_def, ← smul_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f : ↑R
⊢ ↑(PrimeSpectrum.basicOpen f) = Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

Tactic:
exact (PrimeSpectrum.localization_away_comap_range _ _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f

Tactic:
by
  apply IsOpenImmersion.isPullback <;>
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f

Tactic:
isoSpec,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f

Tactic:
isoSpec,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ f ≫ Y.toSpecΓ ≫ (asIso Y.toSpecΓ).inv = f
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : i = k
⊢ IsIso (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
subst hik

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
hij : ¬i = j
⊢ IsIso (pullback.snd (D.f' j i) (D.f' j i))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))

Tactic:
bijective_iff_isIso_ofHom

Goal state after:
case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ IsIso (↾⇑(ConcreteCategory.hom (D.t i j)))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ ((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData LocallyRingedSpace.forgetToSheafedSpace).ι i).hom ≫
          D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv.hom).base ≫
      (LocallyRingedSpace.forgetToSheafedSpace.map D.isoLocallyRingedSpace.inv).hom.base =
    (D.ι i).base

Tactic:
← InducedCategory.comp_hom,

Goal state after:
D : GlueData
i : D.J
⊢ (((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData LocallyRingedSpace.forgetToSheafedSpace).ι i ≫
            D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv).hom.base ≫
      (LocallyRingedSpace.forgetToSheafedSpace.map D.isoLocallyRingedSpace.inv).hom.base =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
⊢ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
intro (i : X); exact isEmptyElim i

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

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        invApp (D.f j i) ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))) ≫
          (D.f j k).c.app
              (op
                ((opensFunctor (D.f j i)).obj
                  ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))))) ≫
            ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
f_invApp_f_app_assoc

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ (F.map k₁.snd.1)
      ((TopCat.Hom.hom (Hom.isoOpensRange (F.map k₁.snd.1)).inv.base)
        ((TopCat.Hom.hom (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).base) x)) =
    (F.map k₂.snd.1)
      ((TopCat.Hom.hom (Hom.isoOpensRange (F.map k₂.snd.1)).inv.base)
        ((TopCat.Hom.hom (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).base) x))

Tactic:
simp only [← Hom.comp_apply]

Goal state after:
J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ ((pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) ≫
        F.map k₁.snd.1)
      x =
    ((pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) ≫
        F.map k₂.snd.1)
      x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      invApp (pullback.snd (D.f k i) (D.f k j))
          (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U))))) ≫
        (D.V (k, j)).presheaf.map (eqToHom ⋯) ≫
          (D.t j k).c.app ((Opens.map (D.f k j).base).op.obj (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U)))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
(D.t j k).c.naturality_assoc,

Goal state after:
case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      invApp (pullback.snd (D.f k i) (D.f k j))
          (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U))))) ≫
        (D.t j k).c.app
            (op
              ((opensFunctor (pullback.snd (D.f k i) (D.f k j))).obj
                (unop
                  (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U))))))) ≫
          ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec

Tactic:
by
  have : IsEmpty (Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ)) :=
    @Function.isEmpty _ _ spec_punit_isEmpty (Scheme.Spec.mapIso
      (initialIsoIsInitial (initialOpOfTerminal CommRingCat.punitIsTerminal))).hom
  have := preservesInitial_of_iso Scheme.Spec (asIso (initial.to _))
  exact preservesColimitsOfShape_pempty_of_preservesInitial _

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✝
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback f g

Tactic:
rw [← Scheme.Spec.map_preimage f, ← Scheme.Spec.map_preimage g]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback (Scheme.Spec.map (Scheme.Spec.preimage f)) (Scheme.Spec.map (Scheme.Spec.preimage g))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine ↑(e.hom ⁻¹ᵁ U)
⊢ P ((f ≫ e.hom) ∣_ U)

Tactic:
rw [morphismRestrict_comp, P.cancel_right_of_respectsIso]

Goal state after:
case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine ↑(e.hom ⁻¹ᵁ U)
⊢ P (f ∣_ e.hom ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this : IsIso (V F (↓i) ↓j).ι
⊢ F.map f ≫ (glueData F).ι j = (glueData F).ι i

Tactic:
have : t F ↓i ↓j ≫ (V F ↓j ↓i).ι ≫ _ = (V F ↓i ↓j).ι ≫ _ :=
    (glueData F).glue_condition i j

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : t F (↓i) ↓j ≫ (V F (↓j) ↓i).ι ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ F.map f ≫ (glueData F).ι j = (glueData F).ι i
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₂
⊢ ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
    (f : α → β) (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)

Tactic:
· introv hf hg
    exact hf.comp hg

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝¹ : M.Over S
f : T ⟶ S
inst✝ : MonObj (M.asOver S)
⊢ MonObj ((pullback (M ↘ S) f).asOver T)

Tactic:
unfold asOver OverClass.asOver at *; exact Over.monObjMkPullbackSnd

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
⊢ IsLocalization.Away (IsLocalization.Away.mulNumerator s t ⟨a, b⟩)
    ((fun x ↦
        match x with
        | ⟨a, b⟩ => Localization.Away ↑b)
      ⟨a, b⟩)

Tactic:
have : IsLocalization.Away ((algebraMap S (Localization.Away a.val))
        (IsLocalization.Away.sec a.val b.val).1) (Localization.Away b.val) := by
      apply IsLocalization.Away.of_associated (r := b.val)
      rw [← IsLocalization.Away.sec_spec]
      apply associated_mul_unit_right
      rw [map_pow _ _]
      exact IsUnit.pow _ (IsLocalization.Away.algebraMap_isUnit _)

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
this :
  IsLocalization.Away ((algebraMap S (Localization.Away ↑a)) (IsLocalization.Away.sec ↑a ↑b).1) (Localization.Away ↑b)
⊢ IsLocalization.Away (IsLocalization.Away.mulNumerator s t ⟨a, b⟩)
    ((fun x ↦
        match x with
        | ⟨a, b⟩ => Localization.Away ↑b)
      ⟨a, b⟩)
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ ∃ a, (algebraMap S (S ⊗[R] T)) a = x ⊗ₜ[R] (algebraMap R T) y

Tactic:
use y • x

Goal state after:
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ (algebraMap S (S ⊗[R] T)) (y • x) = x ⊗ₜ[R] (algebraMap R T) y
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : T
⊢ ∃ a, (algebraMap S (S ⊗[R] T)) a = x ⊗ₜ[R] y

Tactic:
obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g (𝒰.f i ≫ f)
⊢ P (pullback.fst g (𝒰.f i ≫ f))

Tactic:
← P.cancel_left_of_respectsIso (pullbackLeftPullbackSndIso g f _).hom,

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g (𝒰.f i ≫ f)
⊢ P ((pullbackLeftPullbackSndIso g f (𝒰.f i)).hom ≫ pullback.fst g (𝒰.f i ≫ f))