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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
⊢ ∀ (x_1 : ↑↑X.toPresheafedSpace) (hx : x_1 ∈ V x ⊓ V y),
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V y)).op)) (g x)) =
      (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y))

Tactic:
rintro z ⟨hzVx, hzVy⟩

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) z ⋯))
      ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V y)).op)) (g x)) =
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) z ⋯))
      ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y))
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsOpen {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}

Tactic:
rw [isOpen_iff_forall_mem_open]
    rintro x ⟨hxU, hx⟩
    obtain ⟨V, i, hxV, hf⟩ := X.isUnit_res_of_isUnit_germ U f x hxU hx
    use V.1
    refine ⟨?_, V.2, hxV⟩
    intro y hy
    use i.le hy
    convert! RingHom.isUnit_map (X.presheaf.germ _ y hy).hom hf
    exact (X.presheaf.germ_res_apply i y hy f).symm

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

Goal state before:
pp: case h
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
j : J
U : Opens ↑↑s.pt
⊢ (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)

Tactic:
· simp only [op_obj, desc, descCApp, Presheaf.comp_app, comp_c_app, colimitCocone_ι_app_c, assoc]
    rw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc]
    simp

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

Goal state before:
pp: case refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
Q : ∃ W s,
  ∃ (hW : P.pred s),
    tU = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
      tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ :=
  ?refine_1
⊢ tU = tV

pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      tU = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
        tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩

Tactic:
· choose W s hW e using Q
    exact e.1.trans e.2.symm

Goal state after:
case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      tU = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
        tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toStalk (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) ≫
      PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫ toStalk (↑S) p

Tactic:
by
  rw [← algebraMap_germ ⊤ p trivial, ← algebraMap_germ ⊤ (PrimeSpectrum.comap f.hom p) trivial,
    Category.assoc]
  erw [PresheafedSpace.stalkMap_germ (Spec.sheafedSpaceMap f).hom ⊤ p trivial]
  rw [Spec.sheafedSpaceMap_hom_c_app]
  erw [toOpen_comp_comap_assoc]
  rfl

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).inv ≫ f = Y.ofRestrict ⋯

Tactic:
by
  rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))

Tactic:
apply c_iso' f U
      ext1
      dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj, comp_base, TopCat.coe_comp]
      rw [Set.image_comp, Set.preimage_image_eq _ hg.base_open.injective]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ

Tactic:
trivial

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ IsIso f

Tactic:
by
  have : ∀ (U : (Opens Y)ᵒᵖ), IsIso (f.c.app U) := by
    intro U
    have : U = op (opensFunctor f |>.obj ((Opens.map f.base).obj (unop U))) := by
      induction U with | op U => ?_
      cases U
      dsimp only [Functor.op, Opens.map]
      congr
      exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm
    convert! H.c_iso (Opens.map f.base |>.obj <| unop U)
  have : IsIso f.c := NatIso.isIso_of_isIso_app _
  apply +allowSynthFailures isIso_of_components
  let t : X ≃ₜ Y := H.base_open.isEmbedding.toHomeomorph.trans
    { toFun := Subtype.val
      invFun := fun x =>
        ⟨x, by rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial⟩ }
  exact (TopCat.isoOfHomeo t).isIso_hom

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ (Y.presheaf.stalkCongr ⋯).hom ≫ (Arrow.mk (stalkMap f y)).hom =
    (Arrow.mk (stalkMap f x)).hom ≫ (X.presheaf.stalkCongr ⋯).hom

Tactic:
simp only [Arrow.mk_left, Arrow.mk_right, TopCat.Presheaf.stalkCongr_hom,
      Arrow.mk_hom]
    rw [stalkSpecializes_stalkMap]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ (pullbackConeOfLeft f g).pt.presheaf.map i ≫ s.snd.c.app (⋯.functor.op.obj V) ≫ s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i

Tactic:
erw [s.snd.c.naturality_assoc]
        rw [Category.assoc]
        erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]
        congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U✝ : TopCat
X : Scheme
f : U✝ ⟶ TopCat.of ↥X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : (X.restrict h).Opens
⊢ Hom.appIso (X.ofRestrict h) U = Iso.refl Γ(X, X.ofRestrict h ''ᵁ U)

Tactic:
ext1
  simp only [Hom.appIso_hom', ofRestrict_appLE, homOfLE_refl, op_id,
    CategoryTheory.Functor.map_id, Iso.refl_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
i : 𝒰.I₀
⊢ CompactSpace ↑(Set.range ⇑(𝒰.f i))

Tactic:
exact
    @Homeomorph.compactSpace _ _ _ _ (H i)
      (TopCat.homeoOfIso
        (asIso
          (IsOpenImmersion.isoOfRangeEq (𝒰.f i)
            (X.ofRestrict (Opens.isOpenEmbedding ⟨_, (𝒰.map_prop i).base_open.isOpen_range⟩))
            Subtype.range_coe.symm).hom.base))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ x ∈
    Set.range
      ⇑({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
          1)

Tactic:
rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp _)]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ x ∈ Set.univ

X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ Epi
    ({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
        1).base
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ Hom.appLE U.ι V W e = X.presheaf.map (homOfLE ⋯).op

Tactic:
by
  simp only [Hom.appLE, ι_app, toScheme_presheaf_map, Quiver.Hom.unop_op,
    Hom.opensFunctor_map_homOfLE, ← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
⊢ x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Function.Injective ⇑(toBasicOpenₗ R M f)

Tactic:
intro s t h_eq
  induction s using LocalizedModule.induction_on with | h a b =>
  induction t using LocalizedModule.induction_on with | h c d =>
  suffices f ∈ ((⊥ : Submodule R M).colon {d • a - b • c}).radical by
    rw [LocalizedModule.mk_eq]
    obtain ⟨n, hn⟩ := this
    exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl⟩
  simp only [toBasicOpenₗ_mk] at h_eq
  rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.mem_vanishingIdeal]
  intro p hfp
  contrapose hfp
  obtain ⟨u, hu⟩ := LocalizedModule.mk_eq.mp congr(($h_eq).1 ⟨p, hfp⟩)
  rw [PrimeSpectrum.mem_zeroLocus, Set.not_subset]
  exact ⟨u.1, by simpa [sub_eq_zero, smul_sub], u.2⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : IsAffine Y
⊢ IsAffine X

Tactic:
rw [← essImage_Spec] at h ⊢; exact Functor.essImage.ofIso (asIso f).symm h

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Tactic:
by
  have : IsAffine U := hU
  have : IsAffine _ := hV
  conv_rhs =>
    rw [fromSpec, ← X.homOfLE_ι (V := U) f.unop.le, isoSpec_inv, Category.assoc,
      ← Scheme.isoSpec_inv_naturality_assoc,
      ← Spec.map_comp_assoc, Scheme.homOfLE_appTop, ← Functor.map_comp]
  rw [fromSpec, isoSpec_inv, Category.assoc, ← Spec.map_comp_assoc, ← Functor.map_comp]
  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
x : ↑(PrimeSpectrum.Top R)
⊢ localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x = 𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))

Tactic:
by
    ext1
    refine IsLocalizedModule.ext x.asIdeal.primeCompl (LocalizedModule.mkLinearMap ..)
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap ..)) ?_
    ext
    dsimp [localizationtoStalkₗ]
    rw [← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply,
      elementwise_of% toStalkₗ'_stalkToFiberRingHom (M := M) x]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
← RingHom.comp_assoc,

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

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
x : X
⊢ (hom (f ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g))).toFun x =
    (hom (g ≫ ↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g))).toFun x

Tactic:
exact Function.Coequalizer.condition f g x

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:
then

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

Tactic:
then

Goal state after:
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
⊢ HasPullback (D.f' i j) (D.f' i k)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
inst✝¹ : Finite ι
inst✝ : Nonempty ι
⊢ X.zeroLocus ↑(⨅ i, I i) = ⋃ i, X.zeroLocus ↑(I i)

Tactic:
by
  simpa using zeroLocus_biInf_of_nonempty I Set.finite_univ

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ ∀ (a : (MultispanShape.prod (ofOpenSubsets U).J).L),
    (ofOpenSubsets U).diagram.fst a ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).fst a)).inclusion' =
      (ofOpenSubsets U).diagram.snd a ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).snd a)).inclusion'

Tactic:
by rintro ⟨i, j⟩; ext x; rfl

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) → x✝ ∈ ⋃ i, ↑(U i)

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(ofOpenSubsets U).glued
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x ∈ ⋃ i, ↑(U i)
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 j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
simp only [t'_fst_fst_fst, t'_fst_snd, t'_snd_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : Subsingleton ↥X
x : ↥X
⊢ x ∈ Set.univ

Tactic:
trivial

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
⊢ ∀ (a : (MultispanShape.prod (gluing 𝒰 f g).J).L),
    (gluing 𝒰 f g).diagram.fst a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) =
      (gluing 𝒰 f g).diagram.snd a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a)

Tactic:
simp [t_fst_fst_assoc, ← pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ IsOpenMap (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))

Tactic:
rw [isOpenMap_sigma]

Goal state after:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ ∀ (i : ι), IsOpenMap fun a ↦ (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨i, a⟩
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
⊢ Nonempty (IsColimit (Cofan.mk S f))

Tactic:
have : IsOpenImmersion (Sigma.desc f) := by
    refine isOpenImmersion_sigmaDesc _ _ (fun i j hij ↦ ?_)
    simpa [Function.onFun_apply, disjoint_iff, Opens.ext_iff] using hdisj hij

Goal state after:
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (Sigma.desc f)
⊢ Nonempty (IsColimit (Cofan.mk S f))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
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 : 𝒰.I₀
⊢ (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯) ≫
      pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    𝟙 (pullback (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)

Tactic:
simp_rw [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp]

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)
i : ι
⊢ P (f ∣_ Scheme.Hom.opensRange (U i).ι)

Tactic:
Scheme.Opens.opensRange_ι

Goal state after:
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)
i : ι
⊢ P (f ∣_ U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ''ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = Scheme.Hom.opensRange (⨆ i, U i).ι

Tactic:
Scheme.Opens.opensRange_ι

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ''ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = ⨆ i, U i
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hf
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)
⊢ ∀ (i : ↥X), P (f ∣_ U i)

Tactic:
· intro x
    exact P.of_postcomp (f ∣_ U x) (U x).ι (inferInstance : IsOpenImmersion _) (by simp [h₂])

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f ↔ ∀ (i : 𝒰.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
iff_of_iSup_eq_top (P := P)
    (fun i ↦ ⟨_, isAffineOpen_opensRange _⟩) 𝒰.iSup_opensRange

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ (∀ (i : 𝒰.I₀), Q (f ∣_ ↑⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩)) ↔
    ∀ (i : 𝒰.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)