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

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ ((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
        ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
      ((pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').hom ≫
          ofHom
              {
                toFun := fun x ↦
                  ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
                continuous_toFun := ⋯ } ≫
            (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').inv) ≫
        (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').hom ≫
          ofHom
              {
                toFun := fun x ↦
                  ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
                continuous_toFun := ⋯ } ≫
            (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').inv =
    𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion')

Tactic:
← Category.assoc

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ ((((((((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
                    ofHom
                      {
                        toFun := fun x ↦
                          ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1),
                            ⋯⟩,
                        continuous_toFun := ⋯ }) ≫
                  (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
                (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').hom) ≫
              ofHom
                {
                  toFun := fun x ↦
                    ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
                  continuous_toFun := ⋯ }) ≫
            (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').inv) ≫
          (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').hom) ≫
        ofHom
          {
            toFun := fun x ↦
              ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
            continuous_toFun := ⋯ }) ≫
      (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').inv =
    𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion')
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : (ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩ ∈ U j
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨(ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩, hy⟩

Tactic:
rw [(ofOpenSubsets U).ι_eq_iff_rel]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy : (ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩ ∈ U j
⊢ (ofOpenSubsets U).Rel ⟨i, ⟨x, hx⟩⟩ ⟨j, ⟨(ConcreteCategory.hom (U i).inclusion') ⟨x, hx⟩, hy⟩⟩
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
U : Set ↥D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i) ⁻¹' U)

Tactic:
← (TopCat.homeoOfIso D.isoCarrier.symm).isOpen_preimage,

Goal state after:
D : GlueData
U : Set ↥D.glued
⊢ IsOpen (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U) ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i) ⁻¹' U)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
← Category.assoc

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

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
F : Scheme ⥤ PresheafedSpace CommRingCat :=
  forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
⊢ IsIso (F.map (fromGlued 𝒰))

Tactic:
change IsIso 𝒰.fromGlued.toPshHom

Goal state after:
X : Scheme
𝒰 : X.OpenCover
F : Scheme ⥤ PresheafedSpace CommRingCat :=
  forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
⊢ IsIso (fromGlued 𝒰).toPshHom
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 ⋯ ≫ (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)

Tactic:
← Category.assoc

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
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) ≫ (gluing 𝒰 f g).ι 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 ⋯ ⋯ ≫ (gluing 𝒰 f g).ι j

Tactic:
← Category.assoc

Goal state after:
case hf
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)) ≫
      (gluing 𝒰 f g).ι 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 ⋯ ⋯) ≫
      (gluing 𝒰 f g).ι j
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
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
      Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun i ↦
            (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
              pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι i)
          ⋯ ≫
        p1 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst

Tactic:
← Category.assoc

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
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun i ↦
            ((pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
              (gluing 𝒰 f g).ι i)
          ⋯) ≫
      p1 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ 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
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
      Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun i ↦
            (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
              pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι i)
          ⋯ ≫
        p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd

Tactic:
← Category.assoc

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
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun i ↦
            ((pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
              (gluing 𝒰 f g).ι i)
          ⋯) ≫
      p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
⊢ Set.range ⇑(tAux F i j) ⊆ Set.range ⇑(V F j i).ι

Tactic:
by
    rintro _ ⟨x, rfl⟩
    obtain ⟨l, x, rfl⟩ := (Scheme.Opens.iSupOpenCover _).exists_eq x
    simp only [V, tAux, ← Scheme.Hom.comp_apply, Cover.ι_glueMorphisms]
    simp only [Opens.range_ι, iSup_mk, carrier_eq_coe, Hom.coe_opensRange, coe_mk, Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.comp_apply]
    exact Set.mem_iUnion.mpr ⟨⟨l.1, l.2.2, l.2.1⟩, ⟨_, rfl⟩⟩

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₀
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) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i

Tactic:
← Category.assoc

Goal state after:
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) ⋯) ≫
      (gluing 𝒰 f g).ι i =
    ((pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i
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₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ (gluing 𝒰 f g).openCover.f j

Tactic:
← Category.assoc

Goal state after:
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₀
⊢ (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ (gluing 𝒰 f g).openCover.f j
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✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫
      (pullbackP1Iso 𝒰 f g i).hom ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
        pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i

Tactic:
← Category.assoc

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i =
    ((((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
            pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
          (pullbackSymmetry s.fst (𝒰.f i)).hom) ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h.hU
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U ⊆ Set.range ⇑(ConcreteCategory.hom (D.f i i).base)

Tactic:
rw [Set.range_eq_univ.mpr _]

Goal state after:
case h.hU
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U ⊆ Set.univ

C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (D.f i i).base)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case mp
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f

Tactic:
intro hf ⟨U, hU⟩

Goal state after:
case mp
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
U : Y.Opens
hU : U ∈ Y.affineOpens
⊢ AffineTargetMorphismProperty.of P (f ∣_ ↑⟨U, hU⟩)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f ↔
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
            P ((algebraMap S Sₜ).comp f)

Tactic:
rw [locally_iff_finite P f]
  refine ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun t ht Sₜ _ _ _ ↦ ?_⟩, fun ⟨s, hsone, hs⟩ ↦ ?_⟩
  · let e : Localization.Away t ≃+* Sₜ :=
      (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv
    have : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t)) :=
      RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _) _).symm)
    rw [this, RingHom.comp_assoc]
    exact hP.left _ _ (hs t ht)
  · exact ⟨s, hsone, fun t ht ↦ hs t ht _⟩

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
this : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
⊢ (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)

Tactic:
simp [algebraMap_toAlgebra, IsLocalization.Away.map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g f
⊢ P (pullback.fst g f)

Tactic:
IsZariskiLocalAtSource.iff_of_openCover (P := P) (𝒰.pullback₁ <| pullback.snd g f)

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g f
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰).I₀),
    P ((Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰).f i ≫ pullback.fst g f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this✝² : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
this✝¹ :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H : ∀ (a : ↑s), Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))
this✝ : (a : ↑s) → Algebra S' (Sₐ a) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
a : ↑s
⊢ P ((algebraMap S' (Sₐ a)).comp (IsLocalization.Away.map R' S' f r))

Tactic:
· rw [algebraMap_toAlgebra, IsLocalization.Away.map, IsLocalization.map_comp_map]
    exact hPl ((algebraMap _ (Localization.Away a.val)).comp f) r R' (Sₐ a) (hs _ a.2)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ IsSpectralMap ⇑f

Tactic:
rwa [← quasiCompact_iff_isSpectralMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)

Tactic:
have H : ∀ R A B (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X)
      (iY : Spec B ⟶ Y) (iS : Spec R ⟶ S) (e₁ e₂), IsOpenImmersion iX → IsOpenImmersion iY →
      IsOpenImmersion iS → IsEmbedding (L ∘ pullback.map f' g' f g iX iY iS e₁ e₂) := by
    intro R A B f' g' iX iY iS e₁ e₂ _ _ _
    have H : SurjectiveOnStalks g' :=
      have : SurjectiveOnStalks (g' ≫ iS) := e₂ ▸ inferInstance
      .of_comp _ iS
    obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f' := ⟨_, Spec.map_preimage _⟩
    obtain ⟨ψ, rfl⟩ : ∃ ψ, Spec.map ψ = g' := ⟨_, Spec.map_preimage _⟩
    algebraize [φ.hom, ψ.hom]
    rw [HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks)] at H
    convert!
      ((iX.isOpenEmbedding.prodMap iY.isOpenEmbedding).isEmbedding.comp
            (PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks R A B H)).comp
        (Scheme.homeoOfIso (pullbackSpecIso R A B)).isEmbedding
    ext1 x
    obtain ⟨x, rfl⟩ := (Scheme.homeoOfIso (pullbackSpecIso R A B).symm).surjective x
    simp only [Scheme.homeoOfIso_apply, Function.comp_apply]
    ext
    · simp only [L, ← Scheme.Hom.comp_apply, pullback.lift_fst, Iso.symm_hom,
        Iso.inv_hom_id]
      erw [← Scheme.Hom.comp_apply, pullbackSpecIso_inv_fst_assoc]
      rfl
    · simp only [L, ← Scheme.Hom.comp_apply, pullback.lift_snd, Iso.symm_hom,
        Iso.inv_hom_id]
      erw [← Scheme.Hom.comp_apply, pullbackSpecIso_inv_snd_assoc]
      rfl

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)