mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: case refine_1
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i)

Tactic:
obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
      obtain ⟨i, rfl⟩ := e₁.surjective i
      use i, (e₂ i).inv y
      simp [h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case pos
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
x : ↥U
⊢ iU x ∈ iU ''ᵁ f' ⁻¹ᵁ W ↔ (f' ≫ iV) x ∈ iV ''ᵁ W

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case e'_10
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ f = lift g f H ≫ g

Tactic:
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
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

Tactic:
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
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g

Tactic:
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✝
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
⊢ (snd ≫ g) p = g (snd p)

Tactic:
simp

Goal state after:
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)
⊢ IsIso
    ((preservesColimitIso forgetToPresheafedSpace F).inv.c.app (op (H.functor.obj U)) ≫
      (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj
              (unop (op (H.functor.obj U))))).hom ≫
        limit.π
          (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (unop (op (H.functor.obj U)))))
          (op i))

Tactic:
have : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c := inferInstance

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
⊢ IsIso
    ((preservesColimitIso forgetToPresheafedSpace F).inv.c.app (op (H.functor.obj U)) ≫
      (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj
              (unop (op (H.functor.obj U))))).hom ≫
        limit.π
          (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (unop (op (H.functor.obj U)))))
          (op i))
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:
simp

Goal state after:
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 ι✝
ι : Type w
inst✝² : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
ι' : Type v
e : ι ≃ ι'
f : Discrete ι' ≌ Discrete ι := Discrete.equivalence e.symm
⊢ colimit.ι F i =
    (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F))).inv) ≫
      (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F))).hom

Tactic:
simp

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

Goal state before:
pp: case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
x : ↥X
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g

Tactic:
replace h := h (𝒰.idx x)

Goal state after:
case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↥X
h :
  (ConcreteCategory.hom (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U)) f =
    (ConcreteCategory.hom (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U)) g
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g
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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations A ↑x
ha : a ∈ (sectionsSubmodule A U).carrier
hb : b ∈ (sectionsSubmodule A U).carrier
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R A).pred fun x ↦ (a * b) (i x)

Tactic:
by
    obtain ⟨Va, ma, ia, ra, sa, wa⟩ := ha x
    obtain ⟨Vb, mb, ib, rb, sb, wb⟩ := hb x
    refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ra * rb, sa * sb, fun x ↦ ?_⟩
    obtain ⟨hsax, hsa⟩ := wa ⟨x.1, x.2.1⟩
    obtain ⟨hsbx, hsb⟩ := wb ⟨x.1, x.2.2⟩
    exact ⟨x.1.asIdeal.primeCompl.mul_mem hsax hsbx,
      congr($hsa * $hsb).trans (LocalizedModule.mk_mul_mk ..)⟩

Goal state after:
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:
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
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ ↑(const 0 f U hu) x = ↑0 x

Tactic:
simp

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ 0 = ↑0 x
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:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X✝ Y✝ Z✝ : TopCommRingCat
f : { f // Continuous ⇑f }
g : { f // Continuous ⇑f }
⊢ Continuous ⇑((↑g).comp ↑f)

Tactic:
by
      -- TODO automate
      cases f
      cases g
      dsimp
      fun_prop

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ • (f * g₁) = (g₁ * g₂) • f

Tactic:
simp

Goal state after:
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ * (f * g₁) = g₁ * g₂ * f
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.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map (i ≫ j))) ⋯) =
    CommRingCat.ofHom (IsLocalization.map (Localization (G.obj V)) (CommRingCat.Hom.hom (F.map i)) ⋯) ≫
      CommRingCat.ofHom (IsLocalization.map (Localization (G.obj W)) (CommRingCat.Hom.hom (F.map j)) ⋯)

Tactic:
delta CommRingCat.ofHom CommRingCat.of Bundled.of
    simp_rw [F.map_comp]
    ext : 1
    dsimp
    rw [IsLocalization.map_comp_map]

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:
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:
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:
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:
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
this :
  Function.Bijective
    ⇑((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
            ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))
