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

Goal state before:
pp: case app.op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑(Y.restrict ⋯)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U

Tactic:
| op U =>

Goal state after:
case app.op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑(Y.restrict ⋯)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : Opens ↑↑Y
⊢ op U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op U))))

Tactic:
| op U =>

Goal state after:
case op
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : Opens ↑↑Y
⊢ op U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op U))))
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔ (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)

Tactic:
simp_rw [← Scheme.forget_map', ← Scheme.forget_obj,
    ← Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff]

Goal state after:
P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    Presieve.ofArrows X f ∈ (Precoverage.comap forget Types.jointlySurjectivePrecoverage).coverings S ∧
      ∀ (i : ι), P (f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ (Scheme.Hom.opensRange f ⊓ U)

Tactic:
by rw [← f.image_preimage_eq_opensRange_inf, f.preimage_image_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ IsOpenImmersion f ∧ Epi f.base

Tactic:
refine ⟨inferInstance, ?_⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Epi f.base
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 j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
⊢ x ∉
    ↑((Opens.map (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base).obj
        ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)))

Tactic:
rintro ⟨y, hy, eq⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom (colimit.ι F i).hom.base) y =
    (ConcreteCategory.hom (preservesColimitIso forgetToPresheafedSpace F).inv.base)
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToPresheafedSpace) j).base) x)
⊢ False
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
⊢ LocalizedModule.mk (g i • f j) ⟨g i * g j, ⋯⟩ = LocalizedModule.mk (g j • f i) ⟨g i * g j, ⋯⟩

Tactic:
refine toBasicOpenₗ_injective (g i * g j) ?_

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
⊢ (toBasicOpenₗ R M (g i * g j)) (LocalizedModule.mk (g i • f j) ⟨g i * g j, ⋯⟩) =
    (toBasicOpenₗ R M (g i * g j)) (LocalizedModule.mk (g j • f i) ⟨g i * g j, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (g ∣_ UX) (resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯) (resLE iX US UX hUSX) (f ∣_ US)

Tactic:
· refine .of_bot ?_ ?_ (isPullback_morphismRestrict f US)
    · simpa using (isPullback_morphismRestrict g UX).paste_vert H
    · simp [← cancel_mono US.ι, H.w]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, zeroLocus {i}

Tactic:
← PrimeSpectrum.zeroLocus_iUnion₂

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus (⋃ i ∈ s, {i})
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) =
    (ConcreteCategory.hom (toStalk R x)) ((RingHom.id R) r) •
      (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m

Tactic:
← algebraMap_germ_apply U x hxU

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
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) =
    (ConcreteCategory.hom ((structurePresheafInCommRingCat R).germ U x hxU))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op U))) ((RingHom.id R) r)) •
      (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
r : R
m : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ (ConcreteCategory.hom (toStalk R x)) r • m = r • m

Tactic:
by
  change modulePresheafStalkIso R M x (toStalk R x r • (modulePresheafStalkIso R M x).symm m) = _
  rw [← (modulePresheafStalkIso R M x).eq_symm_apply, map_smul]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ CommRingCat.ofHom
        (algebraMap R
          ((structureSheafInType ↑(unop (op (CommRingCat.of R))) ↑(unop (op (CommRingCat.of R)))).obj.obj U)) ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app U =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
dsimp
  rw [← StructureSheaf.algebraMap_self_map _ U _ (homOfLE le_top).op, Category.assoc,
    NatTrans.naturality _ (homOfLE (le_top (a := U.unop))).op,
    ← unop_locallyRingedSpaceAdjunction_counit_app']
  simp_rw [← Γ_map_op]
  rw [← Γ.rightOp_map_unop, ← Category.assoc, ← unop_comp]
  erw [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply]
  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
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV).toFun 1) x✝ = ↑1 x✝

Tactic:
by
    dsimp
    simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]
    exact (Localization.localRingHom ..).map_one

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_2
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ X.presheaf.stalk x ≅ CommRingCat.of (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)

Tactic:
exact ((IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
      (X.presheaf.stalk x)
      (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toCommRingCatIso:)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ (IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal.primeCompl (↑(Y.presheaf.stalk (f x)))
              (Localization.AtPrime (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom ≫
      CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯) =
    Scheme.Hom.stalkMap f x ≫
      (IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl (↑(X.presheaf.stalk x))
              (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom

Tactic:
rw [← Iso.comp_inv_eq]

Goal state after:
case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ ((IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal.primeCompl (↑(Y.presheaf.stalk (f x)))
                (Localization.AtPrime (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom ≫
        CommRingCat.ofHom
          (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
            (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯)) ≫
      (IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl (↑(X.presheaf.stalk x))
              (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toRingEquiv.toCommRingCatIso.inv =
    Scheme.Hom.stalkMap f x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier

Tactic:
refine ⟨fun h => by rw [h], ?_⟩

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier → ⨆ f, X.basicOpen ↑f = U
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
by
  rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R : C
f : R ⟶ X
⊢ Hom.left (LaxMonoidal.ε (pullback f)) = inv (pullback.snd (𝟙 X) f)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id
  rw [← η_pullback_left, ← Over.comp_left, Monoidal.η_ε, Over.id_left]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ (fromGlued 𝒰) (((gluedCover 𝒰).ι (idx 𝒰 x)) y) = x

Tactic:
rw [← ConcreteCategory.comp_apply]

Goal state after:
case h
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ (ConcreteCategory.hom (((gluedCover 𝒰).ι (idx 𝒰 x)).base ≫ (fromGlued 𝒰).base)) y = x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
⊢ ∀ (αY : Y' ⟶ Y) (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

Tactic:
αY

Goal state after:
case refine_1
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
⊢ ∀ (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
suffices IsVanKampenColimit (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) from
      this.of_iso (hc.uniqueUpToIso (coprodIsCoprod _ _)).symm
    refine BinaryCofan.isVanKampen_mk _ _ (fun _ _ ↦ coprodIsCoprod _ _) _
      (fun _ _ ↦ pullbackIsPullback _ _) ?_ ?_
    · intro X' Y' αX αY f h₁ h₂
      have h₁' (x : _) := congr($h₁ x).symm
      have h₂' (x : _) := congr($h₂ x).symm
      dsimp at h₁ h₂ h₁' h₂'
      refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩ <;>
        ext x <;> obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x <;> simp_all
    · dsimp
      refine fun {Z} f ↦ (nonempty_isColimit_binaryCofanMk_of_isCompl _ _ ?_).some
      rw [Scheme.Hom.opensRange_pullbackFst, Scheme.Hom.opensRange_pullbackFst]
      convert! (isCompl_range_inl_inr X Y).map (CompleteLatticeHom.setPreimage f)
      simp [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]

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
⊢ IsIso (coprodSpec R S)

Tactic:
rw [isIso_iff_isIso_stalkMap]

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsIso (coprodSpec R S).base ∧
    ∀ (x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))), IsIso (Scheme.Hom.stalkMap (coprodSpec R S) x)
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✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
            (limit.isoLimitCone
                { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).f
        ((Equiv.refl (Cover.ulift 𝒰).I₀) i)

Tactic:
simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f,
          GlueData.openCover_I₀, gluing_J]

Goal state after:
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
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case mp
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f

pp: case mpr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f

Tactic:
· intro hf ⟨U, hU⟩
      exact IsZariskiLocalAtTarget.restrict hf _

Goal state after:
case mpr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ D.ιInvAppπEqMap U ≫ (D.U i).presheaf.map (eqToHom ⋯) = 𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))

Tactic:
exact Iso.inv_hom_id ((D.U i).presheaf.mapIso (eqToIso _))

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : MorphismProperty.RespectsIso @Surjective
⊢ IsZariskiLocalAtTarget @Surjective

Tactic:
rw [surjective_eq_topologically] at this ⊢

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Ideal.span s = ⊤
h : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
g : S
hg : g ∈ s
⊢ g ∈ ↑(Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)})

Tactic:
exact Ideal.subset_span (h _ hg)

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

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
this : 1 ∈ Ideal.span (Set.range fun a ↦ ↑a)
⊢ t ∈
    ↑(Ideal.span
        (Set.range fun x ↦
          match x with
          | (a, b) => g ↑a * ↑b))

Tactic:
simp only [Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe] at this ⊢

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
t : T
ht : t ∈ ↑sg
this : ∃ c, ∑ i, c i * ↑i = 1
⊢ ∃ c, ∑ i, c i * (g ↑i.1 * ↑i.2) = t
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U i)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
intro X Y f ι U hU hf x
    have hy : f x ∈ iSup U := by rw [hU]; trivial
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
    exact ((RingHom.toMorphismProperty P).arrow_mk_iso_iff <|
      morphismRestrictStalkMap f (U i) ⟨x, hi⟩).mp <| hf i ⟨x, hi⟩

Goal state after: