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

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen 1)))) ≫
        X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen 1)) ≫
          ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
            ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.Γgerm x

Tactic:
← Category.assoc,

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ ((CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)))
              ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen 1)))) ≫
          X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen 1))) ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.Γgerm x
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      (Γ.rightOp.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f)).unop ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
← Category.assoc,

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ ((locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
        (Γ.rightOp.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f)).unop) ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = (pullback.fst (D.f j i) (D.f j i) ≫ D.t j i) ≫ inv (pullback.snd (D.f i i) (D.f i j))
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = (pullback.fst (D.f j i) (D.f j i) ≫ D.t j i) ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
← D.t_fac

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j) ≫ inv (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
D : GlueData C
i j : D.J
⊢ D.t' i j i = (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j) ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
← D.t_fac

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = (D.t' i j i ≫ pullback.snd (D.f j i) (D.f j i)) ≫ inv (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
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  D.t i j ≫ D.t j i ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  (D.t i j ≫ D.t j i) ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨PrimeSpectrum.comap σ p, ⋯⟩ ∈ W
iWU : W ⟶ U
a : M
b : R
h_frac : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), (fun x ↦ s (iWU x)) x = LocalizedModule.mk a ⟨b, hs⟩
⊢ ∀ (x : ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ } ⊓ V)),
    ∃ (hs : σ b ∉ (↑x).asIdeal),
      (fun x ↦
            comapFun f U V hUV s (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }.infLERight V) x))
          x =
        LocalizedModule.mk (f a) ⟨σ b, hs⟩

Tactic:
rintro ⟨q, ⟨hqW, hqV⟩⟩

Goal state after:
R M : Type u
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M ↑x
hs : (isLocallyFraction R M).pred s
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : ↑(PrimeSpectrum.Top S)
hpV : p ∈ V
W : Opens ↑(PrimeSpectrum.Top R)
m : ↑⟨PrimeSpectrum.comap σ p, ⋯⟩ ∈ W
iWU : W ⟶ U
a : M
b : R
h_frac : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), (fun x ↦ s (iWU x)) x = LocalizedModule.mk a ⟨b, hs⟩
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }
hqV : q ∈ ↑V
⊢ ∃ (hs : σ b ∉ (↑⟨q, ⋯⟩).asIdeal),
    (fun x ↦ comapFun f U V hUV s (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }.infLERight V) x))
        ⟨q, ⋯⟩ =
      LocalizedModule.mk (f a) ⟨σ b, hs⟩
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
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
by
  if hij : i = j then
    apply +allowSynthFailures hasPullback_of_left_iso
    simp only [GlueData'.f', dif_pos hij]
    infer_instance
  else if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
subst eq₁ eq₂ e₁ e₃ e₄

Goal state after:
case h
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)
⊢ (ConcreteCategory.hom (D.f i k))
        ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z)) =
      (ConcreteCategory.hom (D.f 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 k i))
        ((ConcreteCategory.hom (D.t i k))
          ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z))) =
      (ConcreteCategory.hom (D.f k j))
        ((ConcreteCategory.hom (D.t j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ Ideal.span s = ⊤

Tactic:
trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ
  · trans hU.fromSpec ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 = hU.fromSpec ⁻¹' U.1
    · refine ⟨fun h => by rw [h], ?_⟩
      intro h
      apply_fun Set.image hU.fromSpec at h
      rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec]
        at h
      simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
      ext1
      refine Set.Subset.antisymm ?_ h
      simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
      intro x _
      exact X.basicOpen_le x
    · simp only [Opens.iSup_def, Set.preimage_iUnion]
      congr! 1
      · refine congr_arg (Set.iUnion ·) ?_
        ext1 x
        exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)
      · exact congr_arg Opens.carrier hU.fromSpec_preimage_self
  · simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
    rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
      PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]
    simp only [Set.iUnion_singleton_eq_range, Subtype.range_val_subtype, Set.ofPred_mem_eq]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(ConcreteCategory.hom
          (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)) ≫
            (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g)).hom)) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)

Tactic:
PreservesCoequalizer.iso_hom,

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(ConcreteCategory.hom
          (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)) ≫
            coequalizerComparison (Hom.toShHom f) (Hom.toShHom g) (SheafedSpace.forget CommRingCat))) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x₁ : ↑(D.U i)
x₂ : ↑(D.U j)
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = (ConcreteCategory.hom (D.ι i)) x₁
⊢ (ConcreteCategory.hom (D.ι i)) x₁ ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
exact ⟨y, by simp [e₁]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (𝟙 ((pullback f).obj (R ⊗ S))) ≫ pullback.snd (R ⊗ S).hom f =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f

Tactic:
simp [CartesianMonoidalCategory.prodComparison]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ pullback.snd (pullback.fst gA gB ≫ gA) f =
    Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).hom ≫
      pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f

Tactic:
simp [CartesianMonoidalCategory.prodComparison]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case left
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : ↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat
j : (D.U i).affineCover.I₀
z : ↥((D.U i).affineCover.X j)
hz : ((D.U i).affineCover.f j) z = y
⊢ (ConcreteCategory.hom (D.toLocallyRingedSpaceGlueData.ι i).base) y ∈
    Set.range ⇑(ConcreteCategory.hom (Hom.toLRSHom ((D.U i).affineCover.f j) ≫ D.toLocallyRingedSpaceGlueData.ι i).base)

pp: case right
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : ↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat
j : (D.U i).affineCover.I₀
z : ↥((D.U i).affineCover.X j)
hz : ((D.U i).affineCover.f j) z = y
⊢ LocallyRingedSpace.IsOpenImmersion (Hom.toLRSHom ((D.U i).affineCover.f j) ≫ D.toLocallyRingedSpaceGlueData.ι i)

Tactic:
· simp only [LocallyRingedSpace.comp_toHom, PresheafedSpace.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]
    exact Set.mem_image_of_mem _ ⟨z, hz⟩

Goal state after:
case right
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : ↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat
j : (D.U i).affineCover.I₀
z : ↥((D.U i).affineCover.X j)
hz : ((D.U i).affineCover.f j) z = y
⊢ LocallyRingedSpace.IsOpenImmersion (Hom.toLRSHom ((D.U i).affineCover.f j) ≫ D.toLocallyRingedSpaceGlueData.ι i)
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
← Category.assoc,

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:
← Category.assoc,

Goal state after:
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
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:
delta IsOpenImmersion.opensFunctor IsOpenEmbedding.functor

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
⊢ op (⋯.functor.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 (⋯.functor.obj U))
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))
⊢ (Opens.map (D.t k i).base).op.obj (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    op
      ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj
        (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))

Tactic:
delta IsOpenImmersion.opensFunctor IsOpenEmbedding.functor

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))
⊢ (Opens.map (D.t k i).base).op.obj (op (⋯.functor.obj U)) =
    op (⋯.functor.obj (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : (Sigma.ι g i) x ∈ U
y : ↥(g j)
hy : (Sigma.ι g j) y = (Sigma.ι g i) x
⊢ (Sigma.ι g i) x ∈ ⊥

Tactic:
obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy

Goal state after:
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i : σ
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
x : ↥(g i)
hx : (Sigma.ι g i) x ∈ U
h : i ≠ i
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hy : (Sigma.ι g i) x = (Sigma.ι g i) x
⊢ (Sigma.ι g i) x ∈ ⊥
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e : (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨iy, y⟩
⊢ (α ix) x = (α iy) y

Tactic:
simpa [← Scheme.Hom.comp_apply] using e

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
i j k : Shrink.{u, w} J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [t]

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
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ F.map f ≫ (glueData F).ι j = (glueData F).ι i

Tactic:
← cancel_epi (V F ↓i ↓j).ι,

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
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ (V F (↓i) ↓j).ι ≫ F.map f ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData 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
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ (V F (↓i) ↓j).ι ≫ F.map f ≫ (glueData F).ι j = tAux F (↓i) ↓j ≫ (glueData F).ι j

Tactic:
← Category.assoc,

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
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ ((V F (↓i) ↓j).ι ≫ F.map f) ≫ (glueData F).ι j = tAux F (↓i) ↓j ≫ (glueData F).ι j
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
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ ((V F (↓i) ↓j).ι ≫ (Hom.isoOpensRange (F.map (𝟙 ↓i))).hom ≫ (F.obj ↓i).homOfLE ⋯ ≫ tAux F (↓i) ↓j) ≫
      (glueData F).ι j =
    tAux F (↓i) ↓j ≫ (glueData F).ι j

Tactic:
← Category.assoc,

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
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ (((V F (↓i) ↓j).ι ≫ (Hom.isoOpensRange (F.map (𝟙 ↓i))).hom) ≫ (F.obj ↓i).homOfLE ⋯ ≫ tAux F (↓i) ↓j) ≫
      (glueData F).ι j =
    tAux F (↓i) ↓j ≫ (glueData F).ι j
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
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ (((V F (↓i) ↓j).ι ≫ (Hom.isoOpensRange (F.map (𝟙 ↓i))).hom) ≫ (F.obj ↓i).homOfLE ⋯ ≫ tAux F (↓i) ↓j) ≫
      (glueData F).ι j =
    tAux F (↓i) ↓j ≫ (glueData F).ι j

Tactic:
← Category.assoc,

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
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ ((((V F (↓i) ↓j).ι ≫ (Hom.isoOpensRange (F.map (𝟙 ↓i))).hom) ≫ (F.obj ↓i).homOfLE ⋯) ≫ tAux F (↓i) ↓j) ≫
      (glueData F).ι j =
    tAux F (↓i) ↓j ≫ (glueData F).ι j