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

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : g₁.base ≫ f = g₂.base ≫ f
⊢ g₁.base = g₂.base

Tactic:
cancel_mono

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : g₁.base = g₂.base
⊢ g₁.base = g₂.base
Module: Mathlib.Topology.Sheaves.SheafOfFunctions

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
⊢ ∃! s, (X.presheafToTypes T).IsGluing U sf s

Tactic:
choose index index_spec using fun x : ↑(iSup U) => Opens.mem_iSup.mp x.2

Goal state after:
X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
index : ↥(iSup U) → ι
index_spec : ∀ (x : ↥(iSup U)), ↑x ∈ U (index x)
⊢ ∃! s, (X.presheafToTypes T).IsGluing U sf s
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
op : {x : ↑X} → T x → T x
hop : ∀ {U : Opens ↑X} {a : (x : ↥U) → T ↑x}, P.pred a → ∀ (p : ↥U), ∃ W i, ↑p ∈ W ∧ P.pred fun x ↦ op (a (i x))
U : Opens ↑X
a : (x : ↥U) → T ↑x
ha✝ : P.sheafify.pred a
x : ↥U
Va : Opens ↑X
ma : ↑x ∈ Va
ia : Va ⟶ U
ha : P.pred fun x ↦ a (ia x)
W : Opens ↑X
sa : W ⟶ Va
hx : ↑⟨↑x, ma⟩ ∈ W
hw : P.pred fun x ↦ op (a (ia (sa x)))
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ (fun x ↦ op (a x)) (i x)

Tactic:
exact ⟨W, hx, sa ≫ ia, hw⟩

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

Goal state before:
pp: X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha✝ : P₁.sheafify.pred a
hb✝ : P₂.sheafify.pred b
x : ↥U
Va : Opens ↑X
ma : ↑x ∈ Va
ia : Va ⟶ U
ha : P₁.pred fun x ↦ a (ia x)
Vb : Opens ↑X
mb : ↑x ∈ Vb
ib : Vb ⟶ U
hb : P₂.pred fun x ↦ b (ib x)
W : Opens ↑X
sa : W ⟶ Va
sb : W ⟶ Vb
hx : ↑⟨↑x, ⋯⟩ ∈ W
hw : P₃.pred fun x ↦ op (a (ia (sa x))) (b (ib (sb x)))
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P₃.pred fun x ↦ (fun x ↦ op (a x) (b x)) (i x)

Tactic:
exact ⟨W, hx, sa ≫ ia, hw⟩

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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          (colimit.ι F j).c.app
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj
                  ((Opens.map
                        (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                    U))) ≫
            ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
← comp_c_app_assoc,

Goal state after:
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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (colimit.ι F j ≫
                  (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).c.app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case inr
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
a✝ : b ≤ x
h : b ≠ x
⊢ x ≤ b

Tactic:
· have := IsClosed.not_specializes hx rfl h
    contradiction

Goal state after:
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; rfl

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

Goal state before:
pp: case e'_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op ≍ Y.presheaf.map (𝟙 (op (hf.functor.obj U)))

pp: case convert_2
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))

Tactic:
· -- Porting note: was `apply Subsingleton.helim; rw [this]`
      -- See https://github.com/leanprover/lean4/issues/2273
      congr
      · simp only
        congr
      apply Subsingleton.helim
      rw [this]

Goal state after:
case convert_2
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
this : IsUnit ((algebraMap ↑R ↑((structurePresheafInCommRingCat ↑R).stalk x)) f) ↔ f ∉ x.asIdeal
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f

Tactic:
by exact this

Goal state after:
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:
simp [Set.image_iUnion₂]

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

Goal state before:
pp: case φ
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
⊢ (limit.cone (cospan f.base g.base)).pt ≅
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
        ((forget C).mapCone (pullbackConeOfLeft f g))).pt

pp: case w
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
⊢ autoParam
    (∀ (j : WalkingCospan),
      (limit.cone (cospan f.base g.base)).π.app j =
        Iso.hom ?φ ≫
          ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
                  ((forget C).mapCone (pullbackConeOfLeft f g))).π.app
            j)
    Cone.ext._auto_1

Tactic:
· exact Iso.refl _

Goal state after:
case w
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
⊢ autoParam
    (∀ (j : WalkingCospan),
      (limit.cone (cospan f.base g.base)).π.app j =
        (Iso.refl (limit.cone (cospan f.base g.base)).pt).hom ≫
          ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
                  ((forget C).mapCone (pullbackConeOfLeft f g))).π.app
            j)
    Cone.ext._auto_1
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ Scheme.Hom.app f U ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op

Tactic:
← map_ΓIso_inv

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv) ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (Z.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap g (snd p))).hom ≫ Hom.stalkMap snd p =
    Hom.stalkMap f x ≫ (X.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap fst p)).hom

Tactic:
subst hx

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
this : IsOpenImmersion fst
⊢ (Z.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap g (snd p))).hom ≫ Hom.stalkMap snd p =
    Hom.stalkMap f (fst p) ≫ (X.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap fst p)).hom
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
⊢ IsIso f

Tactic:
by
    -- We have an isomorphism in `TopCat`,
    let i_Top := asIso ((forget₂ TopCommRingCat TopCat).map f)
    -- and a `RingEquiv`.
    let e_Ring : X ≃+* Y := { f.1, ((forget TopCat).mapIso i_Top).toEquiv with }
    -- Putting these together we obtain the isomorphism we're after:
    exact
      ⟨⟨⟨e_Ring.symm, i_Top.inv.hom.2⟩,
          ⟨by
            ext x
            exact e_Ring.left_inv x, by
            ext x
            exact e_Ring.right_inv x⟩⟩⟩

Goal state after:
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
⊢ Mono F.presheaf.toTotalQuotientPresheaf

Tactic:
by
  apply +allowSynthFailures NatTrans.mono_of_mono_app
  intro U
  apply ConcreteCategory.mono_of_injective
  dsimp [toTotalQuotientPresheaf]
  -- Porting note: `M` and `S` need to be specified manually, so used a hack to save some typing
  set m := _
  change Function.Injective (algebraMap _ (Localization m))
  refine IsLocalization.injective (M := m) (S := Localization m) ?_
  rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
  intro s hs t e
  apply section_ext F (unop U)
  intro x hx
  rw [map_zero]
  apply (Submonoid.mem_iInf.mp hs ⟨x, hx⟩).2
  rw [← map_mul, e, map_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ (basicOpenIsoSpecAway x).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv

Tactic:
subst hx

Goal state after:
R : CommRingCat
f g : ↑R
⊢ (basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V

Tactic:
rw [← TopologicalSpace.Opens.map_comp_obj, ← Scheme.Hom.comp_base, Scheme.homOfLE_ι]
    exact V.functor_map_eq_inf U

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U = (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
change _ = (Spec Γ(X, U)).presheaf.map (homOfLE le_top).op

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U = (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)

Tactic:
convert!
    isAffineOpen_opensRange
      (Spec.map (CommRingCat.ofHom <| algebraMap Γ(X, U) (Localization.Away f)))

Goal state after:
case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ : Spec Γ(X, U) = Spec (CommRingCat.of ↑Γ(X, U))
⊢ PrimeSpectrum.basicOpen f =
    Scheme.Hom.opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U)) (Localization.Away f))))
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
X Y : C
f : X ⟶ Y
𝒰 : PreZeroHypercover Y
hR : 𝒰.presieve₀ ∈ K.coverings Y
x✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i) f
⊢ (∀ (i : { toPreZeroHypercover := 𝒰, mem₀ := hR }.I₀),
      P (pullback.snd f ({ toPreZeroHypercover := 𝒰, mem₀ := hR }.f i))) ↔
    ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], 𝒰.presieve₀ g → P (pullback.snd f g)

Tactic:
refine ⟨fun h U g hfg ↦ ?_, fun h i ↦ h _ ⟨i⟩⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
X Y : C
f : X ⟶ Y
𝒰 : PreZeroHypercover Y
hR : 𝒰.presieve₀ ∈ K.coverings Y
x✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i) f
h :
  ∀ (i : { toPreZeroHypercover := 𝒰, mem₀ := hR }.I₀), P (pullback.snd f ({ toPreZeroHypercover := 𝒰, mem₀ := hR }.f i))
U : C
g : U ⟶ Y
hfg : HasPullback f g
⊢ 𝒰.presieve₀ g → P (pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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

Tactic:
← Adjunction.homEquiv_counit,

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ ((locallyRingedSpaceAdjunction.homEquiv X ((𝟭 CommRingCatᵒᵖ).obj (op (CommRingCat.of R)))).symm
          ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f)).unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit F forgetToSheafedSpace

Tactic:
suffices PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left)
        (F.map WalkingParallelPairHom.right)) forgetToSheafedSpace from
      preservesColimit_of_iso_diagram _ (diagramIsoParallelPair F).symm

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R : C
f : R ⟶ X
⊢ Hom.left (LaxMonoidal.ε (pullback f)) = inv (pullback.snd (𝟙 X) f)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R : C
f : R ⟶ X
⊢ pullback.snd (𝟙 X) f ≫ Hom.left (LaxMonoidal.ε (pullback f)) = 𝟙 ((pullback f).obj (𝟙_ (Over X))).left
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ ⋃ i, ↑(U i) → x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
· rintro ⟨_, ⟨i, rfl⟩, hx⟩
    rename_i x
    exact ⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩

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

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.V (i, k)).presheaf.map
      ((homOfLE ⋯).op ≫
        (opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map
            (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯)) ≫
          eqToHom ⋯) =
    𝟙
      (((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))

Tactic:
(D.V (i, k)).presheaf.map_id

Goal state after:
case e'_3
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ 𝟙 ((D.V (i, k)).presheaf.obj (op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))) =
    𝟙
      (((TopCat.Presheaf.pushforward C (D.f i k).base).obj (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ (ConcreteCategory.hom (((gluedCover 𝒰).ι (idx 𝒰 x)).base ≫ (fromGlued 𝒰).base)) y = x

Tactic:
← 𝒰.ι_fromGlued (𝒰.idx x)

Goal state after:
case h
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : ((gluedCover 𝒰).ι (idx 𝒰 x) ≫ fromGlued 𝒰) y = x
⊢ (ConcreteCategory.hom (((gluedCover 𝒰).ι (idx 𝒰 x)).base ≫ (fromGlued 𝒰).base)) y = x
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))
this :
  Scheme.Hom.stalkMap (coprod.inl ≫ coprodSpec R S) x =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x) ≫ Scheme.Hom.stalkMap coprod.inl x
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))

Tactic:
← IsIso.comp_inv_eq,

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this :
  Scheme.Hom.stalkMap (coprod.inl ≫ coprodSpec R S) x ≫ inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x)))
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))
this :
  Scheme.Hom.stalkMap (coprod.inr ≫ coprodSpec R S) x =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x) ≫ Scheme.Hom.stalkMap coprod.inr x
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Tactic:
← IsIso.comp_inv_eq,

Goal state after:
case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this :
  Scheme.Hom.stalkMap (coprod.inr ≫ coprodSpec R S) x ≫ inv (Scheme.Hom.stalkMap coprod.inr x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
⊢ IsZariskiLocalAtTarget P

Tactic:
by
  refine .mk_of_iff_of_zeroHypercover fun {X Y} f 𝒰 ↦ ⟨fun hf i ↦ ?_, fun h ↦ ?_⟩
  · apply hP _ (𝒰.f i)
    rw [← pullback.condition]
    exact IsZariskiLocalAtSource.comp hf _
  · rw [P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)]
    intro i
    rw [← Scheme.Cover.pullbackHom_map]
    exact P.comp_mem _ _ (h i) (of_isOpenImmersion _)

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

Goal state before:
pp: case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              ((Opens.map
                    (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                (⋯.functor.obj U)))))))

Tactic:
have : IsIso (D.t i j).c := by apply c_isIso_of_iso
      infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsDominant f
hf : IsClosed (Set.range ⇑f)
⊢ Function.Surjective ⇑f

Tactic:
rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]

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

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : Dense ↑U
hU' : U ≤ V
⊢ IsDominant (X.homOfLE hU' ≫ V.ι)

Tactic:
simpa using Opens.isDominant_ι hU

Goal state after: