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

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
rw [←
      show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j ≫ Multicoequalizer.sigmaπ D.diagram)) y
⊢ D.Rel ((ConcreteCategory.hom ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom)) ⟨i, x⟩) ⟨j, y⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x⟩.fst ⟨j, y⟩.fst)) z = ⟨i, x⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, y⟩.fst ⟨i, x⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, x⟩.fst ⟨j, y⟩.fst)) z) = ⟨j, y⟩.snd
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y

Tactic:
dsimp only at *

Goal state after:
case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i j)) z = x
e₂ : (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) = y
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(𝟙 (Spec Γ(X, ⊤))) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝ = ⟨i, x⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨i, y⟩.fst ⟨i, x⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝) =
    ⟨i, y⟩.snd
⊢ x = y

Tactic:
dsimp only at *

Goal state after:
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i i)) w✝ = x
e₂ : (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝) = y
⊢ x = y
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ X.presheaf.map (eqToHom ⋯) = X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
⊢ (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ ↑x.asIdeal

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

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⟩; ext x; rfl

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
obtain ⟨j, ⟨y, hy⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective y

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
y : ↑(of α)
hy : y ∈ U j
e :
  (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩)
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = (ConcreteCategory.hom ((ofOpenSubsets U).ι j)) ⟨y, hy⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) → x✝ ∈ ⋃ i, ↑(U i)

pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ ⋃ i, ↑(U i) → x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
· rintro ⟨x, rfl⟩
    obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
    rw [ι_fromOpenSubsetsGlue_apply]
    exact Set.subset_iUnion _ i hx'

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ ⋃ i, ↑(U i) → x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j ≫
            D.isoCarrier.inv))
        y ↔
    (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j))
          y)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
U : Set ↥D.glued
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen
      (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ∘
          ⇑(ConcreteCategory.hom
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) ⁻¹'
        U) ↔
    IsOpen
      (⇑(ConcreteCategory.hom
            (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
              D.isoCarrier.inv)) ⁻¹'
        U)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D✝ : GlueData
D : GlueData
⊢ { I₀ := D.J, X := D.U, f := D.ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings D.glued

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
D✝ : GlueData
D : GlueData
⊢ (∀ (x : ↥D.glued), ∃ i, x ∈ Set.range ⇑({ I₀ := D.J, X := D.U, f := D.ι }.f i)) ∧
    ∀ (i : { I₀ := D.J, X := D.U, f := D.ι }.I₀), IsOpenImmersion ({ I₀ := D.J, X := D.U, f := D.ι }.f i)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
rfl

Goal state after:
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)
⊢ Function.LeftInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h.left
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ (ConcreteCategory.hom
        ((TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).π.app WalkingCospan.left))
      ⟨(x, y), h⟩ =
    ⟨i, x⟩.snd

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h.right
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ (ConcreteCategory.hom
        ((TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).π.app WalkingCospan.right))
      ⟨(x, y), h⟩ =
    ⟨j, y⟩.snd

Tactic:
rfl

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 ⋯) =
    (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 ⋯).op ≫
          (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map (eqToHom ⋯) ≫
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map
              ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op)

Tactic:
rfl

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))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k

Tactic:
rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ { I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.I₀),
      IsOpenImmersion ({ I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)
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
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
⊢ ∃ U_1,
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2

Tactic:
let α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
    pullback.lift
      (F.map hli ≫ (F.map k₁.2.1).isoOpensRange.hom)
      (F.map hlj ≫ (F.map k₂.2.1).isoOpensRange.hom)
      (by simp [← cancel_mono (Scheme.Opens.ι _), ← Functor.map_comp,
        Subsingleton.elim (hli ≫ k₁.2.1) (hlj ≫ k₂.2.1)])

Goal state after:
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
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
⊢ ∃ U_1,
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
⊢ ↑(Scheme.Hom.opensRange coprod.inl ⊓ Scheme.Hom.opensRange coprod.inr) = ↑⊥ ∧
      ↑(Scheme.Hom.opensRange coprod.inl ⊔ Scheme.Hom.opensRange coprod.inr) = ↑⊤ ↔
    Set.range ⇑coprod.inl ⊓ Set.range ⇑coprod.inr = ⊥ ∧ Set.range ⇑coprod.inl ⊔ Set.range ⇑coprod.inr = ⊤

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.left ≫ (Iso.refl (BinaryCofan.mk f g).pt).hom = c'.inj WalkingPair.left

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.right ≫ (Iso.refl (BinaryCofan.mk f g).pt).hom = c'.inj WalkingPair.right

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.left }) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.right }) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
b✝ : ι
⊢ Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) b✝)) = Spec.map ((CommRingCat.piFan R).proj b✝)

Tactic:
rfl

Goal state after:
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 ≫
        (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
          (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 ≫
            (opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯) ≫
              eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
rfl

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
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i i).c.app (op U) ≫
      (D.t i i).c.app (op ((Opens.map (D.f i i).base).obj U)) ≫
        invApp (D.f i i) ((Opens.map (D.t i i).base).1 ((Opens.map (D.f i i).base).obj U)) ≫
          (D.U i).presheaf.map (eqToHom ⋯).op =
    (D.U i).presheaf.map (eqToHom ⋯)

Tactic:
rw [congr_app (D.t_id _), id_c_app, ← Functor.map_comp]

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i i).c.app (op U) ≫
      (D.V (i, i)).presheaf.map (𝟙 (op ((Opens.map (D.f i i).base).obj U)) ≫ eqToHom ⋯) ≫
        invApp (D.f i i) ((Opens.map (D.t i i).base).1 ((Opens.map (D.f i i).base).obj U)) ≫
          (D.U i).presheaf.map (eqToHom ⋯).op =
    (D.U i).presheaf.map (eqToHom ⋯)
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 : D.J
U : Opens ↑↑(D.U i)
⊢ (D.U i).presheaf.map
      (eqToHom ⋯ ≫
        (opensFunctor (D.f i i)).op.map (𝟙 (op ((Opens.map (D.f i i).base).obj U)) ≫ eqToHom ⋯) ≫ eqToHom ⋯) =
    (D.U i).presheaf.map (eqToHom ⋯)

Tactic:
rfl

Goal state after:
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✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.fst (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ≫ pullback.fst f (𝒰.f i) =
    pullback.fst
        (pullback.snd f (𝒰.f ((Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm ((Equiv.prodPUnit 𝒰.I₀).symm i)).fst))
        (pullback.snd g (𝒰.f ((Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm ((Equiv.prodPUnit 𝒰.I₀).symm i)).fst)) ≫
      pullback.fst f (𝒰.f ((Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm ((Equiv.prodPUnit 𝒰.I₀).symm i)).fst)

Tactic:
rfl

Goal state after:
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✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.snd (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ≫ pullback.fst g (𝒰.f i) =
    pullback.snd
        (pullback.snd f (𝒰.f ((Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm ((Equiv.prodPUnit 𝒰.I₀).symm i)).fst))
        (pullback.snd g (𝒰.f ((Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm ((Equiv.prodPUnit 𝒰.I₀).symm i)).fst)) ≫
      pullback.fst g (𝒰.f ((Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm ((Equiv.prodPUnit 𝒰.I₀).symm i)).fst)

Tactic:
rfl

Goal state after:
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
inst✝ : Small.{u, w} J
s : Cocone F
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : J), (cocone F).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).J).R
⊢ Multicoequalizer.π (glueData F).diagram i ≫ m = (glueData F).ι i ≫ m

Tactic:
rfl

Goal state after: