mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case some.right
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun x ↦
      Option.casesOn (motive := fun t ↦
        x = t →
          ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
        x (fun h ↦ ⋯ ▸ D.gluedIso F)
        (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
    ⋯
⊢ ((D.mapGlueData F).vPullbackCone i j).π.app (some WalkingPair.right) = F.map (D.t i j) ≫ F.map (D.f j i)

Tactic:
;

Goal state after:
case some.right
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun x ↦
      Option.casesOn (motive := fun t ↦
        x = t →
          ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
        x (fun h ↦ ⋯ ▸ D.gluedIso F)
        (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
    ⋯
⊢ ((D.mapGlueData F).vPullbackCone i j).π.app (some WalkingPair.right) = F.map (D.t i j) ≫ F.map (D.f j i)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
⊢ Mono (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
⊢ Mono (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h)
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 (eqToHom ⋯)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i : D.J
⊢ IsIso (eqToHom ⋯)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
Y Z : C
f : Z ⟶ Y
⊢ eqToHom ⋯ ≫ f ≍ f

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
Y Z : C
f : Z ⟶ Y
⊢ eqToHom ⋯ ≫ f ≍ f
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
hij : ¬i = j
⊢ IsIso (pullback.snd (D.f' j i) (D.f' j i))

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
hij : ¬i = j
⊢ IsIso (pullback.snd (D.f' j i) (D.f' j i))
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i k h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i k h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j k h

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j k h
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j i h

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j i h
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 = D.t' j i k ≫ pullback.snd (D.f i k) (D.f i j) ≫ D.f i j

Tactic:
;

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: case e_a
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)
⊢ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.snd (D.f i k) (D.f i j) ≫ D.f i j

Tactic:
;

Goal state after:
case e_a
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)
⊢ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.snd (D.f i k) (D.f i j) ≫ D.f i j
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
x✝² x✝¹ : Discrete ι
j : ι
x✝ : { as := j } ⟶ { as := j }
⊢ F.map { down := { down := ⋯ } } ≫ homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ =
    homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ ≫
      ((Functor.const (Discrete ι)).obj (coproduct F)).map { down := { down := ⋯ } }

Tactic:
;

Goal state after:
ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
x✝² x✝¹ : Discrete ι
j : ι
x✝ : { as := j } ⟶ { as := j }
⊢ F.map { down := { down := ⋯ } } ≫ homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ =
    homMk (colimit.ι (F ⋙ forgetToSheafedSpace) { as := j }) ⋯ ≫
      ((Functor.const (Discrete ι)).obj (coproduct F)).map { down := { down := ⋯ } }
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case h
D : GlueData
h : MkCore
i j : h.J
⊢ h.t i j ≫ h.t j i = 𝟙 ((Opens.toTopCat (h.U i)).obj (h.V i j)) ∧
    h.t j i ≫ h.t i j = 𝟙 ((Opens.toTopCat (h.U j)).obj (h.V j i))

Tactic:
;

Goal state after:
case h
D : GlueData
h : MkCore
i j : h.J
⊢ h.t i j ≫ h.t j i = 𝟙 ((Opens.toTopCat (h.U i)).obj (h.V i j)) ∧
    h.t j i ≫ h.t i j = 𝟙 ((Opens.toTopCat (h.U j)).obj (h.V j i))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case h.left
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i j))
⊢ (ConcreteCategory.hom (h.t i j ≫ h.t j i)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U i)).obj (h.V i j)))) x✝

pp: case h.right
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U j)).obj (h.V j i))
⊢ (ConcreteCategory.hom (h.t j i ≫ h.t i j)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U j)).obj (h.V j i)))) x✝

Tactic:
;

Goal state after:
case h.left
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i j))
⊢ (ConcreteCategory.hom (h.t i j ≫ h.t j i)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U i)).obj (h.V i j)))) x✝

case h.right
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U j)).obj (h.V j i))
⊢ (ConcreteCategory.hom (h.t j i ≫ h.t i j)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U j)).obj (h.V j i)))) x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i i))
⊢ (ConcreteCategory.hom (h.t i i)) x✝ =
    (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U (i, i).1)).obj (h.V (i, i).1 (i, i).2)))) x✝

Tactic:
;

Goal state after:
D : GlueData
h : MkCore
i : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i i))
⊢ (ConcreteCategory.hom (h.t i i)) x✝ =
    (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U (i, i).1)).obj (h.V (i, i).1 (i, i).2)))) x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i i))
⊢ id x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U (i, i).1)).obj (h.V (i, i).1 (i, i).2)))) x✝

Tactic:
;

Goal state after:
D : GlueData
h : MkCore
i : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i i))
⊢ id x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U (i, i).1)).obj (h.V (i, i).1 (i, i).2)))) x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
x✝ : ↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i)))
⊢ (ConcreteCategory.hom (ofHom { toFun := fun x ↦ ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ })) x✝ = id x✝

Tactic:
;

Goal state after:
D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
x✝ : ↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i)))
⊢ (ConcreteCategory.hom (ofHom { toFun := fun x ↦ ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ })) x✝ = id x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: 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'

Tactic:
;

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.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i j : (ofOpenSubsets U).J
x : ↑((ofOpenSubsets U).diagram.left (i, j))
⊢ (ConcreteCategory.hom
        ((ofOpenSubsets U).diagram.fst (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j))).inclusion'))
      x =
    (ConcreteCategory.hom
        ((ofOpenSubsets U).diagram.snd (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j))).inclusion'))
      x

Tactic:
;

Goal state after:
D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i j : (ofOpenSubsets U).J
x : ↑((ofOpenSubsets U).diagram.left (i, j))
⊢ (ConcreteCategory.hom
        ((ofOpenSubsets U).diagram.fst (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j))).inclusion'))
      x =
    (ConcreteCategory.hom
        ((ofOpenSubsets U).diagram.snd (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j))).inclusion'))
      x
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
R S : C
f : R ⟶ S
⊢ (preservesTerminalIso (pullback f)).hom = (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯).hom

Tactic:
;

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
R S : C
f : R ⟶ S
⊢ (preservesTerminalIso (pullback f)).hom = (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯).hom
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv)

Tactic:
;

Goal state after:
D : GlueData
i : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i).base ≫
      (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base

Tactic:
← PresheafedSpace.comp_base,

Goal state after:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i ≫
        D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ ((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData LocallyRingedSpace.forgetToSheafedSpace).ι i).hom.base ≫
        D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv.hom.base) ≫
      (LocallyRingedSpace.forgetToSheafedSpace.map D.isoLocallyRingedSpace.inv).hom.base =
    (D.ι i).base

Tactic:
← PresheafedSpace.comp_base,

Goal state after:
D : GlueData
i : D.J
⊢ ((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData LocallyRingedSpace.forgetToSheafedSpace).ι i).hom ≫
          D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv.hom).base ≫
      (LocallyRingedSpace.forgetToSheafedSpace.map D.isoLocallyRingedSpace.inv).hom.base =
    (D.ι i).base
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
by
                delta IsOpenImmersion.opensFunctor IsOpenEmbedding.functor
                dsimp only [Functor.op, IsOpenMap.functor, Opens.map, unop_op]
                congr
                apply pullback_base

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f z) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
;

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f z) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)

Tactic:
;

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
;

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)

Tactic:
;

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
;

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