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

Goal state before:
pp: case e_a
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)) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv

Tactic:
rw [← cancel_mono (pullback.fst _ _)]

Goal state after:
case e_a
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.fst g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V

pp: case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ?refine_1).hom ≫ f ∣_ U.ι ''ᵁ V =
    f ∣_ U ∣_ V ≫ (Scheme.Hom.isoImage U.ι V).hom

Tactic:
· exact image_morphismRestrict_preimage f U V

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ (Scheme.Hom.isoImage (f ⁻¹ᵁ U).ι ((f ∣_ U) ⁻¹ᵁ V) ≪≫ X.isoOfEq ⋯).hom ≫ f ∣_ U.ι ''ᵁ V =
    f ∣_ U ∣_ V ≫ (Scheme.Hom.isoImage U.ι V).hom
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ X.homOfLE i ≫ resLE f U V e = resLE f U V' ⋯

Tactic:
← resLE_id,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ resLE (𝟙 X) V V' i ≫ resLE f U V e = resLE f U V' ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
⊢ resLE f U V e ≫ Y.homOfLE i = resLE f U' V ⋯

Tactic:
← resLE_id,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : U ≤ U'
⊢ resLE f U V e ≫ resLE (𝟙 Y) U' U i = resLE f U' V ⋯
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case e'_3
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
e_1✝ :
  (CommRingCat.of ↑(Γ.obj (op X)) ⟶
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).obj s) =
    (CommRingCat.of ↑(Γ.obj (op X)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s))))
⊢ X.toToΓSpecMapBasicOpen (unop s) =
    X.toToΓSpecMapBasicOpen (unop r) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f

Tactic:
apply X.presheaf.map_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: I : Type w
inst✝¹ : Category.{v, w} I
D : I ⥤ Scheme
inst✝ : ∀ (i : I), IsAffine (D.obj i)
⊢ PreservesLimit D Scheme.Γ.rightOp

Tactic:
let α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
  have (i : _) : IsIso (α.app i) := IsAffine.affine
  have : IsIso α := NatIso.isIso_of_isIso_app α
  suffices PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp from
    preservesLimit_of_iso_diagram _ (asIso α).symm
  have := monadicCreatesLimits.{v, w} Scheme.Spec.{u}
  suffices PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp) from
    preservesLimit_comp_of_createsLimit _ _
  exact preservesLimit_of_natIso _ (NatIso.op Scheme.SpecΓIdentity)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
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
⊢ Scheme.Hom.appTop hU.isoSpec.inv = U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv

Tactic:
← cancel_mono hU.isoSpec.hom.appTop,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop hU.isoSpec.inv ≫ Scheme.Hom.appTop hU.isoSpec.hom =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ Scheme.Hom.appTop hU.isoSpec.hom
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = Set.range ⇑(pullback.snd U.ι (𝒰.f i))

Tactic:
IsOpenImmersion.range_pullbackSnd U.ι (𝒰.f i),

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = ↑(𝒰.f i ⁻¹ᵁ Hom.opensRange U.ι)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
⊢ toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 (Γ.obj (op X))

Tactic:
unfold toSpecΓ

Goal state after:
X : LocallyRingedSpace
⊢ CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤) =
    𝟙 (Γ.obj (op X))
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✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ IsLimit (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)

Tactic:
let e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅
      cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
    NatIso.ofComponents
      (fun x => by
        cases x
        exacts [D.gluedIso F, Iso.refl _])
      (by rintro (_ | _) (_ | _) (_ | _ | _) <;> simp)

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun x ↦
      Option.casesOn (motive := fun t ↦
        x = t →
          ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
        x (fun h ↦ ⋯ ▸ D.gluedIso F)
        (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
    ⋯
⊢ IsLimit (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ Ideal.span (⇑(ConcreteCategory.hom (X.presheaf.map (homOfLE hVU).op)) '' s) = ⊤

Tactic:
rw [← Ideal.map_span, hs, Ideal.map_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: 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

Tactic:
Functor.mapIso_inv,

Goal state after:
D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (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: D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (SheafedSpace.forgetToPresheafedSpace.mapIso
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                D.toLocallyRingedSpaceGlueData.isoSheafedSpace)).inv) =
    (D.ι i).base

Tactic:
Functor.mapIso_inv,

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

Goal state before:
pp: D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (D.ι i) x = (D.ι j) y ↔
    (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j))
          y)

Tactic:
← D.ι_isoCarrier_inv

Goal state after:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j ≫
            D.isoCarrier.inv))
        y ↔
    (ConcreteCategory.hom
          (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              i ≫
            D.isoCarrier.inv))
        x =
      (ConcreteCategory.hom D.isoCarrier.inv)
        ((ConcreteCategory.hom
            (((((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData
                          LocallyRingedSpace.forgetToSheafedSpace).mapGlueData
                      SheafedSpace.forgetToPresheafedSpace).mapGlueData
                  (PresheafedSpace.forget CommRingCat)).ι
              j))
          y)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰 : X.OpenCover
x y : (gluedCover 𝒰).J
⊢ pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst (x, y)) =
    ((pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom ≫ pullback.fst (𝒰.f y) (𝒰.f x)) ≫
      𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd (x, y))

Tactic:
simpa using! pullback.condition

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ (gluedCover 𝒰).glued ⟶ X

Tactic:
by
  fapply Multicoequalizer.desc
  · exact fun x => 𝒰.f x
  rintro ⟨x, y⟩
  change pullback.fst _ _ ≫ _ = ((pullbackSymmetry _ _).hom ≫ pullback.fst _ _) ≫ _
  simpa using! pullback.condition

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:
by
  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:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
simpa using! pullback.condition

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
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (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)).base).1
            ((Opens.map (D.t j i).base).1 ((Opens.map (D.f i j).base).obj U))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ eqToHom ⋯) =
    (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:
eqToHom_trans

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)
⊢ (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)).base).1
            ((Opens.map (D.t j i).base).1 ((Opens.map (D.f i j).base).obj U))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (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.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
i j : J
l : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
x : ↥((Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).X l)
⊢ (tAux F i j) (((Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).f l) x) ∈ Set.range ⇑(V F j i).ι

Tactic:
simp only [V, tAux, ← Scheme.Hom.comp_apply, Cover.ι_glueMorphisms]

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
i j : J
l : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
x : ↥((Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).X l)
⊢ ((Hom.isoOpensRange (F.map l.snd.1)).inv ≫ F.map l.snd.2) x ∈ Set.range ⇑(⨆ k, Hom.opensRange (F.map k.snd.1)).ι
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ ⊤ ⊓ U = U

Tactic:
top_inf_eq

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ U = U
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:
simp [← Ideal.map_span, hs, Ideal.map_top]

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
s : Cocone F
j : J
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
enter [

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
s : Cocone F
j : J
| 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
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₀
⊢ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) ≫ 𝟙 S =
    𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i) ≫
      pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i

Tactic:
simpa using! pullback.condition

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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) g
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ≫ g)

Tactic:
simp only [topologically, Scheme.Hom.comp_base, TopCat.coe_comp]
    exact hP _ _ hf hg

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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
by
  apply IsZariskiLocalAtTarget.mk'
  · intro X Y f U hf
    simp_rw [topologically, morphismRestrict_base]
    exact hP₂ f U.carrier f.continuous U.2 hf
  · intro X Y f ι U hU hf
    apply hP₃ f U hU f.continuous fun i ↦ ?_
    rw [← morphismRestrict_base]
    exact hf i

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝ : IsAffine Y✝
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ CompactSpace ↥X) f✝ ↔ QuasiSeparatedSpace ↥X✝

Tactic:
exact quasiCompact_affineProperty_iff_quasiSeparatedSpace _

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

Goal state before:
pp: case e_a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
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'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ X.presheaf.map (homOfLE ⋯).op =
    X.presheaf.map (homOfLE ⋯).op ≫
      CommRingCat.ofHom
        (algebraMap
          ↑(X.presheaf.1
              (Opposite.op
                (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ↑U₂ ≫ X.presheaf.map (homOfLE e₂).op)) r'))))
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen s'))))

Tactic:
apply X.presheaf.map_comp

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

Goal state before:
pp: X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
hX : ∃ R, X = Spec R
⊢ IsClosed (⇑f '' Z)

Tactic:
obtain ⟨R, rfl⟩ := hX

Goal state after:
S R : CommRingCat
f : Spec R ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥(Spec R)
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
⊢ IsClosed (⇑f '' Z)