mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := exists_of_pullback_V_V F x

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

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Tactic:
· have := Scheme.Hom.stalkMap_comp coprod.inr (coprodSpec R S) x
    rw [← IsIso.comp_inv_eq,
      Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inr R S)] at this
    rw [coprodMk_inr, ← this]
    let := (RingHom.snd R S).toAlgebra
    have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) :=
      IsOpenImmersion.of_isLocalization (0, 1)
    infer_instance

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

Tactic:
Category.id_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case inv_hom_id.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
i : 𝒰.I₀
⊢ pullback.fst (𝒰.f i ≫ f) g = 𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
Category.id_comp

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
this✝ : IsEmpty ↥(Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ))
this : PreservesColimit (Functor.empty CommRingCatᵒᵖ) Scheme.Spec
⊢ PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec

Tactic:
exact preservesColimitsOfShape_pempty_of_preservesInitial _

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

Tactic:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map (((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map (((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫ eqToHom ⋯)

Tactic:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map
            ((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 ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.toPreZeroHypercover.1), P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ P f

Tactic:
apply of_iSup_eq_top (fun i ↦ (𝒰.f i).opensRange) 𝒰.iSup_opensRange
  exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (H i)

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 ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
            ((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) ≫
          (D.V (j, k)).presheaf.map
            ((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:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
          ((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 ⋯)
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 ≫
      (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
        (D.V (j, k)).presheaf.map
          ((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:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (D.V (j, k)).presheaf.map (homOfLE ⋯).op ≫
      (D.V (j, k)).presheaf.map
        ((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 ⋯)
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 ≫
      (D.V (j, k)).presheaf.map
        ((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:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ 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 ⋯)
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:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ 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 ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
⊢ ∀ {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'

Tactic:
g

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ ∀ {f' : Z ⟶ Y} {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.left
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
⊢ ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
        limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) =
    𝟙 (limit (D.diagramOverOpen U)) ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) ≫
        (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))

Tactic:
Category.id_comp

Goal state after:
case op.left
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
⊢ ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
        limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) =
    limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))

Tactic:
Category.id_comp

Goal state after:
case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData
i : D.J
⊢ SheafedSpace.IsOpenImmersion (D.toSheafedSpaceGlueData.ι i ≫ D.isoSheafedSpace.inv)

Tactic:
apply +allowSynthFailures PresheafedSpace.IsOpenImmersion.comp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (D.toSheafedSpaceGlueData.ι i).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Surjective f
⊢ Set.range ⇑f = Set.univ

Tactic:
by
  simpa [Set.range_eq_univ] using f.surjective

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
this :
  IsLocalization.Away ((algebraMap S (Localization.Away ↑a)) (IsLocalization.Away.sec ↑a ↑b).1) (Localization.Away ↑b)
⊢ IsLocalization.Away (IsLocalization.Away.mulNumerator s t ⟨a, b⟩)
    ((fun x ↦
        match x with
        | ⟨a, b⟩ => Localization.Away ↑b)
      ⟨a, b⟩)

Tactic:
apply IsLocalization.Away.mul' (Localization.Away a.val) (Localization.Away b.val)

Goal state after: