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
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯

Tactic:
let N := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
simp_rw [← Category.assoc]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.snd g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.snd g (Scheme.Opens.ι U)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ ⊤.toSpecΓ = ⊤.ι ≫ X.toSpecΓ

Tactic:
by
  simp [Scheme.Opens.toSpecΓ, toSpecΓ_naturality]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))

Tactic:
rw [← TopCat.coe_comp, ← TopCat.epi_iff_surjective]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Epi ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsLocalizedModule ⊥ (toOpenₗ R M ⊤)
⊢ Function.Bijective ⇑(toOpenₗ R M ⊤)

Tactic:
refine ⟨fun x y e ↦ by simpa using (IsLocalizedModule.eq_iff_exists ⊥ _).mp e, fun x ↦ ?_⟩

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsLocalizedModule ⊥ (toOpenₗ R M ⊤)
x : (structureSheafInType R M).obj.obj (op ⊤)
⊢ ∃ a, (toOpenₗ R M ⊤) a = x
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ ↑((comap f U V hUV) (const a b U hb)) p = ↑(const (f a) (f b) V ⋯) p

Tactic:
comap_apply,

Goal state after:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯)
      (↑(const a b U hb) ⟨PrimeSpectrum.comap f ↑p, ⋯⟩) =
    ↑(const (f a) (f b) V ⋯) p
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ ↑((comap (g.comp f) U W ⋯) s) p = ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

Tactic:
comap_apply,

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (g.comp f) ↑p).asIdeal (↑p).asIdeal (g.comp f) ⋯)
      (↑s ⟨PrimeSpectrum.comap (g.comp f) ↑p, ⋯⟩) =
    ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ Ideal.span s = ⊤

Tactic:
←
      PrimeSpectrum.zeroLocus_empty_iff_eq_top,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus ↑(Ideal.span s) = ∅
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
by
  ext x
  suffices (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ x.asIdeal by
    simpa [← hU.fromSpec_image_basicOpen, -not_not] using! this
  simp_rw [not_not]
  rfl

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ ((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
        ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
      ((pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').hom ≫
          ofHom
              {
                toFun := fun x ↦
                  ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
                continuous_toFun := ⋯ } ≫
            (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').inv) ≫
        (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').hom ≫
          ofHom
              {
                toFun := fun x ↦
                  ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
                continuous_toFun := ⋯ } ≫
            (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').inv =
    𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion')

Tactic:
simp_rw [← Category.assoc]

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ ((((((((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
                    ofHom
                      {
                        toFun := fun x ↦
                          ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1),
                            ⋯⟩,
                        continuous_toFun := ⋯ }) ≫
                  (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
                (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').hom) ≫
              ofHom
                {
                  toFun := fun x ↦
                    ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
                  continuous_toFun := ⋯ }) ≫
            (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').inv) ≫
          (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').hom) ≫
        ofHom
          {
            toFun := fun x ↦
              ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
            continuous_toFun := ⋯ }) ≫
      (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').inv =
    𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion')
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✝ : HasBinaryCoproduct X Y
⊢ coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl 0 0

Tactic:
simp [Iso.comp_inv_eq]

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✝ : HasBinaryCoproduct X Y
⊢ coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr 0 0

Tactic:
simp [Iso.comp_inv_eq]

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

Goal state before:
pp: case 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))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (pullback.snd (D.f i j) (D.f i k)).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.t' k i j).c.app
          ((Opens.map (pullback.snd (D.f i j) (D.f i k)).base).op.obj
            (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U))) ≫
        ((TopCat.Presheaf.pushforward C (D.t' k i j).base).obj (pullback (D.f k i) (D.f k j)).presheaf).map
            (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))

Tactic:
simp_rw [← Category.assoc]

Goal state after:
case 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))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (((pullback.snd (D.f i j) (D.f i k)).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
          (D.t' k i j).c.app
            ((Opens.map (pullback.snd (D.f i j) (D.f i k)).base).op.obj
              (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)))) ≫
        ((TopCat.Presheaf.pushforward C (D.t' k i j).base).obj (pullback (D.f k i) (D.f k j)).presheaf).map
          (eqToHom ⋯)) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case right.left
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ IsOpen (⇑(𝒰.f (idx 𝒰 x)) '' ⇑(𝒰.f (idx 𝒰 x)) ⁻¹' ⇑(fromGlued 𝒰) '' U)

Tactic:
apply (𝒰.f (𝒰.idx x)).isOpenEmbedding.isOpenMap

Goal state after:
case right.left
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ IsOpen (⇑(𝒰.f (idx 𝒰 x)) ⁻¹' ⇑(fromGlued 𝒰) '' U)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
          invApp (pullback.snd (D.f j i) (D.f j k))
              ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
simp_rw [← Category.assoc]

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ ((((D.f i j).c.app (op U) ≫ (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U))) ≫
          (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))))) ≫
        invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).1
            ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))))) ≫
      (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    ((pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
        invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U)) ≫
      (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf
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) ≫ (gluing 𝒰 f g).ι j =
    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 ⋯ ⋯ ≫ (gluing 𝒰 f g).ι j

Tactic:
simp_rw [← Category.assoc]

Goal state after:
case hf
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)) ≫
      (gluing 𝒰 f g).ι j =
    ((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 ⋯ ⋯) ≫
      (gluing 𝒰 f g).ι j
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₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i

Tactic:
simp_rw [← Category.assoc]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      (gluing 𝒰 f g).ι i =
    ((pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

Tactic:
gluing_t

Goal state after:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)
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₀
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.fst (𝒰.f i ≫ f) g = pullback.snd (p1 𝒰 f g) (𝒰.f i)

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_fst]

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₀
⊢ (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) = (gluing 𝒰 f g).ι i

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_fst]

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
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫
      (pullbackP1Iso 𝒰 f g i).hom ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
        pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i

Tactic:
simp_rw [← Category.assoc]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i =
    ((((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
            pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
          (pullbackSymmetry s.fst (𝒰.f i)).hom) ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
⊢ Ideal.span ↑(Finset.image (⇑(ConcreteCategory.hom (↑U).topIso.inv)) s) = ⊤

Tactic:
by simp [← Ideal.map_span, hs, Ideal.map_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
i : (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWX ≫ fXZ =
    (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY ≫ fYZ

Tactic:
by simpa using (H i).w

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

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
hf : P f
inst✝ : Surjective f
⊢ (cover f hf).presieve₀ = Presieve.singleton f

Tactic:
simp [cover]

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

Goal state before:
pp: 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 = ⊤
hs :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P)
      ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
choose t htone ht using hs

Goal state after:
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))
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f