mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      𝟙 (((Functor.const WalkingCospan).obj (limit.cone (cospan f.base g.base)).pt).obj j) ≫
        ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j

Tactic:
simp_rw [Category.id_comp]

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
this : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c
⊢ (j : (Discrete ι)ᵒᵖ) →
    j ≠ op i →
      IsTerminal
        ((PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
              ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (H.functor.obj U))).obj
          j)

Tactic:
rintro ⟨j⟩ hj

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
this : IsIso (preservesColimitIso forgetToPresheafedSpace F).inv.c
j : Discrete ι
hj : op j ≠ op i
⊢ IsTerminal
    ((PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
          ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (H.functor.obj U))).obj
      (op j))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ } ≫ f = Y.ofRestrict ⋯ ≫ g

Tactic:
exact LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition _ _)

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
⊢ 1 ≫ (forget₂ TopCommRingCat TopCat).map φ = 1

Tactic:
by ext; exact φ.1.map_one

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings ↑(⨆ i, U i)

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, inferInstance⟩
    obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp x.2
    use i, ⟨x.1, hi⟩
    apply Subtype.ext
    simp

Goal state after:
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:
simp_rw [← resLE_id, resLE_comp_resLE, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    X.toToΓSpecMapBasicOpen (unop r) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f

Tactic:
convert! X.toΓSpecCApp_spec s.unop

Goal state after:
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 r) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f =
    X.toToΓSpecMapBasicOpen (unop s)
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 ⊤)
x : (structureSheafInType R M).obj.obj (op ⊤)
⊢ ∃ a, (toOpenₗ R M ⊤) a = x

Tactic:
obtain ⟨⟨x, _, rfl⟩, rfl⟩ := IsLocalizedModule.mk'_surjective ⊥ (toOpenₗ R M ⊤) x

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsLocalizedModule ⊥ (toOpenₗ R M ⊤)
x : M
⊢ ∃ a, (toOpenₗ R M ⊤) a = Function.uncurry (IsLocalizedModule.mk' (toOpenₗ R M ⊤)) (x, ⟨1, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ≫
      (structurePresheafInCommRingCat R).germ U x hxU =
    toStalk R x

Tactic:
by
  dsimp [toStalk]
  rw [← (structurePresheafInCommRingCat R).germ_res (homOfLE (le_top : U ≤ ⊤)) _ hxU]
  rfl

Goal state after:
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
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (RingHom.id R) r • (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun m

Tactic:
by
    change _ = toStalk R x _ • TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf _ _ _ _
    rw [← algebraMap_germ_apply U x hxU]
    refine .trans ?_ (PresheafOfModules.germ_smul ..)
    congr 1
    exact (IsScalarTower.algebraMap_smul Γ(R, U) r m).symm

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
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
⊢ ∀ {x y : (i : D.J) × ↑(D.U i)}, D.Rel x y → D.Rel y x

Tactic:
rintro a b ⟨x, e₁, e₂⟩

Goal state after:
D : GlueData
a b : (i : D.J) × ↑(D.U i)
x : ↑(D.V (a.fst, b.fst))
e₁ : (ConcreteCategory.hom (D.f a.fst b.fst)) x = a.snd
e₂ : (ConcreteCategory.hom (D.f b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x) = b.snd
⊢ D.Rel b a
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
x : ↑↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace
⊢ IsLocalRing ↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk x)

Tactic:
by
    obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x
    have : IsLocalRing (((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y) :=
      (F.obj i).isLocalRing _
    exact
      (asIso ((colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u})
        (F ⋙ forgetToSheafedSpace) i :).hom.stalkMap y)).symm.commRingCatIsoToRingEquiv.isLocalRing

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case e
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
x✝ : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom
          (↾⇑(ConcreteCategory.hom f.base) ≫
            ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base))).toFun
      x✝ =
    (ConcreteCategory.hom
          (↾⇑(ConcreteCategory.hom g.base) ≫
            ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base))).toFun
      x✝

Tactic:
simp only [TypeCat.Fun.toFun_apply, comp_apply, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, ← TopCat.comp_app, ← PresheafedSpace.comp_base]

Goal state after:
case e
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
x✝ : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (f.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).base) x✝ =
    (ConcreteCategory.hom (g.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).base) x✝
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ ↑D.glued.toPresheafedSpace ≅
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued

Tactic:
by
  refine (PresheafedSpace.forget _).mapIso ?_ ≪≫
    GlueData.gluedIso _ (PresheafedSpace.forget.{_, _, u} _)
  refine SheafedSpace.forgetToPresheafedSpace.mapIso ?_ ≪≫
    SheafedSpace.GlueData.isoPresheafedSpace _
  refine LocallyRingedSpace.forgetToSheafedSpace.mapIso ?_ ≪≫
    LocallyRingedSpace.GlueData.isoSheafedSpace _
  exact Scheme.GlueData.isoLocallyRingedSpace _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f z) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
delta gluedCoverT'; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)

Tactic:
delta gluedCoverT'; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
delta gluedCoverT'; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)

Tactic:
delta gluedCoverT'; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
· exact ⟨hx, 𝒰.covers x⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
F : Scheme ⥤ PresheafedSpace CommRingCat :=
  forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
⊢ IsIso (fromGlued 𝒰).toPshHom

Tactic:
apply PresheafedSpace.IsOpenImmersion.to_iso

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

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

Tactic:
have e := (D.snd_invApp_t_app' i j k U).choose_spec
  replace e := reassoc_of% e
  rw [← e]
  simp [eqToHom_map]

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 : PullbackCone f g
⊢ s.pt ⟶ (gluing 𝒰 f g).glued

Tactic:
fapply Cover.glueMorphisms (𝒰.pullback₁ s.fst)
  · exact fun i ↦ (pullbackSymmetry _ _).hom ≫
      pullback.map _ _ _ _ (𝟙 _) s.snd f (Category.id_comp _).symm s.condition ≫ (gluing 𝒰 f g).ι i
  intro i j
  rw [← gluedLiftPullbackMap_fst_assoc, ← gluing_f, ← (gluing 𝒰 f g).glue_condition i j,
    gluing_t, gluing_f]
  simp_rw [← Category.assoc]
  congr 1
  apply pullback.hom_ext <;> simp_rw [Category.assoc]
  · rw [t_fst_fst, gluedLiftPullbackMap_snd]
    congr 1
    rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]
  · rw [t_fst_snd, gluedLiftPullbackMap_fst_assoc, pullback.lift_snd, pullback.lift_snd]
    simp_rw [pullbackSymmetry_hom_comp_snd_assoc]
    exact pullback.condition_assoc _

Goal state after:
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
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ R x) i)))

Tactic:
classical
  let := (Pi.evalRingHom R i).toAlgebra
  have : IsLocalization.Away (Function.update (β := R) 0 i 1) (R i) := by
    apply IsLocalization.away_of_isIdempotentElem_of_mul
    · ext j; by_cases h : j = i <;> aesop
    · intro x y
      constructor
      · intro e; ext j; by_cases h : j = i <;> aesop
      · intro e; simpa using! congr_fun e i
    · exact Function.surjective_eval _
  exact IsOpenImmersion.of_isLocalization (Function.update 0 i 1)

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
⊢ IsOpenCover Subtype.val

Tactic:
by ext; simp [← hU]

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

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

Tactic:
refine .mk_of_iff_of_zeroHypercover fun {X Y} f 𝒰 ↦ ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
  · rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
    exact restrict _ _ hf
  · refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange <| .ulift 𝒰) fun i ↦ ?_
    dsimp
    rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f _) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f _).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
    exact hf _

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
⊢ IsOpenCover Subtype.val

Tactic:
by ext; simp [← hU]

Goal state after:
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
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
⊢ P (pullback.fst f g)

Tactic:
rw [iff_of_openCover (P := P) X.affineCover]

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
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
⊢ ∀ (i : X.affineCover.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h : ((glueData F).ι i) xi = ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
⊢ ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓i) xi) =
    ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x

Tactic:
← h,

Goal state after:
case h
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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h : ((glueData F).ι i) xi = ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
⊢ ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓i) xi) = ((glueData F).ι i) xi
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
s : ↥S
⊢ s ∈ Set.range ⇑f ↔ s ∈ Set.range ⇑g

Tactic:
range_eq_range_of_surjective f g e hge

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
s : ↥S
⊢ s ∈ Set.range ⇑g ↔ s ∈ Set.range ⇑g
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
⊢ Ideal.span (Set.range (mulNumerator s p)) = ⊤

Tactic:
rw [← Ideal.radical_eq_top, eq_top_iff, ← hsone, Ideal.span_le]
  intro a ha
  have : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩) :=
    inferInstanceAs <| IsLocalization.Away (⟨a, ha⟩ : s).val (Rₜ ⟨a, ha⟩)
  have h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span
      (algebraMap R (Rₜ ⟨a, ha⟩) '' Set.range (IsLocalization.Away.mulNumerator s p)) := by
    rw [Ideal.span_le]
    intro x hx
    rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]
    refine ⟨a * (IsLocalization.Away.sec a x).1, Ideal.subset_span ⟨⟨⟨a, ha⟩, ⟨x, hx⟩⟩, rfl⟩, ?_⟩
    use ⟨a ^ ((IsLocalization.Away.sec a x).2 + 1), _, rfl⟩
    rw [IsLocalization.eq_mk'_iff_mul_eq, map_pow, map_mul, ← map_pow, pow_add, map_mul,
      ← mul_assoc, IsLocalization.Away.sec_spec a x, mul_comm, pow_one]
  have h₂ : IsLocalization.mk' (Rₜ ⟨a, ha⟩) 1 (1 : Submonoid.powers a) ∈ Ideal.span
      (algebraMap R (Rₜ ⟨a, ha⟩) ''
        (Set.range <| IsLocalization.Away.mulNumerator s p)) := by
    rw [IsLocalization.mk'_one]
    apply h₁
    simp [htone]
  rw [IsLocalization.mem_span_map (Submonoid.powers a)] at h₂
  obtain ⟨y, hy, ⟨-, m, rfl⟩, hyz⟩ := h₂
  rw [IsLocalization.eq] at hyz
  obtain ⟨⟨-, n, rfl⟩, hc⟩ := hyz
  simp only [OneMemClass.coe_one, one_mul, mul_one] at hc
  use n + m
  simpa [pow_add, hc] using Ideal.mul_mem_left _ _ hy

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

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f ↑r ^ n' * (x * f (↑r ^ n)) = f ↑r ^ n' * f b
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
rw [mul_comm x, ← mul_assoc, ← map_pow, ← map_mul, ← map_mul, ← pow_add] at e''

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ (n' + n)) * x = f (↑r ^ n' * b)
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by
  intro R S T _ _ _ _ t _ f hf
  obtain ⟨s, hsone, hs⟩ := hf
  refine ⟨algebraMap S T '' s, ?_, ?_⟩
  · rw [← Ideal.map_span, hsone, Ideal.map_top]
  · rintro - ⟨a, ha, rfl⟩
    let : Algebra (Localization.Away a) (Localization.Away (algebraMap S T a)) :=
      (IsLocalization.Away.map _ _ (algebraMap S T) a).toAlgebra
    have : (algebraMap (Localization.Away a) (Localization.Away (algebraMap S T a))).comp
        (algebraMap S (Localization.Away a)) =
        (algebraMap T (Localization.Away (algebraMap S T a))).comp (algebraMap S T) := by
      simp [algebraMap_toAlgebra, IsLocalization.Away.map]
    rw [← comp_assoc, ← this, comp_assoc]
    have : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a)) := by
      apply IsScalarTower.of_algebraMap_eq
      intro x
      simp [algebraMap_toAlgebra, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply]
    have : IsLocalization.Away (algebraMap S (Localization.Away a) t)
        (Localization.Away (algebraMap S T a)) :=
      IsLocalization.Away.commutes _ T ((Localization.Away (algebraMap S T a))) a t
    apply hPa _ (algebraMap S (Localization.Away a) t)
    apply hs a ha

Goal state after: