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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
⊢ ∃ a, (toBasicOpenₗ R M f) a = s

Tactic:
obtain ⟨ι, _, a, b, ibU, iU, hab, H⟩ := exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const _
    (PrimeSpectrum.isCompact_basicOpen _) s

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus (Set.range b), f ∈ x.asIdeal

Tactic:
exact fun x hx ↦ by simpa using this hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f

Tactic:
← hU.fromSpec_preimage_basicOpen

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (U ⊓ X.basicOpen r)

Tactic:
← Scheme.basicOpen_res _ _ (homOfLE le_top).op

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r))
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
x : X
⊢ x ∈ ⇑(hom f) ⁻¹' U ↔ x ∈ ⇑(hom g) ⁻¹' U

Tactic:
rw [H]

Goal state after:
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⟩
q : ↑(PrimeSpectrum.Top S)
hqW : q ∈ ↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ }
hqV : q ∈ ↑V
hs : b ∉ (↑⟨PrimeSpectrum.comap σ q, hqW⟩).asIdeal
H : s ⟨PrimeSpectrum.comap σ q, ⋯⟩ = LocalizedModule.mk a ⟨b, hs⟩
⊢ (Localizations.comapFun f q) (s ⟨PrimeSpectrum.comap σ q, ⋯⟩) = LocalizedModule.mk (f a) ⟨σ b, hs⟩

Tactic:
rw [H]

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 ∉ (↑⟨PrimeSpectrum.comap σ q, hqW⟩).asIdeal
H : s ⟨PrimeSpectrum.comap σ q, ⋯⟩ = LocalizedModule.mk a ⟨b, hs⟩
⊢ (Localizations.comapFun f q) (LocalizedModule.mk a ⟨b, hs⟩) = LocalizedModule.mk (f a) ⟨σ b, hs⟩
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case none
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 none =
    (Iso.refl ((D.mapGlueData F).vPullbackCone i j).pt).hom ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app none

Tactic:
simp [e]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case some.left
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.left) =
    (Iso.refl ((D.mapGlueData F).vPullbackCone i j).pt).hom ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app
        (some WalkingPair.left)

Tactic:
simp [e]; rfl

Goal state after:
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) =
    (Iso.refl ((D.mapGlueData F).vPullbackCone i j).pt).hom ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app
        (some WalkingPair.right)

Tactic:
simp [e]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ ((Spec S).isoOfEq ⋯ ≪≫ basicOpenIsoSpecAway ((CommRingCat.Hom.hom f) r)).hom ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
    (Arrow.mk (Spec.map f ∣_ basicOpen r)).hom ≫ (basicOpenIsoSpecAway r).hom

Tactic:
have hcomp : CommRingCat.ofHom (algebraMap R (Localization.Away r)) ≫
        CommRingCat.ofHom (Localization.awayMap f.hom r) =
        f ≫ CommRingCat.ofHom (algebraMap S (Localization.Away (f.hom r))) := by
      ext x
      simp [Localization.awayMap, IsLocalization.Away.map]
    rw [← cancel_mono (Spec.map (CommRingCat.ofHom (algebraMap R _)))]
    simp only [Arrow.mk_hom, Category.assoc, ← Spec.map_comp]
    simp [hcomp]

Goal state after:
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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))

Tactic:
← ConcreteCategory.comp_apply,

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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left)) ≫
          (sigmaIsoSigma D.U).hom))
      ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left)) ≫
          (sigmaIsoSigma D.U).hom))
      ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))

Tactic:
← ConcreteCategory.comp_apply,

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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        (Sigma.ι D.diagram.left (i, j) ≫
          D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
              (colimit.isColimit (Discrete.functor D.diagram.left)) ≫
            (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))

Tactic:
← ConcreteCategory.comp_apply,

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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left)) ≫
          (sigmaIsoSigma D.U).hom))
      ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
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))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom (f.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s)) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom (g.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case H
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))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U) ≫
            f.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))))
        s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom (g.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left)) ≫
          (sigmaIsoSigma D.U).hom))
      ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y))

Tactic:
← ConcreteCategory.comp_apply,

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✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        (Sigma.ι D.diagram.left (i, j) ≫
          D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
              (colimit.isColimit (Discrete.functor D.diagram.left)) ≫
            (sigmaIsoSigma D.U).hom))
      y)
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst 0 0

Tactic:
by simp [← Iso.eq_inv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.snd = pullback.snd 0 0

Tactic:
by simp [← Iso.eq_inv_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
by
  refine Iff.trans ?_
    (TopCat.GlueData.ι_eq_iff_rel
      D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
      i j x y)
  rw [← ((TopCat.mono_iff_injective D.isoCarrier.inv).mp _).eq_iff, ← ConcreteCategory.comp_apply]
  · simp_rw [← D.ι_isoCarrier_inv]
    rfl -- `rfl` was not needed before https://github.com/leanprover-community/mathlib4/pull/13170
  · infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.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))
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 : ↑↑(D.V (k, i))
⊢ (ConcreteCategory.hom (D.t i k).base) ((ConcreteCategory.hom (D.t k i).base) x) = x

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case w.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))
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 : ↑↑(D.V (k, i))
⊢ (ConcreteCategory.hom ((D.t k i).base ≫ (D.t i k).base)) x = x
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:
← ConcreteCategory.comp_apply,

Goal state after:
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 ((inv (D.t' k i j)).base ≫ (D.t' k i j).base)) x = x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.refine_2
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 k i) (D.f k j))
⊢ (TopCat.Hom.hom (inv (D.t' k i j)).base) ((ConcreteCategory.hom (D.t' k i j).base) x) = x

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case w.refine_2
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 k i) (D.f k j))
⊢ (ConcreteCategory.hom ((D.t' k i j).base ≫ (inv (D.t' k i j)).base)) x = x
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) = (fromGlued 𝒰) (((gluedCover 𝒰).ι j) y)
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (ConcreteCategory.hom (((gluedCover 𝒰).ι i).base ≫ (fromGlued 𝒰).base)) x = (fromGlued 𝒰) (((gluedCover 𝒰).ι j) y)
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y