mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ unsym a * unsym a * unsym a * unsym b - unsym a * unsym a * unsym a * unsym b = 0

Tactic:
sub_eq_zero

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ unsym a * unsym a * unsym a * unsym b = unsym a * unsym a * unsym a * unsym b
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: 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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
delta colimitPresheafObjIsoComponentwiseLimit
  rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app,
    congr_app (Iso.symm_inv _)]
  dsimp
  rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality,
      ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc,
      colimitCocone_ι_app_c, limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c

Tactic:
ext
    -- Porting note: was one liner
    -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
    rw [NatTrans.comp_app, sheafedSpaceMap_hom_c_app, Functor.whiskerRight_app, eqToHom_refl]
    erw [(sheafedSpaceObj T).presheaf.map_id]
    dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
    rw [comap_comp]
    rfl

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

Goal state before:
pp: case app.op
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 ↑↑(Y.restrict ⋯)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U

Tactic:
cases U

Goal state after:
case app.op.mk
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)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op { carrier := carrier✝, is_open' := is_open'✝ })))) =
    op { carrier := carrier✝, is_open' := is_open'✝ }
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ ↑(X.basicOpen f) ∨ x ∈ ↑(X.basicOpen g)

Tactic:
SetLike.mem_coe

Goal state after:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ X.basicOpen f ∨ x ∈ X.basicOpen g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : Opens ↑↑Y
⊢ op U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op U))))

Tactic:
cases U

Goal state after:
case op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op { carrier := carrier✝, is_open' := is_open'✝ }))))
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
simp [← Scheme.preimage_basicOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
⊢ ∃ R f, IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U

Tactic:
obtain ⟨_, ⟨_, ⟨r : R, rfl⟩, rfl⟩, hr, hr'⟩ :=
    PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open this (Opens.is_open' _)

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
⊢ ∃ R f, IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (homOfLE ⋯).op

Tactic:
dsimp [Hom.appLE]
  exact (X.presheaf.map_comp _ _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ f ⁻¹ᵁ U

Tactic:
f.preimage_image_eq

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit (forgetToSheafedSpace.mapCone (pullbackConeOfLeft f g))

Tactic:
by
    apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun
    apply isLimitOfIsLimitPullbackConeMap SheafedSpace.forgetToPresheafedSpace
    exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case mpr
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
⊢ f = X.toΓSpecCApp r →
    ConcreteCategory.hom
        (CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)))
              ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
          f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r))))

Tactic:
apply congr_arg

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
exact Scheme.basicOpen_le _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
r : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r) = r

Tactic:
rw [Scheme.toSpecΓ_appTop]

Goal state after:
X : Scheme
r : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).hom) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r) = r
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
⊢ (D.t' j k i ≫ D.t' k i j) ≫ D.t' i j k = 𝟙 (pullback (D.f j k) (D.f j i))

Tactic:
simpa using D.cocycle _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R S : CommRingCat
⊢ Function.Surjective map

Tactic:
intro f
  use Spec.preimage f
  simp

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
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (comapFun f y) (LocalizedModule.mk a 1) = σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩

Tactic:
← LocalizedModule.mkLinearMap_apply

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
y : ↑(PrimeSpectrum.Top S)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (comapFun f y) ((LocalizedModule.mkLinearMap (Ideal.comap σ y.asIdeal).primeCompl M) a) =
    σ ↑b • LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
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
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
⊢ ∀ {X Y : WalkingMultispan (MultispanShape.prod D.J)} (f : X ⟶ Y),
    (D.diagram.multispan ⋙ F).map f ≫
        (match Y with
          | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
      (match X with
          | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
        (D.mapGlueData F).diagram.multispan.map f

Tactic:
rintro (⟨_, _⟩ | _) _ (_ | _ | _) <;> simp

Goal state after:
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 : D.J
⊢ Mono (D.f' i j)

Tactic:
by dsimp [GlueData'.f']; split_ifs <;> infer_instance

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
⊢ Hom.left (𝟙 ((pullback f).obj (𝟙_ (Over X)))) = 𝟙 ((pullback f).obj (𝟙_ (Over X))).left

Tactic:
Over.id_left

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R : C
f : R ⟶ X
⊢ 𝟙 ((pullback f).obj (𝟙_ (Over X))).left = 𝟙 ((pullback f).obj (𝟙_ (Over X))).left
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰 : X.OpenCover
⊢ ∀ (a : (MultispanShape.prod (gluedCover 𝒰).J).L),
    (gluedCover 𝒰).diagram.fst a ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst a) =
      (gluedCover 𝒰).diagram.snd a ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd a)

Tactic:
rintro ⟨x, y⟩

Goal state after:
case h
X : Scheme
𝒰 : X.OpenCover
x y : (gluedCover 𝒰).J
⊢ (gluedCover 𝒰).diagram.fst (x, y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst (x, y)) =
    (gluedCover 𝒰).diagram.snd (x, y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd (x, y))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h.hU
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))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq :
  (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y =
    (ConcreteCategory.hom (D.t k i ≫ D.t i k).base) x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)

Tactic:
rw [𝖣.t_inv, id_base, TopCat.id_app] at eq

Goal state after:
case h.hU
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))
x : ↑↑(D.V (k, i))
y : ↑↑(pullback (D.f i j) (D.f i k))
eq : (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y = x
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
· apply pullback.hom_ext
      · simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]
      · simp_rw [Category.assoc, cocycle_fst_fst_snd 𝒰 f g i j k]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
x✝¹ x✝ : X.Over (⊤_ Scheme)
a b : X ⟶ ⊤_ Scheme
⊢ { hom := a } = { hom := b }

Tactic:
simp [Subsingleton.elim a b]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : Subsingleton ↥X
⊢ IsAffine X

Tactic:
cases isEmpty_or_nonempty X with
  | inl h => infer_instance
  | inr h =>
  obtain ⟨x⟩ := h
  obtain ⟨_, ⟨U, hU : IsAffine _, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (a := x) (by trivial) isOpen_univ
  obtain rfl : U = ⊤ := by ext y; simpa [Subsingleton.elim y x]
  exact .of_isIso (Scheme.topIso X).inv

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf.e_a.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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f j ≫ f) g

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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g

Tactic:
· rw [t_fst_fst, gluedLiftPullbackMap_snd]
    congr 1
    rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]

Goal state after:
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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫
      t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f j)).hom ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f j ≫ f) g
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
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : 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)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : 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:
SetLike.mem_coe

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
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : 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)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : 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.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : ↥X → Y.Opens
h₁ : ∀ (x : ↥X), f x ∈ U x
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
x : ↥X
⊢ P (f ∣_ U x ≫ (U x).ι)

Tactic:
by simp [h₂]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_1
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ (Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩))).left ≅
    (Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))).left

pp: case refine_2
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ Iso.hom ?refine_1 ≫ (Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))).hom =
    (Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩))).hom ≫
      (Iso.refl (Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩))).right).hom

Tactic:
· exact pullback.congrHom rfl (diagonalCover_map _ _ _ _) ≪≫
      pullbackDiagonalMapIso _ _ _ _ ≪≫ (asIso (pullback.diagonal _)).symm

Goal state after:
case refine_2
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
⊢ (pullback.congrHom ⋯ ⋯ ≪≫
          pullbackDiagonalMapIso f (𝒰.f ⟨i, (j, j)⟩.fst) ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1)
              ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2) ≪≫
            (asIso (pullback.diagonal ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1))).symm).hom ≫
      (Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))).hom =
    (Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩))).hom ≫
      (Iso.refl (Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩))).right).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g ≅
    pullback (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g

Tactic:
exact asIso
          (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using! pullback.condition) (by simp))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mp
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 : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
⊢ (colimit.ι F ↓i) xi = (colimit.ι F ↓j) xj → ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
← ((isColimit F).coconePointUniqueUpToIso
    (colimit.isColimit F)).inv.isOpenEmbedding.injective.eq_iff

Goal state after:
case mp
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 : Shrink.{u, w} J
xi : ↥(F.obj ↓i)
j : Shrink.{u, w} J
xj : ↥(F.obj ↓j)
⊢ ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓i) xi) =
      ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓j) xj) →
    ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj