mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Hom.stalkMap α x'

Tactic:
rw [stalkMap.congr α α rfl x x' h]

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

Goal state before:
pp: case h
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ limit.lift
        ((pushforwardDiagramToColimit F).leftOp ⋙
          (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
        { pt := s.pt.presheaf.obj (op U),
          π :=
            { app := fun j ↦ (s.ι.app (unop j)).c.app (op U) ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
              naturality := ⋯ } } ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U))).inv ≫
        (limit.π (pushforwardDiagramToColimit F).leftOp (op j)).app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)) ≫
          (whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)

Tactic:
limitObjIsoLimitCompEvaluation_inv_π_app_assoc

Goal state after:
case h
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ limit.lift
        ((pushforwardDiagramToColimit F).leftOp ⋙
          (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
        { pt := s.pt.presheaf.obj (op U),
          π :=
            { app := fun j ↦ (s.ι.app (unop j)).c.app (op U) ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
              naturality := ⋯ } } ≫
      limit.π
          ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
          (op j) ≫
        (whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ sheafedSpaceMap (f ≫ g).unop = sheafedSpaceMap f.unop ≫ sheafedSpaceMap g.unop

Tactic:
by simp [Spec.sheafedSpaceMap_comp]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
⊢ ∀ (f_1 : U ⟶ V),
    (Y.restrict ⋯).presheaf.map f_1 ≫
        (asIso (f.c.app (op ((opensFunctor f).obj (unop V)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
      (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
        ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1

Tactic:
i

Goal state after:
case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ (Y.restrict ⋯).presheaf.map i ≫
      (asIso (f.c.app (op ((opensFunctor f).obj (unop V)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
    (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
      ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map i
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑X
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑X
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ f ⁻¹ᵁ U = g ⁻¹ᵁ U

Tactic:
subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ Γ(Y, U) = Γ(X, eqToHom e ⁻¹ᵁ U)

Tactic:
subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ app (eqToHom e) U = eqToHom ⋯

Tactic:
subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set ↑Γ(Y, U)
⊢ ⇑f ⁻¹' Y.zeroLocus s = X.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.app f U)) '' s)

Tactic:
by
  ext
  simp [← Scheme.preimage_basicOpen]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U V : (Opens ↑↑X)ᵒᵖ
⊢ ∀ (f_1 : U ⟶ V),
    X.presheaf.map f_1 ≫ invApp f (unop V) ≫ g.c.app (op (⋯.functor.obj (unop V))) ≫ Y.presheaf.map (eqToHom ⋯) =
      (invApp f (unop U) ≫ g.c.app (op (⋯.functor.obj (unop U))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map f_1

Tactic:
i

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) ≫ g.c.app (op (⋯.functor.obj (unop V))) ≫ Y.presheaf.map (eqToHom ⋯) =
    (invApp f (unop U) ≫ g.c.app (op (⋯.functor.obj (unop U))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map i
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ (pullbackConeOfLeft f g).pt.presheaf.map i ≫ s.snd.c.app (⋯.functor.op.obj V) ≫ s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i

Tactic:
s.snd.c.naturality_assoc

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        Y.presheaf.map (eqToHom ⋯) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
s.snd.c.naturality_assoc

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ (pullbackConeOfLeft f g).snd.c.app x ≫
      s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x

Tactic:
s.snd.c.naturality_assoc

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.adjunction.counit.app (unop x)).op ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app x =
    s.snd.c.app x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X.toPresheafedSpace
⊢ (Opens.map f.hom.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X.toPresheafedSpace
⊢ op U = (Opens.map f.hom.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
simp [Opens.map_def, Set.preimage_image_eq _ H.base_open.injective]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
⊢ ∀ (f : U ⟶ V),
    (X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map f ≫ (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom =
      (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom ≫ X.presheaf.map f

Tactic:
i

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ (X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map i ≫ (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom =
    (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom ≫ X.presheaf.map i
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι

Tactic:
by
  delta pullbackRestrictIsoRestrict; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Tactic:
by
  delta pullbackRestrictIsoRestrict; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ Arrow.mk (f ∣_ U) = Arrow.mk (f ∣_ V)

Tactic:
subst e; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ hU.isoSpec.hom x = (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
dsimp [IsAffineOpen.isoSpec_hom, Scheme.isoSpec_hom, Scheme.toSpecΓ_apply, Scheme.Opens.toSpecΓ,
    TopCat.Presheaf.Γgerm]
  rw [← Scheme.Hom.comp_apply, ← Spec.map_comp,
    (Iso.eq_comp_inv _).mpr (Scheme.Opens.germ_stalkIso_hom U (V := ⊤) x trivial),
    X.presheaf.germ_res_assoc, Spec.map_comp, Scheme.Hom.comp_apply]
  congr 1
  exact IsLocalRing.comap_closedPoint (U.stalkIso x).inv.hom

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.snd

Tactic:
simpa using congr($s.condition ≫ prod.fst)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ equalizer.lift s.fst ⋯ ≫ equalizer.ι f g ≫ f = s.snd

Tactic:
simpa using congr($s.condition ≫ prod.fst)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact ↑U

Tactic:
convert! @IsCompact.image _ _ _ _ Set.univ hU.fromSpec PrimeSpectrum.compactSpace.1 (by fun_prop)

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U = ⇑hU.fromSpec '' Set.univ
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
rw [← hU.fromSpec_image_basicOpen, Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x) ⊓
      X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩)

Tactic:
Scheme.basicOpen_res

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) ⁻¹' U)

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ 𝖣.diagram]

Goal state after:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' k j i ≫ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    D.t' k j i ≫ pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j

Tactic:
𝖣.cocycle_assoc,

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i = D.t' k j i ≫ pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ Arrow.mk (Spec.map f ∣_ basicOpen r) ≅
    Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))

Tactic:
refine Arrow.isoMk ?_ ?_ ?_
  · exact (Spec _).isoOfEq (comap_basicOpen _ _) ≪≫ basicOpenIsoSpecAway (f.hom r)
  · exact basicOpenIsoSpecAway r
  · 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.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ?m.92 ∈ ↑(U i)
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
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 j)) z = (ConcreteCategory.hom (D.f i j)) z
e₂ : (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) = y
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z) = (ConcreteCategory.hom (D.ι j)) y

Tactic:
← e₂

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 = (ConcreteCategory.hom (D.f i j)) z
e₂ :
  (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) =
    (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z)
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z) =
    (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z))
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 i)) w✝ = x
e₂ : (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝) = y
⊢ (ConcreteCategory.hom (D.f i i)) w✝ = y

Tactic:
← e₂

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
⊢ (ConcreteCategory.hom (D.f i i)) w✝ = (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.f j i)) ''
      ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U

Tactic:
Set.image_preimage_eq_inter_range

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ∩
      Set.range ⇑(ConcreteCategory.hom (D.f j i))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

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

Tactic:
by
  ext1; exact toUnit_unique _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
      (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso
            (PresheafedSpace.forget CommRingCat)).inv ≫
        ((PresheafedSpace.forget CommRingCat).mapIso
            (SheafedSpace.forgetToPresheafedSpace.mapIso
                (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                  D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
              D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace)).inv =
    (D.ι i).base

Tactic:
GlueData.ι_gluedIso_inv_assoc,

Goal state after:
D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      ((PresheafedSpace.forget CommRingCat).mapIso
          (SheafedSpace.forgetToPresheafedSpace.mapIso
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
            D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace)).inv =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ pullback (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
    pullback (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))

Tactic:
by
  refine (pullbackRightPullbackFstIso _ _ _).hom ≫ ?_
  refine ?_ ≫ (pullbackSymmetry _ _).hom
  refine ?_ ≫ (pullbackRightPullbackFstIso _ _ _).inv
  refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_
  · simp [pullback.condition]
  · simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
apply pullback.hom_ext <;> rw [Category.id_comp]
  · apply pullback.hom_ext
    · rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, Category.assoc, t_fst_fst]
    · simp only [Category.assoc, t_fst_snd]
  · rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, t_snd, Category.assoc]

Goal state after: