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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
h₁ : ↑x ∈ X.basicOpen r
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
replace h₂ : X.basicOpen r ≤ V := by
    simpa [Scheme.image_basicOpen] using! (U.ι.image_mono h₂).trans (U.ι.image_preimage_le _)

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ↑x ∈ X.basicOpen r
h₂ : X.basicOpen r ≤ V
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
⊢ P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f g → P (g ≫ f)

Tactic:
rw [H _ 𝒰]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
⊢ (∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)) ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, Presieve.ofArrows 𝒰.X 𝒰.f g → P (g ≫ f)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
this : (Spec R).toSpecΓ = Spec.map (inv (Scheme.ΓSpecIso R).inv)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
IsIso.Iso.inv_inv,

Goal state after:
R : CommRingCat
this : (Spec R).toSpecΓ = Spec.map (Scheme.ΓSpecIso R).hom
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
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)
⊢ IsLocalizedModule x.asIdeal.primeCompl (Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x))

Tactic:
convert!
    IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl (toStalkₗ R R x)
      (commRingCatStalkEquivModuleStalk R x)

Goal state after:
case e'_10
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)
e_5✝ : CommRing.toCommSemiring.toAddCommMonoid = inst✝⁴.toAddCommGroup.toAddCommMonoid
e_7✝ : Semiring.toModule ≍ Semiring.toModule
⊢ Algebra.linearMap R ↑((structurePresheafInCommRingCat R).stalk x) =
    ↑(commRingCatStalkEquivModuleStalk R x) ∘ₗ toStalkₗ R R x
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

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

Tactic:
ext x

Goal state after:
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
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
⊢ ⇑(hom s.π) ∘ ⇑(hom f) = ⇑(hom s.π) ∘ ⇑(hom g)

Tactic:
ext x

Goal state after:
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
x : (fun X ↦ X) X
⊢ (⇑(hom s.π) ∘ ⇑(hom f)) x = (⇑(hom s.π) ∘ ⇑(hom g)) x
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: X Y Z : Type u
f g : X ⟶ Y
x✝¹ : Cofork f g
x✝ : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt ⟶ x✝¹.pt
hm : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).π ≫ x✝ = x✝¹.π
⊢ x✝ = ↾Function.Coequalizer.desc ⇑(hom f) ⇑(hom g) ⇑(hom x✝¹.π) ⋯

Tactic:
ext x

Goal state after:
X Y Z : Type u
f g : X ⟶ Y
x✝¹ : Cofork f g
x✝ : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt ⟶ x✝¹.pt
hm : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).π ≫ x✝ = x✝¹.π
x : (Cofork.ofπ (↾Function.Coequalizer.mk ⇑(hom f) ⇑(hom g)) ⋯).pt
⊢ (hom x✝).toFun x = (hom (↾Function.Coequalizer.desc ⇑(hom f) ⇑(hom g) ⇑(hom x✝¹.π) ⋯)).toFun x
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝² : HasMulticoequalizer D.diagram
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ (D.mapGlueData F).ι i ≫ (D.gluedIso F).inv = F.map (D.ι i)

Tactic:
by
  rw [Iso.comp_inv_eq, ι_gluedIso_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : f x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g) = 0 →
      (ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) g = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
by
  let := Y.presheaf.algebra_section_stalk ⟨f x, hx⟩
  apply (hU.isLocalization_stalk ⟨f x, hx⟩).injective_of_map_algebraMap_zero
  exact h

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
r : ↑R
⊢ CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
      CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) =
    f ≫ CommRingCat.ofHom (algebraMap (↑S) (Localization.Away ((CommRingCat.Hom.hom f) r)))

Tactic:
ext x

Goal state after:
R S : CommRingCat
f : R ⟶ S
r : ↑R
x : ↑(CommRingCat.of ↑R)
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)) ≫
          CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))
      x =
    (CommRingCat.Hom.hom (f ≫ CommRingCat.ofHom (algebraMap (↑S) (Localization.Away ((CommRingCat.Hom.hom f) r))))) x
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) =
    Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
ext x

Goal state after:
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) ↔
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' Set.univ =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) '' ⇑(ConcreteCategory.hom (D.f j i)) '' Set.univ

Tactic:
← Set.image_comp,

Goal state after:
D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' Set.univ =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ∘ ⇑(ConcreteCategory.hom (D.f j i)) '' Set.univ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑U.toSpecΓ ⁻¹' PrimeSpectrum.zeroLocus s = U.carrier ↓∩ X.zeroLocus s

Tactic:
ext x

Goal state after:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥↑U
⊢ x ∈ ⇑U.toSpecΓ ⁻¹' PrimeSpectrum.zeroLocus s ↔ x ∈ U.carrier ↓∩ X.zeroLocus s
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
ext x

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
⊢ x ∈ ⇑hU.fromSpec ⁻¹' X.zeroLocus s ↔ x ∈ PrimeSpectrum.zeroLocus s
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom x))
      ((ConcreteCategory.hom
          ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
            ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
        s))
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)

Tactic:
PresheafedSpace.stalkMap_germ_apply (coequalizer.π f.toShHom g.toShHom).hom U _ hU

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U

Tactic:
ext x

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
x : ↑(D.V (j, i))
⊢ x ∈ ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ↔
    x ∈ ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
⊢ X.zeroLocus ↑(I ⊓ J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
ext x

Goal state after:
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↥X
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f.liftQuotient I hI ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = f

Tactic:
rw [Scheme.Hom.liftQuotient, Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.lift_comp_mk]
  simp only [CommRingCat.hom_comp, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom, Spec.map_comp, ←
    Scheme.toSpecΓ_naturality_assoc, ← SpecMap_ΓSpecIso_hom]
  simp

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
ext x

Goal state after:
D : GlueData
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
i j : (ofOpenSubsets U).J
x : ↑((ofOpenSubsets U).diagram.left (i, j))
⊢ (ConcreteCategory.hom
        ((ofOpenSubsets U).diagram.fst (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j))).inclusion'))
      x =
    (ConcreteCategory.hom
        ((ofOpenSubsets U).diagram.snd (i, j) ≫ (U ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j))).inclusion'))
      x
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inl

Tactic:
dsimp [pushoutZeroZeroIso]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inl
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr

Tactic:
dsimp [pushoutZeroZeroIso]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inr
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ f = g

Tactic:
let 𝒰 : X.OpenCover := {
    I₀ := X, X i := (U i), f i := (U i).ι,
    mem₀ := by
      rw [presieve₀_mem_precoverage_iff]
      refine ⟨fun x ↦ ⟨x, by simpa using hxU x⟩, inferInstance⟩ }

Goal state after:
X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
𝒰 : X.OpenCover := { I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι, mem₀ := ⋯ }
⊢ f = g
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(TopCat.Hom.hom (D.t i j).base) '' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U =
    ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.t j i).base) ∘ ⇑(TopCat.Hom.hom (D.t i j).base) ''
      ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U =
    ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

case hf
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t j i).base)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion coprod.inl

Tactic:
rw [← ι_left_coprodIsoSigma_inv]; infer_instance

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

Tactic:
simp_rw [pullbackSymmetry_hom_comp_snd_assoc]

Goal state after:
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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.fst s.fst (𝒰.f i) ≫ s.snd =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.fst s.fst (𝒰.f j) ≫ s.snd
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (Opens.iSupOpenCover fun k ↦ Hom.opensRange (F.map k.snd.1)).I₀
⊢ pullback.fst ((F.obj i).homOfLE ⋯) ((F.obj i).homOfLE ⋯) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
    pullback.snd ((F.obj i).homOfLE ⋯) ((F.obj i).homOfLE ⋯) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2

Tactic:
apply fst_inv_eq_snd_inv F

Goal state after:
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
h₁ : αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f
h₂ : α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:
have h₁' (x : _) := congr($h₁ x).symm

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
h₁ : αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f
h₂ : αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f
h₁' :
  ∀ (x : ↥X'), ((BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f) x = (αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl) x
⊢ 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: case refine_1.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
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl

Tactic:
ext x

Goal state after:
case refine_1.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
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥(X' ⨿ Y')
⊢ x ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔ x ∈ ↑(Scheme.Hom.opensRange coprod.inl)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_2
ι : 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
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr = Scheme.Hom.opensRange coprod.inr

Tactic:
ext x

Goal state after:
case refine_1.refine_2
ι : 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
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥(X' ⨿ Y')
⊢ x ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔ x ∈ ↑(Scheme.Hom.opensRange coprod.inr)
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
⊢ (coprodSpec R S).base =
    (TopCat.isoOfHomeo
        (PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))).inv

Tactic:
ext x

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
⊢ (coprodSpec R S) x =
    (ConcreteCategory.hom
        (TopCat.isoOfHomeo
            (PrimeSpectrum.primeSpectrumProdHomeo.trans
              (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))).inv)
      x