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

Goal state before:
pp: 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)
m : M
α : stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
⊢ α.addCommGroupIsoToAddEquiv ((toStalkₗ R M x) m) = (ModuleCat.Hom.hom (toStalkₗ' R M x)) m

Tactic:
change α.hom _ = _

Goal state after:
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)
m : M
α : stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
⊢ (ConcreteCategory.hom α.hom) ((toStalkₗ R M x) m) = (ModuleCat.Hom.hom (toStalkₗ' R M x)) m
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
r : ↑Γ(X, ⊤)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
rw [← basicOpen_eq_of_affine, Scheme.preimage_basicOpen, ← Scheme.Hom.appTop]
  congr
  rw [Scheme.toSpecΓ_appTop]
  exact Iso.inv_hom_id_apply (C := CommRingCat) _ _

Goal state after:
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
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥V
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) s) p =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)

Tactic:
dsimp [comapₗ, comapFun]
  suffices ⇑(Localizations.comapFun f.toSemilinearMap p.1) =
      ⇑(Localization.localRingHom (PrimeSpectrum.comap f p.1).asIdeal _ f rfl) from
    congr($this _)
  ext m
  induction m using LocalizedModule.induction_on with | h m s =>
  trans LocalizedModule.mk (f m) ⟨f ↑s, s.2⟩
  · simp
  convert_to! Localization.mk _ _ = Localization.localRingHom _ _ _ _ (Localization.mk _ _)
  simp [Localization.mk_eq_mk']

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 k : D.J
hij : ¬i = j
hik : i = k
⊢ IsIso (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
by
      subst hik; infer_instance

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x : (i : D.J) × ↑(D.U i)
⊢ (ConcreteCategory.hom (D.f x.fst x.fst))
      ((ConcreteCategory.hom (D.t x.fst x.fst)) ((ConcreteCategory.hom (inv (D.f x.fst x.fst))) x.snd)) =
    x.snd

Tactic:
by simp [IsIso.inv_hom_id_apply (D.f x.fst x.fst)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
exact (Spec _).isoOfEq (comap_basicOpen _ _) ≪≫ basicOpenIsoSpecAway (f.hom r)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a.inr
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inr x))
⊢ (coprodMk X Y) (Sum.inr x) ∈ Scheme.Hom.opensRange coprod.inl

Tactic:
simp only [coprodMk_inr, ← Scheme.Hom.comp_apply, coprod.inr_map] at hxy

Goal state after:
case a.inr
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy : coprod.inl y = (g ≫ coprod.inr) x
⊢ (coprodMk X Y) (Sum.inr x) ∈ Scheme.Hom.opensRange coprod.inl
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 : PullbackCone f g
⊢ gluedLift 𝒰 f g s ≫ p2 𝒰 f g = s.snd

Tactic:
rw [← cancel_epi (Cover.fromGlued <| 𝒰.pullback₁ s.fst)]
  apply Multicoequalizer.hom_ext
  intro b
  simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]
  simp_rw [(Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]
  simp [p2]

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₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
rw [pullback.condition, ← 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₀
⊢ (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ (gluing 𝒰 f g).openCover.f j
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.snd (D.f j i) (D.f j k)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
      (pullbackSymmetry (D.f j k) (D.f j i)).hom.c.app
          (op
            ((Opens.map (pullback.snd (D.f j i) (D.f j k)).base).obj
              ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
                ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U)))) ≫
        ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                (pullback (D.f j k) (D.f j i)).presheaf).map
            (eqToHom ⋯) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
← PresheafedSpace.comp_c_app_assoc,

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    ((pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.snd (D.f j i) (D.f j k)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
      ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
              (pullback (D.f j k) (D.f j i)).presheaf).map
          (eqToHom ⋯) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f j k) (D.f j i))
              ((Opens.map (D.t' j k i).base).1
                ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this :
  Scheme.Hom.stalkMap (coprod.inr ≫ coprodSpec R S) x =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x) ≫ Scheme.Hom.stalkMap coprod.inr x
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Tactic:
rw [← IsIso.comp_inv_eq,
      Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inr R S)] at this

Goal state after:
case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
⊢ IsIso (sigmaSpec R)

Tactic:
have : sigmaSpec R =
      (colimit.isoColimitCocone ⟨_,
        (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm _).symm (isColimitOfPreserves
          Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R)))⟩).hom := by
    ext1
    simp; rfl
  rw [this]
  infer_instance

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

Goal state before:
pp: case H
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
⊢ f x ∈ ↑(⨆ i, U i)

Tactic:
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]

Goal state after:
case H
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
⊢ ∃ i, f x ∈ U i
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✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i :
  { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
      f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀
⊢ IsOpenImmersion
    ({ I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
          f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.f
      i)

Tactic:
· dsimp
      have : pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp) =
        (pullbackSymmetry _ _).hom ≫ (pullbackLeftPullbackSndIso _ _ _).inv ≫
          pullback.fst _ _ ≫ (pullbackSymmetry _ _).hom := by aesop
      rw [this]
      infer_instance

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
i j : (glueData F).J
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
homOfLE_tAux_assoc F ↓i ↓j k.2.1 k.2.2,

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
i j : (glueData F).J
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ 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₀
e : pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i))).symm
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
⊢ P (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))

Tactic:
rw [← this, P.cancel_left_of_respectsIso]

Goal state after:
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₀
e : pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i))).symm
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
⊢ P (pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
⊢ Q.diagonal f

Tactic:
by
    refine (diagonal_iff (targetAffineLocally Q)).mpr ?_
    let 𝒰 := Y.openCoverOfIsOpenCover _
      ((isAffineOpen_top Y).iSup_basicOpen_eq_self_iff.mpr hs)
    have (i : _) : IsAffine (𝒰.X i) := (isAffineOpen_top Y).basicOpen i.1
    refine diagonal_of_openCover_diagonal (targetAffineLocally Q) f 𝒰 ?_
    intro i
    exact (Q.diagonal.arrow_mk_iso_iff
      (morphismRestrictEq _ (by simp [𝒰]) ≪≫ morphismRestrictOpensRange _ _)).mp (hs' i)

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

Goal state before:
pp: case restrict
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
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U)

Tactic:
topologically,

Goal state after:
case restrict
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
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
⊢ P ⇑(f ∣_ U)
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) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
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) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
a : ↑s
⊢ P (IsLocalization.map (Sₐ a) ((algebraMap S (Localization.Away ↑a)).comp f) ⋯)

Tactic:
apply hPl

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ X.basicOpen f = (⨆ i, ↑↑i) ⊓ X.basicOpen f

Tactic:
iSup_subtype,

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ X.basicOpen f = (⨆ i, ⨆ (h : i ∈ s), ↑↑⟨i, h⟩) ⊓ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x)

Tactic:
mul_left_comm

Goal state after:
X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ *
      ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case hU
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
specialize H i

Goal state after:
case hU
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))