mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯

Tactic:
choose g hxg igU f H using fun x : U ↦ exists_const U s x.1 x.2

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
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ ⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))) ≤ ⋯.functor.obj (unop (op W))

Tactic:
suffices V.ι ''ᵁ _ ≤ U.ι ''ᵁ W by simpa

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ V.ι ''ᵁ X.homOfLE h ''ᵁ W ≤ U.ι ''ᵁ W
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
X : Scheme
U V : X.Opens
h : U ≤ V
W : (↑U).Opens
⊢ ⋯.functor.obj (unop (op (X.homOfLE h ''ᵁ W))) ≤ ⋯.functor.obj (unop (op W))

Tactic:
suffices V.ι ''ᵁ _ ≤ U.ι ''ᵁ W by simpa
        simp [← Scheme.Hom.comp_image]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U : X.Opens
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = 𝟙 (Over.mk U.ι)

Tactic:
ext1

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U : X.Opens
⊢ Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯) = Over.Hom.left (𝟙 (Over.mk U.ι))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U V W : X.Opens
i : U ⟶ V
j : V ⟶ W
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = Over.homMk (X.homOfLE ⋯) ⋯ ≫ Over.homMk (X.homOfLE ⋯) ⋯

Tactic:
ext1

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U✝ U V W : X.Opens
i : U ⟶ V
j : V ⟶ W
⊢ Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯) = Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯ ≫ Over.homMk (X.homOfLE ⋯) ⋯)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.isoOfEq ⋯ = Iso.refl ↑U

Tactic:
ext1

Goal state after:
X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom = (Iso.refl ↑U).hom
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
rw [Category.assoc, pullback.condition.symm, pullbackRestrictIsoRestrict_inv_fst_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ ⊤ = Scheme.Hom.opensRange (𝟙 X)

Tactic:
ext1

Goal state after:
X : Scheme
inst✝ : IsAffine X
⊢ ↑⊤ = ↑(Scheme.Hom.opensRange (𝟙 X))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    (f ≫ coequalizer.π f g) ≫ coequalizer.desc s.inl ⋯ = s.inr

Tactic:
exact fun s ↦ by simpa using congr(coprod.inl ≫ $s.condition)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f

Tactic:
ext1

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f) = ↑(X.basicOpen f)
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:
ext1

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.Hom.hom (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x) =
    ModuleCat.Hom.hom (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)))
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)) ⋯)) ≫
      (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

Tactic:
ext1

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, ⋯⟩) := ⋯
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⟩) := ⋯
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ CommRingCat.Hom.hom
      (((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) =
    CommRingCat.Hom.hom (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)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ⨆ f, X.basicOpen ↑f = U

Tactic:
ext1

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ↑(⨆ f, X.basicOpen ↑f) = ↑U
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case inst.inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    (limit.π
        (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
          ((Opens.map
                (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                      (Hom.toShHom g)).hom.base).obj
            (unop (op U))))
        (op WalkingParallelPair.one)).hom'

Tactic:
apply CommRingCat.equalizer_ι_isLocalHom'

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ X.affineBasicOpen f = X.affineBasicOpen g

Tactic:
ext1

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ ↑(X.affineBasicOpen f) = ↑(X.affineBasicOpen g)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.inv '' PrimeSpectrum.zeroLocus s = X.zeroLocus s

Tactic:
by
  rw [← isoSpec_inv_preimage_zeroLocus, Set.image_preimage_eq]
  exact (bijective_of_isIso X.isoSpec.inv.base).surjective

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case h.left
D : GlueData
h : MkCore
i j : h.J
⊢ h.t i j ≫ h.t j i = 𝟙 ((Opens.toTopCat (h.U i)).obj (h.V i j))

Tactic:
ext1

Goal state after:
case h.left
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i j))
⊢ (ConcreteCategory.hom (h.t i j ≫ h.t j i)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U i)).obj (h.V i j)))) x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case h.right
D : GlueData
h : MkCore
i j : h.J
⊢ h.t j i ≫ h.t i j = 𝟙 ((Opens.toTopCat (h.U j)).obj (h.V j i))

Tactic:
ext1

Goal state after:
case h.right
D : GlueData
h : MkCore
i j : h.J
x✝ : ↑((Opens.toTopCat (h.U j)).obj (h.V j i))
⊢ (ConcreteCategory.hom (h.t j i ≫ h.t i j)) x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U j)).obj (h.V j i)))) x✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
R S : C
f : R ⟶ S
⊢ preservesTerminalIso (pullback f) = isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
R S : C
f : R ⟶ S
⊢ (preservesTerminalIso (pullback f)).hom = (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯).hom
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 : C
⊢ (zeroProdIso X).inv ≫ prod.snd = 𝟙 X

Tactic:
by
  dsimp [zeroProdIso, binaryFanZeroLeft]
  simp

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 ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, k)).presheaf.map (homOfLE ⋯).op ≫
        (D.V (i, k)).presheaf.map
            ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map
              (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
←
    (D.V (i, k)).presheaf.map_comp,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, k)).presheaf.map (homOfLE ⋯).op ≫
        (D.V (i, k)).presheaf.map
          ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).op.map
              (eqToHom ⋯ ≫ (Opens.map (pullback.fst (D.f i j) (D.f i k)).base).op.map (eqToHom ⋯)) ≫
            eqToHom ⋯)
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₀
⊢ pullback (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
    pullback (fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k)

Tactic:
refine pullback.map _ _ _ _ (t 𝒰 f g i j) (𝟙 _) (𝟙 _) ?_ ?_

Goal state after:
case refine_1
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) ≫ 𝟙 X =
    t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j

case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ 𝒰.f k ≫ 𝟙 X = 𝟙 (𝒰.X k) ≫ 𝒰.f k
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)
⊢ (Opens.map (D.ι j).base).obj (⋯.functor.obj U) =
    (opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))

Tactic:
ext1

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)
⊢ ↑((Opens.map (D.ι j).base).obj (⋯.functor.obj U)) =
    ↑((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: 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)

Tactic:
exact CategoryTheory.ConcreteCategory.bijective_of_isIso (C := TopCat) _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ ⟨i, x⟩ = ⟨j, y⟩ → ∃ k fi fj x_1, ((Discrete.functor g).map fi) x_1 = x ∧ ((Discrete.functor g).map fj) x_1 = y

Tactic:
· simp only [Discrete.functor_obj_eq_as, Sigma.mk.injEq]
    rintro ⟨rfl, e⟩
    obtain rfl := (heq_eq_eq x y).mp e
    exact ⟨⟨i⟩, 𝟙 _, 𝟙 _, x, by simp⟩

Goal state after:
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))
this✝ : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
this : x ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ ?m.101

Tactic:
by simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
⊢ IsCompl (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr)

Tactic:
convert! isCompl_range_inl_inr X Y

Goal state after:
X Y : Scheme
⊢ IsCompl (Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inr) ↔
    IsCompl (Set.range ⇑coprod.inl) (Set.range ⇑coprod.inr)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (Opens.map (D.f j k).base).obj (unop (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) =
    (Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj (⋯.functor.obj U)

Tactic:
ext1

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ↑((Opens.map (D.f j k).base).obj (unop (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))))) =
    ↑((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj (⋯.functor.obj U))
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

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ IsVanKampenColimit (BinaryCofan.mk coprod.inl 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✝
R S : CommRingCat
⊢ coprodComparison Scheme.Spec (op R) (op S) ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    coprodSpec ↑R ↑S

Tactic:
ext1

Goal state after:
case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ coprod.inl ≫
      coprodComparison Scheme.Spec (op R) (op S) ≫
        Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv) =
    coprod.inl ≫ coprodSpec ↑R ↑S

case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ coprod.inr ≫
      coprodComparison Scheme.Spec (op R) (op S) ≫
        Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv) =
    coprod.inr ≫ coprodSpec ↑R ↑S
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 ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
· simp [p2]

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)
this✝ : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
this : IsLocalization.Away (Function.update 0 i 1) (R i)
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ R x) i)))

Tactic:
exact IsOpenImmersion.of_isLocalization (Function.update 0 i 1)

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:
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.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
⊢ sigmaSpec R =
    (colimit.isoColimitCocone
        {
          cocone :=
            (Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm
                  (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)).symm
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }).hom

Tactic:
ext1

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
b✝ : ι
⊢ Sigma.ι (fun i ↦ Spec (R i)) b✝ ≫ sigmaSpec R =
    Sigma.ι (fun i ↦ Spec (R i)) b✝ ≫
      (colimit.isoColimitCocone
          {
            cocone :=
              (Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
            isColimit :=
              (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)).symm
                (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }).hom