mathlib-initiative/mathlib-tactics huggingface dataset:
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))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f)

Tactic:
convert! this

Goal state after:
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))
⊢ ⇑((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f) =
    ⇑((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))
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
t : ↑(F.presheaf.obj U)
⊢ t * s = 0 → t = 0

Tactic:
e

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)
e : t * s = 0
⊢ t = 0
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
e : U = V
⊢ Set.range ⇑U.ι = Set.range ⇑V.ι

Tactic:
e

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
e : U = V
⊢ Set.range ⇑V.ι = Set.range ⇑V.ι
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 ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g

Tactic:
← pullback.condition,

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 ≫ V.ι = pullback.fst f g ≫ f
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
inst✝ : IsOpenImmersion f
⊢ IsOpenImmersion (f ∣_ U)

Tactic:
delta morphismRestrict
  exact PresheafedSpace.IsOpenImmersion.comp _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ X.homOfLE i ≫ resLE f U V e = resLE f U V' ⋯

Tactic:
simp_rw [← resLE_id, resLE_comp_resLE, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
⊢ X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)

Tactic:
e

Goal state after:
X Y : Scheme
inst✝ : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
⊢ X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)
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:
by
  dsimp; infer_instance

Goal state after:
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))
⊢ X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Tactic:
refine LocallyRingedSpace.forgetToSheafedSpace.map_injective
    (Spec.basicOpen_hom_ext w ?_)
  intro r U
  erw [SheafedSpace.comp_hom_c_app, toOpen_comp_comap_assoc]
  dsimp
  rw [Category.assoc]
  erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]
  exact h r

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op ⊤) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
⊢ CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤) =
    𝟙 (Γ.obj (op X))

Tactic:
convert! this

Goal state after:
case e'_3
X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op ⊤) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
e_1✝ :
  (Γ.obj (op X) ⟶ ((pushforward CommRingCat X.toΓSpec.base).obj X.presheaf).obj (op ⊤)) =
    (CommRingCat.of ↑(Γ.obj (op X)) ⟶
      ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).obj (op ⊤))
⊢ 𝟙 (Γ.obj (op X)) = X.presheaf.map ((Opens.map X.toΓSpecBase).obj ⊤).leTop.op
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
convert! this

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
⊢ ⇑((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f) =
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₃ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) ≫ D.f i i = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom

Tactic:
← pullback.condition,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₃ : D.t' i i j ≫ pullback.fst (D.f i j) (D.f i i) ≫ D.f i j = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
have := D.cocycle i j i

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this : D.t' i j i ≫ D.t' j i i ≫ D.t' i i j = 𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ (Spec R).toSpecΓ = 𝟙 (Spec Γ(Spec R, ⊤))

Tactic:
← SpecMap_ΓSpecIso_hom,

Goal state after:
R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ Spec.map (Scheme.ΓSpecIso R).hom = 𝟙 (Spec Γ(Spec R, ⊤))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)

Tactic:
← SpecMap_ΓSpecIso_hom,

Goal state after:
R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
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 : D.J
⊢ IsIso (D.f' i i)

Tactic:
simp only [↓reduceDIte, GlueData'.f']; infer_instance

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := ⋯ }
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)

Tactic:
have V_open : IsOpen ((coequalizer.π f.toShHom g.toShHom).hom.base '' V.1) :=
    imageBasicOpen_image_open f g U s

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier)
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)
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.Hom.appTop (specTargetImageFactorization f)))

Tactic:
change Function.Injective <| ((ΓSpec.adjunction.homEquiv X _) φ'.op).appTop

Goal state after:
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.Hom.appTop ((ΓSpec.adjunction.homEquiv X (op (specTargetImage f))) φ'.op)))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x y : ↑(ofOpenSubsets U).glued
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x = (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y → x = y

Tactic:
e

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x y : ↑(ofOpenSubsets U).glued
e : (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x = (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y
⊢ x = y
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ IsOpenImmersion (D.ι i)

Tactic:
IsOpenImmersion,

Goal state after:
D : GlueData
i : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (Hom.toLRSHom (D.ι i))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
⊢ U ≤ ⊥

Tactic:
x

Goal state after:
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(∐ g)
⊢ x ∈ U → x ∈ ⊥
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
erw [← (D.V (j, k)).presheaf.map_comp]

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf.e_a.h₀
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₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f j ≫ f) g

Tactic:
rw [t_fst_fst, gluedLiftPullbackMap_snd]

Goal state after:
case hf.e_a.h₀
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.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.snd s.fst (𝒰.f j) =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f j ≫ f) g
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₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.f i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp_rw [t_fst_snd, pullback.lift_snd, pullbackFstιToV_fst_assoc, pullback.condition_assoc,
        GlueData.openCover_f, p2]

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₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫
      (gluing 𝒰 f g).ι j ≫ Multicoequalizer.desc (gluing 𝒰 f g).diagram Y (fun i ↦ pullback.snd (𝒰.f i ≫ f) g) ⋯ =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
U : (X ⨿ Y).Opens
⊢ (coprodPresheafObjIso U).hom ≫ prod.fst = Hom.app coprod.inl U

Tactic:
by
  simp [coprodPresheafObjIso, Hom.appIso_hom, ← Functor.map_comp, Subsingleton.elim _ (𝟙 _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
U : (X ⨿ Y).Opens
⊢ (coprodPresheafObjIso U).hom ≫ prod.snd = Hom.app coprod.inr U

Tactic:
by
  simp [coprodPresheafObjIso, Hom.appIso_hom, ← Functor.map_comp, Subsingleton.elim _ (𝟙 _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.snd (𝒰.f i ≫ f) g = pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g

Tactic:
by
  simp_rw [pullbackP1Iso, pullback.lift_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
by
  simp_rw [pullbackP1Iso, pullback.lift_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Finite ↥X
inst✝ : DiscreteTopology ↥X
this : IsAffineOpen (⨆ x, { carrier := {x}, is_open' := ⋯ })
⊢ IsAffineOpen ⊤

Tactic:
convert! this

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Finite ↥X
inst✝ : DiscreteTopology ↥X
this : IsAffineOpen (⨆ x, { carrier := {x}, is_open' := ⋯ })
⊢ ⊤ = ⨆ x, { carrier := {x}, is_open' := ⋯ }
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ⊤ ≤ ⨆ x, V x

Tactic:
rintro x -

Goal state after:
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ x ∈ ⨆ x, V x
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q (pullback.snd f (𝟙 Y) ≫ 𝟙 Y) ↔ Q f

Tactic:
← pullback.condition,

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q (pullback.fst f (𝟙 Y) ≫ f) ↔ Q f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.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.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))

Tactic:
simp_rw [Category.assoc]
    rw [Category.id_comp]
    apply π_ιInvApp_π

Goal state after: