mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
⊢ Sheaf.pullback A f ≅ sheafPullback A hf

Tactic:
refine Sheaf.pullbackIso A f ≪≫ NatIso.ofComponents (fun F ↦ ?_) (fun u ↦ ?_)

Goal state after:
case refine_1
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
F : TopCat.Sheaf A Y
⊢ (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology ↑X) A).obj F ≅
    (sheafPullback A hf).obj F

case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology ↑X) A).map u ≫
      Iso.hom ?refine_1 =
    Iso.hom ?refine_1 ≫ (sheafPullback A hf).map u
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
F : J ⥤ PresheafedSpace C
j : J
U : (Opens ↑↑(F.obj j))ᵒᵖ
⊢ 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base

Tactic:
by simp

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : ↑Y.toTopCat
⊢ y = (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)

Tactic:
by simp

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ e.inv ≫ e.hom = 𝟙 Y

Tactic:
by simp

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : ↑Y.toTopCat
z : ↑(Y.presheaf.stalk ((ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)))
⊢ y = (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)

Tactic:
by simp

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
x : ↑X.toTopCat
⊢ x = (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)

Tactic:
by simp

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ e.hom ≫ e.inv = 𝟙 X

Tactic:
by simp

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
x : ↑X.toTopCat
y : ↑(X.presheaf.stalk ((ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)))
⊢ x = (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ U✝ = (TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
⊢ ↑(f ⁻¹ᵁ iSup U) = ↑(⨆ i, f ⁻¹ᵁ U i)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ appTop (inv f) = inv (appTop f)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ Spec.map (𝟙 R).unop = 𝟙 (Spec (unop R))

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Spec.map (f ≫ g).unop = Spec.map f.unop ≫ Spec.map g.unop

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫ (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (eqToHom ⋯).op = eqToHom ⋯

Tactic:
simp [eqToHom_map]

Goal state after:
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 : IsOpenImmersion f
g : Y ⟶ Z
⊢ pullbackConeOfLeftFst f g ≫ f = Y.ofRestrict ⋯ ≫ g

Tactic:
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun U => ?_
  · simpa using! pullback.condition
  · induction U
    simp only [(NatTrans.comp_app), comp_c_app, unop_op, Functor.whiskerRight_app,
      pullbackConeOfLeftFst, app_invApp_assoc, eqToHom_app, Category.assoc,
      NatTrans.naturality_assoc, restrict_carrier, comp_base, ofRestrict_base, restrict_presheaf,
      Functor.comp_obj, Functor.op_obj, Opens.map_comp_obj, TopCat.Presheaf.pushforward_obj_obj,
      Opens.carrier_eq_coe, homOfLE_leOfHom, TopCat.Presheaf.pushforward_obj_map, Functor.comp_map,
      Functor.op_map, eqToHom_unop, ofRestrict_c_app, Functor.id_obj]
    rw [← Y.presheaf.map_comp, ← Y.presheaf.map_comp]
    congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y) = y

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
z : ↑(Y.presheaf.stalk (e.hom (e.inv y)))
⊢ e.hom (e.inv y) = y

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
y : ↑(X.presheaf.stalk (e.inv (e.hom x)))
⊢ e.inv (e.hom x) = x

Tactic:
by simp

Goal state after:
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
U : X.Opens
⊢ U = 𝟙 X ''ᵁ U

Tactic:
by simp

Goal state after:
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 Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : X.Opens
⊢ g ''ᵁ f ''ᵁ U = (f ≫ g) ''ᵁ U

Tactic:
by simp

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

Goal state before:
pp: case refine_2.op
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
x : Opens ↑↑X
this :
  ∀ {Z_1 : C}
    (h : ((TopCat.Presheaf.pushforward C (s.snd ≫ g).base).obj s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶ Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ s.fst.c.app (op x) ≫
      ((TopCat.Presheaf.pushforward C s.fst.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
        inv (s.pt.presheaf.map (eqToHom ⋯)) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
simp [eqToHom_map]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K L : Precoverage C
P : MorphismProperty C
inst✝ : K.HasIsos
X : C
⊢ Presieve.singleton (𝟙 X) (𝟙 X)

Tactic:
by simp

Goal state after:
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
H : IsOpenImmersion f
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
inst✝¹ : JointlySurjective K
inst✝ : Nonempty ↥X
𝒰 : Cover K X
⊢ Nonempty 𝒰.I₀

Tactic:
by
  obtain ⟨i, _⟩ := 𝒰.exists_eq ‹Nonempty X›.some
  use i

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
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (f.c.app (op U))

Tactic:
have : U = H.base_open.functor.obj ((Opens.map f.base).obj U) := by
    ext1
    exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm
  convert! H.c_iso ((Opens.map f.base).obj U)

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (pullback.snd iV f) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
rw [← H.isoPullback_inv_snd] at hx

Goal state after:
case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
y : ↥V
hy : y ∈ ↑W
x : ↥(pullback iV f)
hx : (H.isoPullback.inv ≫ iU) x ∉ Set.range ⇑iU
e : iV y = f ((pullback.snd iV f) x)
⊢ (pullback.snd iV f) x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ IsPullback (lift g f H) (𝟙 X) g f

Tactic:
by
  convert! IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)
  · exact (Category.comp_id _).symm
  · simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f✝) g
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd ≫ 𝟙 (𝒰.X i.fst) =
    𝟙 (𝒰.affineRefinement.openCover.X i) ≫ (𝒰.X i.fst).affineCover.f i.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U

Tactic:
simp_rw [← U.ι_image_top]

Goal state after:
X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ U.ι ''ᵁ unop (op (U.ι ⁻¹ᵁ U)) = U

Tactic:
by simp

Goal state after:
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
U : Opens ↑(PrimeSpectrum.Top R)
⊢ U ≤ basicOpen 1

Tactic:
by simp

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
f₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
h : g₂ • f₁ = g₁ • f₂
x : ↥(unop (op U))
⊢ ∃ u, u • ⟨g₂, ⋯⟩ • f₁ = u • ⟨g₁, ⋯⟩ • f₂

Tactic:
simp [h, Submonoid.smul_def]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds
X : Scheme
⊢ ∀ (a : ↥X) (u : Set ↥X), a ∈ u → IsOpen u → ∃ v ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, a ∈ v ∧ v ⊆ u

Tactic:
· rintro a U haU hU
    rcases X.affineCover.covers a with ⟨x, e⟩
    let U' := (X.affineCover.f (X.affineCover.idx a)) ⁻¹' U
    have hxU' : x ∈ U' := by rw [← e] at haU; exact haU
    rcases PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU'
        ((X.affineCover.f (X.affineCover.idx a)).continuous.isOpen_preimage _
          hU) with
      ⟨_, ⟨_, ⟨s, rfl⟩, rfl⟩, hxV, hVU⟩
    refine ⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩ <;> rw [affineBasisCover_map_range]
    · exact ⟨x, hxV, e⟩
    · rw [Set.image_subset_iff]; exact hVU

Goal state after:
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
U : Opens ↑(PrimeSpectrum.Top R)
m : M
⊢ U ≤ basicOpen 1

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ (fun U_1 ↦ U_1 ≤ Scheme.Hom.opensRange U.ι) = fun V ↦ V ≤ U

Tactic:
by simp

Goal state after:
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
U : Opens ↑(PrimeSpectrum.Top R)
f : M
⊢ U ≤ basicOpen 1

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R
⊢ basicOpen f ≤ basicOpen 1

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r) = X.basicOpen r

Tactic:
Scheme.basicOpen_res_eq

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen r = X.basicOpen r
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen r

Tactic:
rw [Scheme.Opens.ι_image_basicOpen', Scheme.basicOpen_res_eq]

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
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
s : ↑(F.presheaf.obj U)
hs : s ∈ m
⊢ s ∈ nonZeroDivisorsRight ↑(F.presheaf.obj U)

Tactic:
t

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
⊢ t * s = 0 → t = 0
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
V : (↑U).Opens
r : ↑Γ(↑U, V)
x : ↥U
⊢ x ∈ (↑U).basicOpen r ↔ ↑x ∈ X.basicOpen r

Tactic:
← U.toScheme.basicOpen_res_eq _ (eqToHom (U.ι.preimage_image_eq V)).op

Goal state after:
X : Scheme
U : X.Opens
V : (↑U).Opens
r : ↑Γ(↑U, V)
x : ↥U
⊢ x ∈ (↑U).basicOpen ((ConcreteCategory.hom ((↑U).presheaf.map (eqToHom ⋯).op)) r) ↔ ↑x ∈ X.basicOpen r
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ 1 • s ^ n • f = s ^ n • f

Tactic:
by simp

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
f : R
s : LocalizedModule.Away f M
⊢ ∀ ⦃a₂ : LocalizedModule.Away f M⦄, (toBasicOpenₗ R M f) s = (toBasicOpenₗ R M f) a₂ → s = a₂

Tactic:
t

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s t : LocalizedModule.Away f M
⊢ (toBasicOpenₗ R M f) s = (toBasicOpenₗ R M f) t → s = t
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [e₃, ← Functor.map_comp]

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W =
    X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op)
⊢ X.presheaf.map
      (((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫
        inv ((Hom.opensFunctor U.ι).map ((Opens.map (X.homOfLE e).base).map (eqToHom this))).op) =
    X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U V : X.Opens
i : U ⟶ V
⊢ X.homOfLE ⋯ ≫ (Over.mk V.ι).hom = (Over.mk U.ι).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
⊢ (isoImage f U).inv ≫ X.homOfLE e = Y.homOfLE ⋯ ≫ (isoImage f V).inv

Tactic:
simp [← cancel_mono (f.isoImage V).hom, ← f.isoImage_hom_homOfLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
⊢ U.ι ≫ (Iso.refl X).hom = (Iso.refl ↑U).hom ≫ U.ι

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
⊢ V.ι ≫ (Iso.refl X).hom = (Iso.refl ↑V).hom ≫ V.ι

Tactic:
by simp

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
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
⊢ (i.1, j.1) ∈ t ×ˢ t

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ resLE (𝟙 X) V' V i = X.homOfLE i

Tactic:
by
  simp only [resLE, morphismRestrict_id]
  rfl

Goal state after:
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
⊢ ↑((resLE f U V e) x) = f ↑x

Tactic:
by simp

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
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

Tactic:
rw [← pow_succ, Ideal.span, Finsupp.mem_span_range_iff_exists_finsupp] at 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 : ∃ c, (c.sum fun i a ↦ a • b i) = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
Iso.eq_inv_comp,

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ Y.homOfLE ⋯ ≫ resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ = resLE iY UT UY ⋯ ≫ T.homOfLE hUST

Tactic:
by simp

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
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 : (c.sum fun i a ↦ a • b i) = f ^ (n + 1)
⊢ ∀ (i : ι), 0 • b i = 0

Tactic:
by simp

Goal state after: