mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), equalizer.lift s.fst ⋯ ≫ equalizer.ι f g = s.fst

Tactic:
exact fun s ↦ by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_2
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))),
    coequalizer.π f g ≫ coequalizer.desc s.inl ⋯ = s.inl

Tactic:
exact fun s ↦ by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal ↑Γ(X, U)
⊢ ((∀ (x : ↥X) (h : x ∈ U),
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J) ∧
      ∀ (x : ↥X) (h : x ∈ U),
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I) ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ∧
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I

Tactic:
forall_and

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
x✝ : ↑(CommRingCat.of R)
x : ↥(unop (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))
⊢ ↑((CommRingCat.Hom.hom
            (CommRingCat.ofHom (algebraMap R ↑((structureSheaf R).obj.obj (op U))) ≫
              CommRingCat.ofHom
                (comap f U ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)))
          x✝)
      x =
    ↑((CommRingCat.Hom.hom
            (CommRingCat.ofHom f ≫
              CommRingCat.ofHom
                (algebraMap S
                  ↑((structureSheaf S).obj.obj
                      (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))))
          x✝)
      x

Tactic:
by
    dsimp
    rw [comap_apply]
    exact Localization.localRingHom_to_map _ _ _ _ _

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

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
x : ↑↑(colimit (F ⋙ forgetToSheafedSpace)).toPresheafedSpace
⊢ IsLocalRing ↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk x)

Tactic:
obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x

Goal state after:
ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
⊢ IsLocalRing
    ↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
x : ↑(coproductCofan F).pt.toTopCat
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom x))

Tactic:
obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forgetToSheafedSpace) x

Goal state after:
ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝ = ⟨i, x⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨i, y⟩.fst ⟨i, x⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝) =
    ⟨i, y⟩.snd
⊢ x = y

Tactic:
· dsimp only at *
    -- Porting note: there were `cases e₁` and `cases e₂`, instead of the `rw`
    rw [← e₁, ← e₂]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
x : ↥Y
⊢ (coprodMk X Y) (Sum.inr x) = coprod.inr x

Tactic:
change ((TopCat.binaryCofan X Y).inr ≫
    (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map coprod.inr x

Goal state after:
X Y : Scheme
x : ↥Y
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inr)) x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsIso (coprodSpec R S)

Tactic:
by
  rw [isIso_iff_isIso_stalkMap]
  refine ⟨?_, isIso_stalkMap_coprodSpec R S⟩
  convert_to IsIso (TopCat.isoOfHomeo (X := Spec (.of <| R × S)) <|
    PrimeSpectrum.primeSpectrumProdHomeo.trans (coprodMk (Spec <| .of R) (Spec <| .of S))).inv
  · ext x; exact coprodSpec_apply R S x
  · infer_instance

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
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ m =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ gluedLift 𝒰 f g s

Tactic:
rw [gluedLift, (Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ m =
    (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
      pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ (gluing 𝒰 f g).ι i
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 : (Y.openCoverOfIsOpenCover Subtype.val ⋯).I₀
⊢ P (pullback.snd f ((Y.openCoverOfIsOpenCover Subtype.val ⋯).f i))

Tactic:
obtain ⟨_, i, rfl⟩ := i

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 (pullback.snd f ((Y.openCoverOfIsOpenCover Subtype.val ⋯).f ⟨U i, ⋯⟩))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : (X.openCoverOfIsOpenCover Subtype.val ⋯).I₀
⊢ P ((X.openCoverOfIsOpenCover Subtype.val ⋯).f i ≫ f)

Tactic:
obtain ⟨_, i, rfl⟩ := i

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : ι
⊢ P ((X.openCoverOfIsOpenCover Subtype.val ⋯).f ⟨U i, ⋯⟩ ≫ f)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
delta ιInvApp

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ limit.lift (D.diagramOverOpen U)
        { pt := (D.U i).presheaf.obj (op U), π := { app := fun j ↦ D.ιInvAppπApp U (unop j), naturality := ⋯ } } ≫
      D.diagramOverOpenπ U i =
    (D.U i).presheaf.map (eqToHom ⋯)
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
h : x ^ n * y ∈ J
⊢ y ∈ J

Tactic:
induction n with

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

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

Tactic:
obtain ⟨cf, hcf⟩ := this

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

Goal state before:
pp: case restrict
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (f ∘ Subtype.val)
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ {ι : Type u} (U : ι → Opens X), IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f →
      topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (U.ι ≫ f)

pp: case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (f ∘ Subtype.val)
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ {ι : Type u} (U : ι → Opens X), IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) ((U i).ι ≫ f)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f

Tactic:
· introv hf
    exact hP₁ f f.continuous _ hf

Goal state after:
case of_sSup_eq_top
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (f ∘ Subtype.val)
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ {ι : Type u} (U : ι → Opens X), IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) ((U i).ι ≫ f)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case h₂
X Y : Scheme
f : X ⟶ Y
inst✝ : SurjectiveOnStalks f
hf : Function.Injective ⇑f
⊢ ∀ (x : ↑↑((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).obj X).toPresheafedSpace),
    Epi
      (PresheafedSpace.Hom.stalkMap
        ((Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).map f).hom x)

Tactic:
exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)

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

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R : CommRingCat
⊢ ∀ (A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))

Tactic:
A

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A : CommRingCat
⊢ ∀ (B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
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.app f ⊤))

Tactic:
Scheme.Hom.app_eq_appLE

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.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case openCover
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)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen ↑r)).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Tactic:
rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]

Goal state after:
case openCover
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)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
r : ↑↑s
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen ↑r) ⋯))
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: ⊢ OfLocalizationMaximal fun R x ↦ IsReduced R

Tactic:
introv R h
  constructor
  intro x hx
  apply eq_zero_of_localization
  intro J hJ
  specialize h J hJ
  exact (hx.map <| algebraMap R <| Localization.AtPrime J).eq_zero

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⨆ (_ : ⊤ ≠ ⊤), ⊤.height ≤ ⨆ (_ : ⊥.IsMaximal), ⊥.height

Tactic:
grind [iSup_le_iff, Ideal.IsPrime.ne_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case e'_3
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) a * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ 0 =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a *
      (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b

Tactic:
exact e.symm

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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
this : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P f ↔ ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
iff_exists_appLE_locally (P := P) hQ

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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
this : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ (∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))) ↔
    ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

case hQi
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
this : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
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
hQl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQa : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
by
    have : HasRingHomProperty (affineLocally (Locally Q)) (Locally Q) :=
      ⟨locally_propertyIsLocal hQl hQa, rfl⟩
    ext X Y f
    rw [h, iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso]

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

Goal state before:
pp: case a
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := ⋯
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) ≤
    PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)

Tactic:
rw [Ideal.map_le_iff_le_comap]
        intro x hx
        suffices ∀ p, (X.affineBasicOpen f).2.fromSpec p ∈ Z → F.hom x ∈ p.asIdeal by
          simpa [PrimeSpectrum.mem_vanishingIdeal] using! this
        intro x hxZ
        refine (PrimeSpectrum.mem_vanishingIdeal _ _).mp hx
          (Spec.map (X.presheaf.map (homOfLE _).op) x) ?_
        rwa [Set.mem_preimage, ← Scheme.Hom.comp_apply,
          IsAffineOpen.map_fromSpec _ (X.affineBasicOpen f).2]

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
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P f

Tactic:
by
  have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
  wlog hY : IsAffine Y generalizing X Y f
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
    intro U
    refine this (fun x ↦ ?_) U.2
    exact (hQi.arrow_mk_iso_iff (AlgebraicGeometry.morphismRestrictStalkMap f U x)).mpr (H x.val)
  wlog hX : IsAffine X generalizing X f
  · rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
    intro U
    refine this ?_ U.2
    intro x
    rw [Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp, hQi.cancel_right_isIso]
    exact H x.val
  wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
  · rw [← P.cancel_right_of_respectsIso (g := Y.isoSpec.hom)]
    rw [← P.cancel_left_of_respectsIso (f := X.isoSpec.inv)]
    refine this inferInstance (fun x ↦ ?_) inferInstance ?_
    · rw [Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp,
        hQi.cancel_right_isIso, CommRingCat.hom_comp, hQi.cancel_left_isIso]
      apply H
    · use Γ(Y, ⊤), Γ(X, ⊤)
  obtain ⟨R, S, rfl, rfl⟩ := hXY
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  rw [Spec_iff (P := P)]
  apply hQ
  intro P hP
  specialize H ⟨P, hP⟩
  rwa [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)] at H

Goal state after: