mathlib-initiative/mathlib-tactics huggingface dataset:
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)
r : R
m : ↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x)
⊢ (Limits.colimit.isoColimitCocone
            {
              cocone :=
                (forget₂ (ModuleCat R) Ab).mapCocone
                  (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
              isColimit :=
                Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
                  (Limits.colimit.isColimit
                    ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }).addCommGroupIsoToAddEquiv.toFun
      (r • m) =
    (RingHom.id R) r •
      (Limits.colimit.isoColimitCocone
              {
                cocone :=
                  (forget₂ (ModuleCat R) Ab).mapCocone
                    (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
                isColimit :=
                  Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
                    (Limits.colimit.isColimit
                      ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }).addCommGroupIsoToAddEquiv.toFun
        m

Tactic:
let α : TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
      (forget₂ _ _).obj ((structurePresheafInModuleCat R M).stalk x) :=
      Limits.colimit.isoColimitCocone ⟨_, Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
      (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙
        structurePresheafInModuleCat R M))⟩
    obtain ⟨U, hxU, s, rfl⟩ := TopCat.Presheaf.exists_germ_eq _ m
    have : TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
        (forget₂ _ _).map ((structurePresheafInModuleCat R M).germ U x hxU) :=
      Limits.colimit.isoColimitCocone_ι_hom (C := Ab) ..
    have (m : _) : α.hom (TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU m) =
        (structurePresheafInModuleCat R M).germ U x hxU m := congr($this m)
    change α.hom (r • germₗ M U x hxU _) =
      r • (show (structurePresheafInModuleCat R M).stalk x from _)
    rw [← map_smul]
    refine (this _).trans ?_
    dsimp [toStalk]
    erw [this]
    exact ((structurePresheafInModuleCat R M).germ U x hxU).hom.map_smul _ _

Goal state after:
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₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
replace h₁ : x.1 ∈ X.basicOpen r := by simpa [U.mem_basicOpen_toScheme] using! h₁

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₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
h₁ : ↑x ∈ X.basicOpen r
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
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).carrier ∩ ↑U = U.carrier ∩ ↑U
⊢ ⨆ f, X.basicOpen ↑f = U

Tactic:
simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h

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.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        (Sigma.ι D.diagram.left (i, j) ≫
          D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
              (colimit.isColimit (Discrete.functor D.diagram.left)) ≫
            (sigmaIsoSigma D.U).hom))
      y)

Tactic:
colimit.ι_desc_assoc

Goal state after:
case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).snd i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.t k i).base)

pp: case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U

Tactic:
· refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
      rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R)) ⊕ ↥(Spec (CommRingCat.of S))
⊢ ((coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) x)).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm x).asIdeal

Tactic:
obtain (x | x) := x <;>
    simp only [coprodMk_inl, coprodMk_inr, ← Scheme.Hom.comp_apply,
      coprodSpec, coprod.inl_desc, coprod.inr_desc]

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal

case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal
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 : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.snd (𝒰.f i ≫ f) g = pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_snd]

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
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i) = pullback.fst (𝒰.f i ≫ f) g

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_snd]

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P f ↔ P f'

Tactic:
rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]

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

Goal state before:
pp: case hU
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
i : ι
⊢ Q (f ∣_ ↑(U i))

Tactic:
exact hU' i

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

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

pp: case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              ((Opens.map
                    (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                (⋯.functor.obj U)))))))

Tactic:
· erw [D.ι_image_preimage_eq i j U]
      infer_instance

Goal state after:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              ((Opens.map
                    (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                (⋯.functor.obj U)))))))
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 : D.J
U : Opens ↑↑(D.U i)
j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) j =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) j

Tactic:
induction j with

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : WalkingMultispan (MultispanShape.prod D.J)
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) (op j) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op j)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

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

Tactic:
have : MorphismProperty.RespectsIso @Surjective := inferInstance
  rw [surjective_eq_topologically] at this ⊢
  refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) ?_
  intro α β _ _ f ι U H _ hf x
  obtain ⟨i, hxi⟩ : ∃ i, x ∈ U i := by simpa using congr(x ∈ $H)
  obtain ⟨⟨y, _⟩, hy⟩ := hf i ⟨x, hxi⟩
  exact ⟨y, congr(($hy).1)⟩

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
⊢ P.universally (𝒰.f i ≫ f)

Tactic:
apply MorphismProperty.universally_mk'

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
⊢ ∀ {T : Scheme} (f_1 : T ⟶ Y) [inst : HasPullback f_1 (𝒰.f i ≫ f)], P (pullback.fst f_1 (𝒰.f i ≫ f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
⊢ P.universally f

Tactic:
apply MorphismProperty.universally_mk'

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
⊢ ∀ {T : Scheme} (f_1 : T ⟶ Y) [inst : HasPullback f_1 f], P (pullback.fst f_1 f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: 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
⊢ IsZariskiLocalAtSource (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P)

Tactic:
by
  let := stalkwise_respectsIso hP
  apply IsZariskiLocalAtSource.mk'
  · intro X Y f U hf x
    rw [Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp, hP.cancel_right_isIso]
    exact hf _
  · intro X Y f ι U hU hf x
    have hy : x ∈ iSup U := by rw [hU]; trivial
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
    rw [← hP.cancel_right_isIso _ ((U i).ι.stalkMap ⟨x, hi⟩)]
    simpa [Scheme.Hom.stalkMap_comp] using hf i ⟨x, hi⟩

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

Goal state before:
pp: X : Scheme
⊢ QuasiSeparatedSpace ↥X ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
quasiSeparatedSpace_iff

Goal state after:
X : Scheme
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ P).IsLocal

Tactic:
by
  constructor
  · exact sourceAffineLocally_respectsIso P h₁
  · intro X Y _ f r H
    rw [sourceAffineLocally_morphismRestrict]
    intro U hU
    have : X.basicOpen (f.appLE ⊤ U (by simp) r) = U := by
      simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]
      rw [Scheme.basicOpen_res]
      simpa using hU
    rw [← f.appLE_congr (by simp [Scheme.Hom.appLE]) rfl this (fun f => P f.hom),
      IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2 _ r]
    simp only [CommRingCat.hom_ofHom]
    apply +allowSynthFailures h₂
    exact H U
  · introv hs hs' U
    apply h₃ _ _ hs
    intro r
    simp_rw [sourceAffineLocally_morphismRestrict] at hs'
    have := hs' r ⟨X.basicOpen (f.appLE ⊤ U le_top r.1), U.2.basicOpen (f.appLE ⊤ U le_top r.1)⟩
      (by simp [Scheme.Hom.appLE])
    rwa [IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2, CommRingCat.hom_ofHom,
      ← h₁.isLocalization_away_iff] at this

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
i : ↑s
⊢ ↑↑i ≤ ⨆ i, ↑↑i

Tactic:
exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
Scheme.Hom.appTop,

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case hU
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f ≫ X.presheaf.map (homOfLE ⋯).op))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))

Tactic:
Scheme.Hom.appTop,

Goal state after:
case hU
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤ ≫ X.presheaf.map (homOfLE ⋯).op))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(S i) ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource P

Tactic:
apply HasAffineProperty.isZariskiLocalAtSource

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], KrullDimLE n (Rₚ P)
⊢ KrullDimLE n R

Tactic:
simp_rw [Ring.krullDimLE_iff] at h ⊢
  nontriviality R
  rw [← Ideal.sup_isMaximal_height_eq_ringKrullDim]
  refine (WithBot.coe_le_coe).mpr (iSup₂_le_iff.mpr fun P hP ↦ ?_)
  rw [← WithBot.coe_le_coe, ← IsLocalization.AtPrime.ringKrullDim_eq_height P (Rₚ P)]
  exact h P

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
hX : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ (Y.basicOpen a).ι)))

Tactic:
exact hQ _ a _ hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
⊢ IrreducibleSpace ↥X

Tactic:
by_contra H

Goal state after:
X : Scheme
inst✝ : IsIntegral X
H : ¬IrreducibleSpace ↥X
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) n, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) n, ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'

Tactic:
cases n

Goal state after:
case zero
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) 0, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) 0, ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'

case succ
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n✝ : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) (n✝ + 1), ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) (n✝ + 1), ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f✝ : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
exact (locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
n : ℕ
hn : n ≠ 0
⊢ (I ^ n).support = I.support

Tactic:
cases n

Goal state after:
case zero
X : Scheme
I : X.IdealSheafData
hn : 0 ≠ 0
⊢ (I ^ 0).support = I.support

case succ
X : Scheme
I : X.IdealSheafData
n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (I ^ (n✝ + 1)).support = I.support