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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
this : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c
j : Discrete ι
hj : op j ≠ op i
⊢ IsTerminal
    ((PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
          ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (H.functor.obj U))).obj
      (op j))

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
this : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c
j : Discrete ι
hj : op j ≠ op i
⊢ IsTerminal
    ((F.obj j).presheaf.obj
      (op
        ((Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj
          ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (H.functor.obj U)))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))

Tactic:
have h₁ := ι_preservesColimitIso_inv SheafedSpace.forgetToPresheafedSpace F i
    have h₂ : colimit.ι F i =
      { hom := (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫
        (preservesColimitIso _ F).inv) } :=
      InducedCategory.hom_ext h₁.symm
    have H :
      IsOpenEmbedding
        (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
            (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).base := by
      have := h₁.symm
      convert! sigma_ι_isOpenEmbedding F i
    suffices IsIso <| (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
        (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).c.app <|
      op (H.functor.obj U) by
      convert! this
    rw [PresheafedSpace.comp_c_app,
      ← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π]
    -- Porting note: this instance created manually to make the `inferInstance` below work
    have : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c := inferInstance
    suffices IsIso (limit.π (PresheafedSpace.componentwiseDiagram
      (F ⋙ SheafedSpace.forgetToPresheafedSpace) ((Opens.map
        (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv.base).obj
          (H.functor.obj U))) (op i)) from inferInstance
    apply limit_π_isIso_of_is_strict_terminal
    rintro ⟨j⟩ hj
    dsimp
    convert! (F.obj j).sheaf.isTerminalOfEmpty using 3
    convert! image_preimage_is_empty F i j (fun h => hj (congr_arg op h.symm)) U using 6
    exact congr_arg PresheafedSpace.Hom.base h₁

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

Goal state before:
pp: case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x =
    inv
        (f.stalkMap
          ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x)) ≫
      eqToHom ⋯ ≫
        g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x) ≫ PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (inv
          (f.stalkMap
            ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x)) ≫
        eqToHom ⋯ ≫
          g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x) ≫
            PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x))

Tactic:
dsimp

Goal state after:
case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x =
    inv
        (f.stalkMap
          ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x)) ≫
      eqToHom ⋯ ≫
        g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x) ≫ PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x
⊢ IsLocalHom
    ((((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x)).comp
              (CommRingCat.Hom.hom (g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x)))).comp
          (CommRingCat.Hom.hom (eqToHom ⋯))).comp
      (CommRingCat.Hom.hom
        (inv
          (f.stalkMap
            ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x)))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m =
    {
      toHom :=
        PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
      prop := ⋯ }

Tactic:
← cancel_mono (pullbackConeOfLeft f g).snd

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m ≫ (pullbackConeOfLeft f g).snd =
    {
        toHom :=
          PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
        prop := ⋯ } ≫
      (pullbackConeOfLeft f g).snd
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case inst
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit
    (cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr))
    (PresheafedSpace.forget CommRingCat)

Tactic:
dsimp

Goal state after:
case inst
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f.toHom g.toHom) (PresheafedSpace.forget CommRingCat)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ
⊢ Module ↑((structurePresheafInCommRingCat R ⋙ forget₂ CommRingCat RingCat).obj X)
    ↑((structurePresheafInModuleCat R M ⋙ forget₂ (ModuleCat R) Ab).obj X)

Tactic:
dsimp

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ
⊢ Module ((structureSheafInType R R).obj.obj X) ((structureSheafInType R M).obj.obj X)
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: R : TopCommRingCat
⊢ Continuous ⇑{ toFun := fun x ↦ x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Tactic:
dsimp

Goal state after:
R : TopCommRingCat
⊢ Continuous fun x ↦ x
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: case mk.mk
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ⇑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ⇑val✝
⊢ Continuous ⇑((↑⟨val✝, property✝⟩).comp ↑⟨val✝¹, property✝¹⟩)

Tactic:
dsimp

Goal state after:
case mk.mk
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ⇑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ⇑val✝
⊢ Continuous (⇑val✝ ∘ ⇑val✝¹)
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
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ CommRingCat.Hom.hom
      (ConcreteCategory.ofHom
        (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map i ≫ F.map j)) ⋯)) =
    CommRingCat.Hom.hom
      (ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
        ConcreteCategory.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯))

Tactic:
dsimp

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ IsLocalization.map (Localization (G.obj W)) ((CommRingCat.Hom.hom (F.map j)).comp (CommRingCat.Hom.hom (F.map i))) ⋯ =
    (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯).comp
      (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
u : ↥(↑⟨p, hfp⟩).asIdeal.primeCompl
hu : u • ⟨↑d, ⋯⟩ • a = u • ⟨↑b, ⋯⟩ • c
⊢ ∃ a_1 ∈ ↑(⊥.colon {d • a - b • c}), a_1 ∉ ↑p.asIdeal

Tactic:
exact ⟨u.1, by simpa [sub_eq_zero, smul_sub], u.2⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ (appIso (X.homOfLE h) W).hom ≫ X.presheaf.map (homOfLE ⋯).op =
    𝟙 (X.presheaf.obj (op (⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))))))

Tactic:
dsimp

Goal state after:
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ (appIso (X.homOfLE h) W).hom ≫ X.presheaf.map (homOfLE ⋯).op =
    𝟙 (X.presheaf.obj (op (⋯.functor.obj (X.homOfLE h ''ᵁ W))))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ (X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map i ≫ (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom =
    (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom ≫ X.presheaf.map i

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ Hom.appTop (X.homOfLE ⋯) ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map i
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ Set.range ⇑((f ⁻¹ᵁ U).ι ≫ f) = Set.range ⇑U.ι

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ Set.range (⇑(TopCat.Hom.hom f.base) ∘ ⇑(TopCat.Hom.hom (f ⁻¹ᵁ U).ι.base)) = Set.range ⇑U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom) ≫ e.inv) ≫ g =
    (Arrow.mk (pullback.snd f g)).hom ≫ g

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ f ∣_ Scheme.Hom.opensRange g) ≫ e.inv) ≫ g = pullback.snd f g ≫ g
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_1
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
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
⊢ (fun i ↦ g ↑i ^ (N + 1)) j • (fun i ↦ g ↑i ^ N • f ↑i) i = (fun i ↦ g ↑i ^ (N + 1)) i • (fun i ↦ g ↑i ^ N • f ↑i) j

Tactic:
dsimp

Goal state after:
case refine_1
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
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
i j : ↥t
⊢ g ↑j ^ (N + 1) • g ↑i ^ N • f ↑i = g ↑i ^ (N + 1) • g ↑j ^ N • f ↑j
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ x✝ ∈ X.toΓSpecFun ⁻¹' ↑(basicOpen r) ↔ x✝ ∈ ↑(X.toRingedSpace.basicOpen r)

Tactic:
dsimp

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ x✝ ∈ X.toΓSpecFun ⁻¹' ↑(basicOpen r) ↔ x✝ ∈ ↑(X.toRingedSpace.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (U.stalkIso ((resLE f U V e) x) ≪≫ Y.presheaf.stalkCongr ⋯).hom ≫ (Arrow.mk (stalkMap f ↑x)).hom =
    (Arrow.mk (stalkMap (resLE f U V e) x)).hom ≫ (V.stalkIso x).hom

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ ((U.stalkIso ((resLE f U V e) x)).hom ≫ Y.presheaf.stalkSpecializes ⋯) ≫ stalkMap f ↑x =
    stalkMap (resLE f U V e) x ≫ (V.stalkIso x).hom
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 : ℕ
hn : f ^ n ∈ Ideal.span (Set.range b)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s

Tactic:
replace hn := Ideal.mul_mem_right f _ hn

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 : ℕ
hn : f ^ n * f ∈ Ideal.span (Set.range b)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x =
    X.presheaf.Γgerm x

Tactic:
rw [PresheafedSpace.Hom.stalkMap,
    ← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
    ← Category.assoc, Category.assoc (CommRingCat.ofHom _), stalkFunctor_map_germ, ← Category.assoc,
    X.toΓSpecSheafedSpace_app_eq, X.toΓSpecCApp_spec, Γgerm,
    ← dsimp% stalkPushforward_germ _ _ X.presheaf ⊤]
  congr 1
  exact (X.toΓSpecBase _* X.presheaf).germ_res le_top.hom _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
i : (Scheme.coverOfIsIso (𝟙 X)).I₀
⊢ IsAffine ((Scheme.coverOfIsIso (𝟙 X)).X i)

Tactic:
dsimp

Goal state after:
X : Scheme
inst✝ : IsAffine X
i : (Scheme.coverOfIsIso (𝟙 X)).I₀
⊢ IsAffine X
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CommRingCat.ofHom
            (algebraMap ↑(Γ.obj (op X))
              ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          { hom := X.toΓSpecSheafedSpace.hom }.hom.c.app
            (op ((Opens.map { hom := (Spec.sheafedSpaceMap f).hom }.hom.base).obj (unop (op U))))) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)

Tactic:
dsimp

Goal state after:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h :
  ∀ (r : ↑R),
    f ≫ X.presheaf.map (homOfLE ⋯).op =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op (basicOpen r)))) ≫
        β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        CommRingCat.ofHom
            (algebraMap ↑(X.presheaf.obj (op ⊤))
              ↑((structureSheaf ↑(X.presheaf.obj (op ⊤))).obj.obj
                  (op
                    ((Opens.comap { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                      U)))) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op ((Opens.map (Spec.sheafedSpaceMap f).hom.base).obj U))) ≫
      (forgetToSheafedSpace.obj X).presheaf.map (eqToHom ⋯) =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫
      (forgetToSheafedSpace.map β).hom.c.app (op U)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ (ConcreteCategory.hom
        (((𝟭 LocallyRingedSpace).obj X).toΓSpec.base ≫ (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base))
      x =
    (ConcreteCategory.hom ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).base) x

Tactic:
dsimp

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ (TopCat.Hom.hom (Spec.locallyRingedSpaceMap (f.c.app (op ⊤))).base) ((TopCat.Hom.hom X.toΓSpec.base) x) =
    (TopCat.Hom.hom Y.toΓSpec.base) ((TopCat.Hom.hom f.base) x)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (ConcreteCategory.hom
        (((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
          (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base))
      p =
    (ConcreteCategory.hom (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base) p

Tactic:
dsimp

Goal state after:
case w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (TopCat.Hom.hom (Spec.topMap (toSpecΓ R))) ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p) = p
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)ᵒᵖ
⊢ CommRingCat.ofHom
        (algebraMap R
          ((structureSheafInType ↑(unop (op (CommRingCat.of R))) ↑(unop (op (CommRingCat.of R)))).obj.obj U)) ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app U =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
dsimp

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)ᵒᵖ
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj U)) ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app U =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := ⋯
this✝ : Algebra R S := ⋯
this : IsScalarTower R S N
⊢ ((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑b, ⋯⟩)
      ((comapFun f y) (LocalizedModule.mk a b)) =
    ((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑b, ⋯⟩)
      (LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩)

Tactic:
dsimp

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ σ ↑b • (comapFun f y) (LocalizedModule.mk a b) = σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