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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ (ConcreteCategory.hom (α ≫ β).base) x = x

Tactic:
IsIso.hom_inv_id α,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ (ConcreteCategory.hom (𝟙 X).base) x = x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ Mono (X.ofRestrict hf)

Tactic:
have : Mono f := (TopCat.mono_iff_injective _).mpr hf.injective
  constructor
  intro Z g₁ g₂ eq
  ext1
  · have := congr_arg PresheafedSpace.Hom.base eq
    simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this
    rw [cancel_mono] at this
    exact this
  · ext V
    have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
    have :
      IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.functor.obj V)))) :=
        NatIso.isIso_app_of_isIso
          (whiskerLeft hf.functor hf.isOpenMap.adjunction.counit) V
    have := PresheafedSpace.congr_app eq (op (hf.functor.obj V))
    rw [PresheafedSpace.comp_c_app, PresheafedSpace.comp_c_app,
      PresheafedSpace.ofRestrict_c_app, Category.assoc, cancel_epi] at this
    have h : _ ≫ _ = _ ≫ _ ≫ _ :=
      congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this
    simp only [g₁.c.naturality, g₂.c.naturality_assoc] at h
    simp only [eqToHom_op, eqToHom_map, eqToHom_trans,
      ← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc] at h
    simpa using h

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

Goal state before:
pp: J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
⊢ ((pushforward C
              (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).obj
          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt.presheaf).obj
      (op U) ≅
    limit (componentwiseDiagram F U)

Tactic:
refine (limitObjIsoLimitCompEvaluation _ _).trans (Limits.lim.mapIso ?_)

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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
⊢ (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)) ≅
    componentwiseDiagram F 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 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:
f

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.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_3
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
gl' : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
⊢ (fun s ↦ (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s) gl' → gl' = ⟨gl, ⋯⟩

Tactic:
hgl'

Goal state after:
case refine_3
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
gl' : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf gl'
⊢ gl' = ⟨gl, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat ↑R).germ ⊤ (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) trivial ≫
        PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial

Tactic:
erw [PresheafedSpace.stalkMap_germ (Spec.sheafedSpaceMap f).hom ⊤ p trivial]

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: 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
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
⊢ ⇑(ConcreteCategory.hom s.snd.base) ⁻¹' ↑(⋯.functor.obj (unop U)) =
    ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U)

Tactic:
let s' : PullbackCone f.base g.base :=
                  PullbackCone.mk s.fst.base s.snd.base (congr_arg Hom.base s.condition)

Goal state after:
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
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
⊢ ⇑(ConcreteCategory.hom s.snd.base) ⁻¹' ↑(⋯.functor.obj (unop U)) =
    ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U)
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✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ V ≤ U

Tactic:
by rwa [preimage_image_eq] at e

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

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X 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))
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
⊢ HasLimit (cospan g f ⋙ forget)

Tactic:
have : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl)
      ((cospan g f ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map g) ((forget).map f))
    infer_instance
  apply hasLimit_of_iso (diagramIsoCospan _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.fst f g ≫ f) = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
pullback.condition,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(pullback.snd f g ≫ g) = Set.range ⇑f ∩ Set.range ⇑g
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
this✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right =
    limit.π (cospan f g ⋙ forget) right ≫ 𝟙 Y.toPresheafedSpace
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)

Tactic:
rw [Category.comp_id] at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right = (pullback.snd f g).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right =
    limit.π (cospan f g ⋙ forget) right
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)
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
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left =
    limit.π (cospan g f ⋙ forget) left ≫ 𝟙 Y.toPresheafedSpace
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)

Tactic:
rw [Category.comp_id] at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this✝ : (preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left = (pullback.fst g f).hom
this :
  (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left =
    limit.π (cospan g f ⋙ forget) left
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : Scheme
⊢ ∀ (f : X✝ ⟶ Y✝), MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f

Tactic:
f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
⊢ MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
f

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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ∑ x, c x • b x • a i = f ^ (n + 1) • a i

Tactic:
← smul_assoc,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ∑ x, (c x • b x) • a i = f ^ (n + 1) • a i
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl

Tactic:
have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
H₂ : g ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl
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 : R
hf : x ∈ basicOpen f
⊢ IsUnit ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
by
  have := (isUnit_toStalk x f hf).map (algebraMap _
    (Module.End ((structurePresheafInCommRingCat R).stalk x)
      ((structurePresheafInModuleCat R M).stalk x)))
  rw [Module.End.isUnit_iff] at this ⊢
  convert! this
  ext a
  simp only [Module.algebraMap_end_apply]
  rw [toStalk_smul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    (CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        Y.toΓSpec.c.app (op (basicOpen r))) ≫
      ((𝟭 LocallyRingedSpace).map f).c.app (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r)))))

Tactic:
erw [Y.toΓSpecSheafedSpace_app_spec, f.c.naturality]

Goal state after:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    f.c.app (op ⊤) ≫ ((pushforward CommRingCat f.base).obj X.presheaf).map (Y.toΓSpecMapBasicOpen r).leTop.op
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
⊢ P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], 𝒰.presieve₀ g → P (pullback.snd f g)

Tactic:
H _ ⟨𝒰, hR⟩

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
⊢ (∀ (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)
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.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P f

Tactic:
IsLocalAtTarget.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : K.HasPullbacks
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (pullback.snd f (𝒰.restrictIndexOfSmall.f i))
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f)

Tactic:
obtain ⟨𝒰, rfl⟩ := hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
⊢ P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f g → P (g ≫ 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✝¹ : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f

Tactic:
IsLocalAtSource.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.restrictIndexOfSmall.I₀), P (𝒰.restrictIndexOfSmall.f i ≫ f)
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
⊢ (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)) ⋯) =
    Scheme.Hom.stalkMap f x ≫
      (IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl (↑(X.presheaf.stalk x))
              (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom

Tactic:
← Iso.comp_inv_eq

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
⊢ ((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 =
    Scheme.Hom.stalkMap f x
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ IsOpenMap ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
by
  intro s hs
  rw [(ofOpenSubsets U).isOpen_iff] at hs
  rw [isOpen_iff_forall_mem_open]
  rintro _ ⟨x, hx, rfl⟩
  obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
  use fromOpenSubsetsGlue U '' s ∩ Set.range (@Opens.inclusion' (TopCat.of α) (U i))
  use Set.inter_subset_left
  constructor
  · rw [← Set.image_preimage_eq_inter_range]
    apply (Opens.isOpenEmbedding (X := TopCat.of α) (U i)).isOpenMap
    convert! hs i using 1
    rw [← ι_fromOpenSubsetsGlue, coe_comp, Set.preimage_comp]
    congr! 1
    exact Set.preimage_image_eq _ (fromOpenSubsetsGlue_injective U)
  · refine ⟨Set.mem_image_of_mem _ hx, ?_⟩
    rw [ι_fromOpenSubsetsGlue_apply]
    exact Set.mem_range_self (f := (Opens.inclusion' _).hom) ⟨x, hx'⟩

Goal state after: