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

Goal state before:
pp: case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    CommRingCat.ofHom
        (algebraMap (↑(unop (Γ.rightOp.obj Y)))
          ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
      ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).c.app (op (basicOpen r))

Tactic:
rw [LocallyRingedSpace.comp_c_app, ← Category.assoc]

Goal state after:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
r : ↑(unop (Γ.rightOp.obj Y))
⊢ (Γ.rightOp.map f).unop ≫ ((𝟭 LocallyRingedSpace).obj X).presheaf.map (homOfLE ⋯).op =
    (CommRingCat.ofHom
          (algebraMap (↑(unop (Γ.rightOp.obj Y)))
            ((structureSheafInType ↑(unop (Γ.rightOp.obj Y)) ↑(unop (Γ.rightOp.obj Y))).obj.obj (op (basicOpen r)))) ≫
        Y.toΓSpec.c.app (op (basicOpen r))) ≫
      ((𝟭 LocallyRingedSpace).map f).c.app (op ((Opens.map Y.toΓSpec.base).obj (unop (op (basicOpen r)))))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
R : CommRingCat
⊢ ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
      (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base =
    (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base

Tactic:
ext (p : PrimeSpectrum R)

Goal state after:
case w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (ConcreteCategory.hom
        (((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
          (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base))
      p =
    (ConcreteCategory.hom (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base) p
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
apply
    (IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers f)
      (asIso <| basicOpenSectionsToAffine hU f).commRingCatIsoToRingEquiv).mpr
  convert! StructureSheaf.IsLocalization.to_basicOpen _ f using 1
  apply Algebra.algebra_ext
  intro _
  congr 1
  dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
    basicOpenSectionsToAffine]
  rw [hU.fromSpec.naturality_assoc, hU.fromSpec_app_self]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))
            ⋯)).comp
      (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) =
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))

Tactic:
← CommRingCat.hom_comp,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))

Tactic:
← CommRingCat.hom_comp,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) =
    ((CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
          (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
← CommRingCat.hom_comp,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    ((CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
          (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    ((CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)).comp
          (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
← CommRingCat.hom_comp,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e'_10
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
e_5✝ : CommRing.toCommSemiring.toAddCommMonoid = inst✝⁴.toAddCommGroup.toAddCommMonoid
e_7✝ : Semiring.toModule ≍ Semiring.toModule
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
⊢ Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x) =
    ↑(commRingCatStalkEquivModuleStalk R x) ∘ₗ toStalkₗ R R x

Tactic:
have : (TopCat.Presheaf.germ (moduleStructurePresheaf R R).presheaf ⊤ x (by simp)) ≫ α.hom =
      (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map
        ((structurePresheafInCommRingCat R).germ ⊤ x (by simp)) :=
    Limits.colimit.isoColimitCocone_ι_hom ..

Goal state after:
case e'_10
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
e_5✝ : CommRing.toCommSemiring.toAddCommMonoid = inst✝⁴.toAddCommGroup.toAddCommMonoid
e_7✝ : Semiring.toModule ≍ Semiring.toModule
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
this :
  germ (moduleStructurePresheaf R R).presheaf ⊤ x ⋯ ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ ⊤ x ⋯)
⊢ Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x) =
    ↑(commRingCatStalkEquivModuleStalk R x) ∘ₗ toStalkₗ R R 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))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (LocalizedModule.mk a ⟨b, ⋯⟩) =
    LocalizedModule.mk (f a) ⟨f b, ⋯⟩

Tactic:
convert_to! Localization.localRingHom _ _ _ _ (Localization.mk _ _) = Localization.mk _ _

Goal state after:
case convert_15
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 ⋯) (Localization.mk a ⟨b, ⋯⟩) =
    Localization.mk (f a) ⟨f b, ⋯⟩
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ = ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
Set.union_eq_left

Goal state after:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ (↑U)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus ↑(I i)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ⟨(⟨↑((ConcreteCategory.hom (h.t k i))
              ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩),
          ⋯⟩,
        (ConcreteCategory.hom (h.t k i))
          ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩),
      ⋯⟩ =
    ⟨(⟨x, hx⟩, ⟨x, hx'⟩), ⋯⟩

Tactic:
Subtype.mk_eq_mk,

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ (⟨↑((ConcreteCategory.hom (h.t k i))
            ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩),
        ⋯⟩,
      (ConcreteCategory.hom (h.t k i))
        ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩) =
    (⟨x, hx⟩, ⟨x, hx'⟩)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ⟨↑((ConcreteCategory.hom (h.t k i))
            ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩),
        ⋯⟩ =
      ⟨x, hx⟩ ∧
    (ConcreteCategory.hom (h.t k i))
        ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩ =
      ⟨x, hx'⟩

Tactic:
Subtype.mk_eq_mk,

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ↑((ConcreteCategory.hom (h.t k i))
          ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩) =
      x ∧
    (ConcreteCategory.hom (h.t k i))
        ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩ =
      ⟨x, hx'⟩
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.f i j)

Tactic:
apply GlueData.f_open

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ SheafedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.f i j)

Tactic:
apply GlueData.f_open

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ PresheafedSpace.IsOpenImmersion
    (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i j)

Tactic:
apply GlueData.f_open

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 ⋯) =
    ((D.t' k i j ≫ 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)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U)

Tactic:
congr_app (D.t_fac k i j),

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.fst (D.f k i) (D.f k j) ≫ D.t k i).c.app
            (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
          (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op) ≫
      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 (⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x)))

Tactic:
rw [← Set.image_preimage_eq_inter_range]
    apply (𝒰.f (𝒰.idx x)).isOpenEmbedding.isOpenMap
    convert! hU (𝒰.idx x) using 1
    simp only [← ι_fromGlued, gluedCover_U, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.preimage_comp]
    congr! 1
    exact Set.preimage_image_eq _ 𝒰.fromGlued_injective

Goal state after:
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)
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)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← cancel_mono (pullback.snd _ _),

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)
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)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm),

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P
    (((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (Scheme.Hom.opensRange (𝒰.f i)).ι ⋯).hom ≫
        (Scheme.Hom.opensRange (𝒰.f i)).ι) ≫
      f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) := ⋯
Sₐ : ↑s → Type u := ⋯
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
this✝² : ∀ (a : ↑s), IsLocalization (Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M) (Sₐ a)
this✝¹ : ∀ (a : ↑s), IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f M)) (Sₐ a)
this✝ : (a : ↑s) → Algebra S' (Sₐ a) := ⋯
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
a : ↑s
⊢ P ((algebraMap S (Localization.Away ↑a)).comp f)

Tactic:
exact hs a.val a.property

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

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact (Set.range ⇑((X.openCoverOfIsOpenCover U hU).f i) ∩ Set.range ⇑((X.openCoverOfIsOpenCover U hU).f j))

Tactic:
simpa using hU₂ i j

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

Goal state before:
pp: case refine_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
      ⟨i, j⟩ ⟶
    pullback (f ≫ g) (Z.affineCover.f i)

pp: case refine_2
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ QuasiSeparated ?refine_1

Tactic:
· exact pullback.map _ _ _ _ (𝟙 _) _ _ (by simp) (Category.comp_id _) ≫
      (pullbackRightPullbackFstIso g (Z.affineCover.f i) f).hom

Goal state after:
case refine_2
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ QuasiSeparated
    (pullback.map f
        (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover).f
          ⟨i, j⟩)
        f ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).f ⟨i, j⟩.fst) (𝟙 X)
        (((fun i ↦
                ((fun x ↦ ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)
                    i).toPreZeroHypercover)
              ⟨i, j⟩.fst).f
          ⟨i, j⟩.snd)
        (𝟙 Y) ⋯ ⋯ ≫
      (pullbackRightPullbackFstIso g (Z.affineCover.f i) f).hom)