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

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
obtain ⟨U, hp, s, e⟩ := TopCat.Presheaf.exists_germ_eq _ y
  obtain ⟨_, ⟨r, rfl⟩, hpr : p ∈ PrimeSpectrum.basicOpen r, hrU : PrimeSpectrum.basicOpen r ≤ U⟩ :=
    PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U from hp) U.2
  change PrimeSpectrum.basicOpen r ≤ U at hrU
  replace e :=
    ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
      (homOfLE hrU) p hpr _).trans e
  set s' := (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map
      (homOfLE hrU).op s with h
  replace e : ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).obj).germ _
      p hpr) s' = y := by
    rw [h]; exact e
  clear_value s'; clear! U
  obtain ⟨⟨s, ⟨_, n, rfl⟩⟩, hsn⟩ :=
    @IsLocalization.surj _ _ _ _ _ _
      (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) s'
  refine ⟨⟨s, ⟨r, hpr⟩ ^ n⟩, ?_⟩
  rw [Submonoid.smul_def, Algebra.smul_def, algebraMap_pushforward_stalk, toPushforwardStalk,
    CommRingCat.comp_apply, CommRingCat.comp_apply]
  iterate 2
    erw [← (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
      (homOfLE le_top) p hpr]
  rw [← e]
  let f := TopCat.Presheaf.germ (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _*
      (structureSheaf S).obj) _ p hpr
  rw [← map_mul, mul_comm]
  dsimp only [Subtype.coe_mk] at hsn
  rw [← map_pow (algebraMap R S)] at hsn
  congr 1

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
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        Y.presheaf.map (eqToHom ⋯) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app (op x) =
    s.fst.c.app (op x)

Tactic:
erw [← s.pt.presheaf.map_comp]

Goal state after:
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
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        Y.presheaf.map (eqToHom ⋯) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ (appIso f U).inv ≫ app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op = 𝟙 Γ(X, U)

Tactic:
rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]; rfl

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
s : PullbackCone f g
⊢ IsLimit ((forget C).mapCone (pullbackConeOfLeft f g))

Tactic:
by
      apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan _) _).toFun
      refine (IsLimit.equivIsoLimit ?_).toFun (limit.isLimit (cospan f.base g.base))
      fapply Cone.ext
      · exact Iso.refl _
      change ∀ j, _ = 𝟙 _ ≫ _ ≫ _
      simp_rw [Category.id_comp]
      rintro (_ | _ | _) <;> symm
      · simp only [limit.cone_x, cospan_one, Functor.mapCone_π_app, PullbackCone.condition_one,
        forget_map,
          comp_base, cospan_left, cospan_right, Functor.comp_map, cospan_map_inl, cospan_map_inr,
          diagramIsoCospan_hom_app, PullbackCone.fst_limit_cone]
        tauto
      · exact Category.comp_id _
      · exact Category.comp_id _

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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : R
a : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)

Tactic:
by
    obtain ⟨V, m, i, ra, sa, wa⟩ := ha x
    exact ⟨V, m, i, r • ra, sa, fun x ↦ ⟨(wa x).1,
      congr(r • $((wa x).2)).trans (LocalizedModule.smul'_mk ..)⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
hgy : g ∉ (↑⟨y, ⋯⟩).asIdeal
H : (fun x ↦ ↑s (iVU x)) ⟨y, ⋯⟩ = LocalizedModule.mk f ⟨g, hgy⟩
⊢ ↑(const (g' • f) (g' * g) (basicOpen (g' * g)) ⋯) ⟨y, hy✝⟩ =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s) ⟨y, hy✝⟩

Tactic:
refine (LocalizedModule.mk_eq.mpr ⟨1, ?_⟩).trans H.symm

Goal state after:
case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
hgy : g ∉ (↑⟨y, ⋯⟩).asIdeal
H : (fun x ↦ ↑s (iVU x)) ⟨y, ⋯⟩ = LocalizedModule.mk f ⟨g, hgy⟩
⊢ 1 • ⟨g, hgy⟩ • g' • f = 1 • ⟨g' * g, ⋯⟩ • f
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
R : TopCommRingCat
X : TopCatᵒᵖ
⊢ continuousFunctions.pullback (𝟙 X) R = 𝟙 (continuousFunctions X R)

Tactic:
ext
        rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings ↑(⨆ i, U i)

Tactic:
by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, inferInstance⟩
    obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp x.2
    use i, ⟨x.1, hi⟩
    apply Subtype.ext
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.fromSpec ≫ X.toSpecΓ = Spec.map (X.presheaf.map (homOfLE ⋯).op)

Tactic:
rw [fromSpec, Category.assoc, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top,
    isoSpec_inv_toSpecΓ_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: case init.id
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
⊢ ∀ (xi : F.obj none) (xj : F.obj (some i)),
    (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.init i))) xi =
        (ConcreteCategory.hom (F.map (WidePushoutShape.Hom.id (some i)))) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

Tactic:
simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_eq']
    exact fun x ↦ ⟨_, 𝟙 _, .init _, x, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ ⋯.fromSpec = X.isoSpec.inv

Tactic:
rw [fromSpec, Iso.inv_comp_eq]
  simp [isoSpec_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ↑x ∈ X.basicOpen r
h₂ : X.basicOpen r ≤ V
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
exact ⟨U.topIso.hom.hom r, by simp [Scheme.Opens.toScheme_presheaf_obj, h₁, h₂]⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
by
  rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
⊢ (ConcreteCategory.hom (D.t j i))
      ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k)))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
          ⟨((ConcreteCategory.hom (D.t i j)) x, y), ⋯⟩)) =
    x

Tactic:
pullbackIsoProdSubtype_inv_fst_apply,

Goal state after:
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
⊢ (ConcreteCategory.hom (D.t j i)) (↑⟨((ConcreteCategory.hom (D.t i j)) x, y), ⋯⟩).1 = x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↥X
hs : IsClosed s
⊢ ∃ I, s = X.zeroLocus ↑I

Tactic:
let Z : Set (Spec Γ(X, ⊤)) := X.toΓSpecFun '' s

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
⊢ ∃ I, s = X.zeroLocus ↑I
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: 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))
⊢ IsOpen
    (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)

Tactic:
imageBasicOpen_image_preimage

Goal state after:
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))
⊢ IsOpen (imageBasicOpen f g U s).carrier
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ h.t' i j k ≫ h.t' j k i ≫ h.t' k i j = 𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion')

Tactic:
delta MkCore.t'
    simp_rw [← Category.assoc]
    rw [Iso.comp_inv_eq]
    simp only [Iso.inv_hom_id_assoc, Category.assoc, Category.id_comp]
    rw [← Iso.eq_inv_comp, Iso.inv_hom_id]
    ext1 ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩
    dsimp only [Opens.coe_inclusion', hom_comp, hom_ofHom, ContinuousMap.comp_assoc,
      ContinuousMap.comp_apply, ContinuousMap.coe_mk, hom_id, ContinuousMap.id_apply]
    rw [Subtype.mk_eq_mk, Prod.mk_inj, Subtype.mk_eq_mk, Subtype.ext_iff, and_self_iff]
    convert! congr_arg Subtype.val (h.t_inv k i ⟨x, hx'⟩) using 3
    refine Subtype.ext ?_
    exact h.cocycle i j k ⟨x, hx⟩ hx'

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ ∀ (a : (MultispanShape.prod (ofOpenSubsets U).J).L),
    (ofOpenSubsets U).diagram.fst a ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).fst a)).inclusion' =
      (ofOpenSubsets U).diagram.snd a ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).snd a)).inclusion'

Tactic:
rintro ⟨i, j⟩

Goal state after:
D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i j : (ofOpenSubsets U).J
⊢ (ofOpenSubsets U).diagram.fst (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j))).inclusion' =
    (ofOpenSubsets U).diagram.snd (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j))).inclusion'
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
⊢ ∀ (a : (MultispanShape.prod (ulift 𝒰).gluedCover.J).L),
    (ulift 𝒰).gluedCover.diagram.fst a ≫ f (idx 𝒰 ((MultispanShape.prod (ulift 𝒰).gluedCover.J).fst a)) =
      (ulift 𝒰).gluedCover.diagram.snd a ≫ f (idx 𝒰 ((MultispanShape.prod (ulift 𝒰).gluedCover.J).snd a))

Tactic:
rintro ⟨i, j⟩

Goal state after:
case h
X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
i j : (ulift 𝒰).gluedCover.J
⊢ (ulift 𝒰).gluedCover.diagram.fst (i, j) ≫ f (idx 𝒰 ((MultispanShape.prod (ulift 𝒰).gluedCover.J).fst (i, j))) =
    (ulift 𝒰).gluedCover.diagram.snd (i, j) ≫ f (idx 𝒰 ((MultispanShape.prod (ulift 𝒰).gluedCover.J).snd (i, j)))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
⊢ (ulift 𝒰).fromGlued ≫ f₁ = (ulift 𝒰).fromGlued ≫ f₂

Tactic:
apply Multicoequalizer.hom_ext

Goal state after:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
⊢ ∀ (b : (MultispanShape.prod (ulift 𝒰).gluedCover.J).R),
    Multicoequalizer.π (ulift 𝒰).gluedCover.diagram b ≫ (ulift 𝒰).fromGlued ≫ f₁ =
      Multicoequalizer.π (ulift 𝒰).gluedCover.diagram b ≫ (ulift 𝒰).fromGlued ≫ f₂
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
⊢ p1 𝒰 f g ≫ f = p2 𝒰 f g ≫ g

Tactic:
apply Multicoequalizer.hom_ext

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ ∀ (b : (MultispanShape.prod (gluing 𝒰 f g).J).R),
    Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p1 𝒰 f g ≫ f =
      Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p2 𝒰 f g ≫ g
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
s : PullbackCone f g
⊢ Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
    Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst

Tactic:
apply Multicoequalizer.hom_ext

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ ∀ (b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R),
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
      Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst
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
s : PullbackCone f g
⊢ Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ gluedLift 𝒰 f g s ≫ p2 𝒰 f g =
    Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd

Tactic:
apply Multicoequalizer.hom_ext

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ ∀ (b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R),
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ gluedLift 𝒰 f g s ≫ p2 𝒰 f g =
      Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

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

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

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

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
              ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map (((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)