a : (structureSheafInType R M).obj.obj (op (basicOpen f))
⊢ ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f) a =
    ((algebraMap ((structureSheafInType R R).obj.obj (op (basicOpen f)))
          (Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
            ((structureSheafInType R M).obj.obj (op (basicOpen f)))))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f))
      a

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.homOfLE ⋯ = 𝟙 ↑U

Tactic:
← cancel_mono U.ι,

Goal state after:
X : Scheme
U : X.Opens
⊢ X.homOfLE ⋯ ≫ U.ι = 𝟙 ↑U ≫ U.ι
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:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥↑(⨆ i, U i)
i : J
hi : ↑x ∈ U i
⊢ ↑(({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i) ⟨↑x, hi⟩) = ↑x

Tactic:
simp

Goal state after:
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:
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
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ Set.range ⇑f = Set.range ⇑(opensRange f).ι

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom = (Iso.refl ↑U).hom

Tactic:
← cancel_mono U.ι,

Goal state after:
X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom ≫ U.ι = (Iso.refl ↑U).hom ≫ U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ ⇑V.ι '' Set.range ⇑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U).ι = ↑(V.ι ''ᵁ V.ι ⁻¹ᵁ U)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case H'
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (f ⁻¹ᵁ U).ι

Tactic:
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:
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:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ 𝟙 X ∣_ U = 𝟙 ↑(𝟙 X ⁻¹ᵁ U)

Tactic:
← cancel_mono U.ι,

Goal state after:
X : Scheme
U : X.Opens
⊢ 𝟙 X ∣_ U ≫ U.ι = 𝟙 ↑(𝟙 X ⁻¹ᵁ U) ≫ U.ι
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:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_2.convert_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 : ↥t
⊢ basicOpen ((fun i ↦ g ↑i ^ (N + 1)) i) ≤ basicOpen (g ↑i)

Tactic:
simp

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

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
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x =
    (Y.presheaf.stalkCongr ⋯).hom ≫ stalkMap f (V.ι x) ≫ stalkMap V.ι x

Tactic:
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)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
x : PrimeSpectrum R
hx : x ∈ PrimeSpectrum.zeroLocus (Set.range b)
⊢ f ∈ x.asIdeal

Tactic:
simpa using this hx

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Tactic:
simp

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ 𝟙 Γ(↑U, ⊤) = 𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
⊢ (↑U).OpenCover

Tactic:
refine Cover.copy (𝒰.pullback₁ U.ι) 𝒰.I₀ _ (𝒰.f · ∣_ U) (Equiv.refl _)
    (fun i ↦ IsOpenImmersion.isoOfRangeEq (Opens.ι _) (pullback.snd _ _) ?_) ?_
  · dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_I₀, Equiv.refl_apply, PreZeroHypercover.pullback₁_X]
    rw [IsOpenImmersion.range_pullbackSnd U.ι (𝒰.f i), Opens.opensRange_ι]
    exact Subtype.range_val
  · intro i
    rw [← cancel_mono U.ι]
    simp [morphismRestrict_ι, Equiv.refl_apply, Category.assoc, pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus (⋃ i ∈ s, {i})

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
i : J
x : F.obj { as := i }
⊢ (ConcreteCategory.hom (F.map (𝟙 { as := i }))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 { as := i }))) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : WidePushoutShape J
x : F.obj i
⊢ (ConcreteCategory.hom (F.map (𝟙 i))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 i))) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) x =
      (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init j))) x ∧
    (ConcreteCategory.hom (F.map (𝟙 none))) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (𝟙 none))) x = x ∧
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) x =
      (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
x : F.obj none
⊢ (ConcreteCategory.hom (F.map (𝟙 none))) x = x ∧ (ConcreteCategory.hom (F.map (𝟙 none))) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ equalizer.lift s.fst ⋯ ≫ equalizer.ι f g = s.fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: 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))
⊢ coequalizer.π f g ≫ coequalizer.desc s.inl ⋯ = s.inl

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
simp

Goal state after: