mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan f g)).hom ≫ limit.π (cospan f g ⋙ forget) right)

Tactic:
← 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 ≫
      (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))).hom ≫ limit.π (cospan f.hom g.hom) right)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V =
    (Scheme.Hom.appIso g V).inv ≫
      Scheme.Hom.app g (g ''ᵁ V) ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op

Tactic:
Scheme.Hom.appIso_inv_app_assoc,

Goal state after:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = U.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.app f (g ⁻¹ᵁ g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op
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
⊢ PresheafedSpace.IsOpenImmersion (pullback.fst g f).hom

Tactic:
← 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
⊢ 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 Z✝ : Scheme
f✝ : X ⟶ Z✝
g✝ : Y ⟶ Z✝
H : IsOpenImmersion f✝
Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
H' : Set.range ⇑g ⊆ Set.range ⇑f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (lift f g H' ≫ f)

Tactic:
simpa

Goal state after:
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
⊢ PresheafedSpace.IsOpenImmersion ((preservesLimitIso forget (cospan g f)).hom ≫ limit.π (cospan g f ⋙ forget) left)

Tactic:
← 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 ≫
      (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))).hom ≫ limit.π (cospan g.hom f.hom) left)
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
⊢ IsIso
    (limit.π
      (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
        ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (H.functor.obj U)))
      (op i))

Tactic:
apply limit_π_isIso_of_is_strict_terminal

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 ι)ᵒᵖ) →
    j ≠ op i →
      IsTerminal
        ((PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
              ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (H.functor.obj U))).obj
          j)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Y.restrict ⋯ ⟶ X

Tactic:
use PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.1 g.1

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),
    IsLocalHom
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
i : s
hi : x ∈ U i
⊢ x ∈ Set.range ⇑({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)

Tactic:
simpa

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 : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
this : V.ι ''ᵁ ?m.39 ≤ U.ι ''ᵁ W
⊢ ⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))) ≤ ⋯.functor.obj (unop (op W))

Tactic:
simpa

Goal state after:
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
⊢ Set.range ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι) = Set.range ⇑U.ι

Tactic:
have : V.ι ''ᵁ (V.ι ⁻¹ᵁ U) = U := by simpa [Scheme.Hom.image_preimage_eq_opensRange_inf]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.range ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι) = Set.range ⇑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.ι ⁻¹ᵁ U).ι = ↑U

Tactic:
← this

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ U ⊓ W = U

Tactic:
simpa

Goal state after:
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
⊢ g ↑j ^ (N + 1) • g ↑i ^ N • f ↑i = g ↑i ^ (N + 1) • g ↑j ^ N • f ↑j

Tactic:
convert_to (g i * g ↑j) ^ N • g j • f i = (g i * g ↑j) ^ N • g i • f j

Goal state after:
case e'_2
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 * g ↑j) ^ N • g ↑j • f ↑i

case e'_3
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 ↑i ^ (N + 1) • g ↑j ^ N • f ↑j = (g ↑i * g ↑j) ^ N • g ↑i • f ↑j

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 ↑i * g ↑j) ^ N • g ↑j • f ↑i = (g ↑i * g ↑j) ^ N • g ↑i • 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:
simp only [Set.mem_preimage, SetLike.mem_coe]

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

Goal state before:
pp: ⊢ PreservesLimits forgetToScheme

Tactic:
apply +allowSynthFailures @preservesLimits_of_natIso _ _ _ _ _ _
    (Functor.isoWhiskerRight equivCommRingCat.unitIso forgetToScheme).symm
  change PreservesLimits (equivCommRingCat.functor ⋙ Scheme.Spec)
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
⊢ IsUnit ((ConcreteCategory.hom (toStalk R x)) f)

Tactic:
convert! (isUnit_basicOpen f).map ((structurePresheafInCommRingCat R).germ _ x hf).hom
  exact ((structurePresheafInCommRingCat R).germ_res_apply (homOfLE (le_top : basicOpen f ≤ ⊤))
    x hf (algebraMap R Γ(R, ⊤) f)).symm

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
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ ↑s •
      (IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
          (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯)
        (LocalizedModule.mk f s) =
    ↑s •
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
        (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
rw [← map_smul, LocalizedModule.smul'_mk, ← Submonoid.smul_def, LocalizedModule.mk_cancel,
    ← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply, ← map_smul,
    ← toOpenₗ_germ (basicOpen ↑s) _ s.2, smul_const]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (toOpenₗ R M (basicOpen ↑s)) ≫ (structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      f =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯))
      (const (↑s • f) (↑s) (basicOpen ↑s) ⋯)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
      inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y) =
    PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)))

Tactic:
← this

Goal state after:
ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
      inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y) =
    PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap ((forgetToSheafedSpace.mapCocone s).ι.app i).hom y) ≫
        inv (PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ (Opens.map f.base).obj (imageBasicOpen f g U s) = (Opens.map g.base).obj (imageBasicOpen f g U s)

Tactic:
delta imageBasicOpen

Goal state after:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ (Opens.map f.base).obj
      (Y.toRingedSpace.basicOpen
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this)) =
    (Opens.map g.base).obj
      (Y.toRingedSpace.basicOpen
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this))
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
⊢ D.t'' i j k ≫ D.t'' j k i ≫ D.t'' k i j = 𝟙 (pullback (D.f' i j) (D.f' i k))

Tactic:
delta GlueData'.t''
    if hij : i = j then
      subst hij
      if hik : i = k then
        subst hik
        ext <;> simp
      else
        simp [hik, Ne.symm hik, fst_eq_snd_of_mono_eq]
    else if hik : i = k then
      subst hik
      ext <;> simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq, pullback.condition_assoc]
    else if hjk : j = k then
      subst hjk
      ext <;> simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq]
    else
      ext <;> simp [hij, Ne.symm hij, hik, Ne.symm hik, hjk, Ne.symm hjk,
        pullback.map_comp_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
⊢ ∃ I, s = X.zeroLocus ↑I

Tactic:
have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs

Goal state after:
case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
⊢ ∃ I, s = X.zeroLocus ↑I
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
this : (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ ↑x.asIdeal
⊢ x ∈ ⇑hU.fromSpec ⁻¹' X.zeroLocus s ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
by
    simpa [← hU.fromSpec_image_basicOpen, -not_not] using! this

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ X.toSpecΓ ≫
      Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk I) ≫
          CommRingCat.ofHom (Ideal.Quotient.lift I (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop)) hI)) =
    f

Tactic:
← CommRingCat.ofHom_comp,

Goal state after:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ X.toSpecΓ ≫
      Spec.map
        (CommRingCat.ofHom
          ((Ideal.Quotient.lift I (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop)) hI).comp (Ideal.Quotient.mk I))) =
    f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) := ((ΓSpec.adjunction.homEquiv X (op A)).symm f).unop
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
⊢ Function.Injective ⇑(ConcreteCategory.hom ((Scheme.ΓSpecIso (specTargetImage f)).hom ≫ φ'))

Tactic:
apply (RingHom.kerLift_injective φ.hom).comp

Goal state after:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) := ⋯
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := ⋯
⊢ Function.Injective ⇑(Scheme.ΓSpecIso (specTargetImage f)).hom.hom'
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))

Tactic:
rw [bijective_iff_isIso_ofHom]

Goal state after:
case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ IsIso (↾⇑(ConcreteCategory.hom (D.t i j)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
⊢ op (⋯.functor.obj (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U)))))) =
    (Opens.map (D.f i k).base).op.obj (op (⋯.functor.obj U))

Tactic:
dsimp only [Functor.op, IsOpenMap.functor, Opens.map, unop_op]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
⊢ op
      {
        carrier :=
          ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) ''
            ↑((↑(TopCat.Hom.frameHom (pullback.fst (D.f i j) (D.f i k)).base)).toFunctor.1 U),
        is_open' := ⋯ } =
    op
      ((↑(TopCat.Hom.frameHom (D.f i k).base)).toFunctor.obj
        { carrier := ⇑(ConcreteCategory.hom (D.f i j).base) '' ↑U, is_open' := ⋯ })
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
· apply pullback.hom_ext
    · rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, Category.assoc, t_fst_fst]
    · simp only [Category.assoc, t_fst_snd]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
· simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst (𝒰.f j) s.fst =
    pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f j ≫ f) g

Tactic:
pullback.lift_fst,

Goal state after:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst (𝒰.f j) s.fst = pullback.fst (𝒰.f j) s.fst ≫ 𝟙 (𝒰.X j)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j))

Tactic:
exact D.opensImagePreimageMap i j U

Goal state after: