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

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j

Tactic:
rw [← 𝖣.t_fac_assoc]

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = D.t' j i k ≫ pullback.snd (D.f i k) (D.f i j) ≫ D.f i j
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.t i k ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j

Tactic:
rw [← 𝖣.t_fac_assoc]

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
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.lift I (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop)) hI))) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) =
    f

Tactic:
Category.assoc,

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)) ≫
        Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) =
    f
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) ≫
      pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

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) ≫
        pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j
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) ≫
        pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

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 ≫
          pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case h
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion') ⊆
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∧
    IsOpen[inst✝]
        (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')) ∧
      (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
        ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')

Tactic:
use Set.inter_subset_left

Goal state after:
case right
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ IsOpen[inst✝]
      (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')) ∧
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
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))
this : pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U

Tactic:
rw [← IsIso.inv_comp_eq] at this

Goal state after:
case w
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))
this : inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = pullback.snd (D.f i j) (D.f i k)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.refine_1
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))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
x : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (D.t' k i j).base) ((TopCat.Hom.hom (inv (D.t' k i j)).base) x) = x

Tactic:
rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
        ConcreteCategory.id_apply]

Goal state after:
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)) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)) ≫
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op 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)) ≫
      (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯) ≫
        (D.t' k i j).c.app (op U) ≫
          invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ ⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x)) ⊆ ⇑(fromGlued 𝒰) '' U ∧
    IsOpen (⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x))) ∧ x ∈ ⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x))

Tactic:
use Set.inter_subset_left

Goal state after:
case right
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ IsOpen (⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x))) ∧ x ∈ ⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x))
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

Tactic:
Category.assoc,

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

Goal state before:
pp: X : Scheme
𝒰 : 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
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) ((ulift 𝒰).f i) ≫ ((ulift 𝒰).gluedCover.ι i ≫ (ulift 𝒰).fromGlued) ≫ glueMorphisms 𝒰 f hf =
    pullback.fst (𝒰.f x) ((ulift 𝒰).f i) ≫ f x

Tactic:
Category.assoc,

Goal state after:
X : Scheme
𝒰 : 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
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift 𝒰)).I₀
⊢ pullback.snd (𝒰.f x) ((ulift 𝒰).f i) ≫ (ulift 𝒰).gluedCover.ι i ≫ (ulift 𝒰).fromGlued ≫ glueMorphisms 𝒰 f hf =
    pullback.fst (𝒰.f x) ((ulift 𝒰).f i) ≫ f x
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 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:
Category.assoc,

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 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.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
Category.assoc,

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.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)
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.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g

Tactic:
Category.assoc,

Goal state after:
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.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.fst (𝒰.f i ≫ f) g =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.fst (𝒰.f i ≫ 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 j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
Category.assoc,

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.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.snd (𝒰.f i ≫ 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 j k : 𝒰.I₀
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)

Tactic:
Category.assoc,

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.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)
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
i : 𝒰.I₀
⊢ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f = (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g

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
i : 𝒰.I₀
⊢ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f = pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g
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 ⋯) =
    ((pullback.snd (D.f j i) (D.f j k)).c.app
          (op
            ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
              ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
        (pullback (D.f j i) (D.f j k)).presheaf.map (eqToHom ⋯)) ≫
      (pullbackSymmetry (D.f j k) (D.f j i)).hom.c.app
          (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).obj U)) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f j k) (D.f j i))
              ((Opens.map (D.t' j k i).base).1
                ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
Category.assoc,

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 ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.snd (D.f j i) (D.f j k)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
      (pullback (D.f j i) (D.f j k)).presheaf.map (eqToHom ⋯) ≫
        (pullbackSymmetry (D.f j k) (D.f j i)).hom.c.app
            (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).obj U)) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                  (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 ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    ((pullback.fst (D.f j k) (D.f j i)).c.app
          (op
            ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
              ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
              (pullback (D.f j k) (D.f j i)).presheaf).map
          (eqToHom ⋯) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f j k) (D.f j i))
              ((Opens.map (D.t' j k i).base).1
                ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
Category.assoc,

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 ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                (pullback (D.f j k) (D.f j i)).presheaf).map
            (eqToHom ⋯) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)