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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y) = 𝟙 (𝒰.X i.2) ≫ 𝒰.f i.2

Tactic:
by simp

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y) = 𝒰.f i.1 ≫ f

Tactic:
by simp

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y) = 𝒰.f i.2 ≫ f

Tactic:
by simp

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (pullback.fst (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫
        (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y)) ≫
      (Iso.refl X).hom =
    (asIso
          (pullback.map (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.1) (𝒰.f i.2)
            (𝟙 (𝒰.X i.1)) (𝟙 (𝒰.X i.2)) (pullback.fst f (𝟙 Y)) ⋯ ⋯)).hom ≫
      pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1

Tactic:
by simp

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ pullback.diagonal f ≫ (Iso.refl (pullback.diagonalObj f)).hom = (Iso.refl X).hom ≫ pullback.diagonal f

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
U : X.Opens
⊢ (U.ι ≫ f) ≫ 𝟙 Y = U.ι ≫ f

Tactic:
by simp

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
⊢ ∀ (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)

Tactic:
t

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
t : S
⊢ ∀ [IsLocalization.Away t T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a))

Tactic:
apply IsScalarTower.of_algebraMap_eq

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) := ⋯
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ ∀ (x : S),
    (algebraMap S (Localization.Away ((algebraMap S T) a))) x =
      (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a)))
        ((algebraMap S (Localization.Away a)) x)
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
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
hU : ↑U ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ ↑U ≤ f ⁻¹ᵁ ⊤

Tactic:
by simp

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

Goal state before:
pp: case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
⊢ ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier

Tactic:
intro U hU V hV

Goal state after:
case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V : X.Opens
hV : IsCompact V.carrier
⊢ IsCompact (U ⊓ V).carrier
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : Z.affineCover.I₀
j : (pullback g (Z.affineCover.f i)).affineCover.I₀
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact ↑(⨆ i ∈ s✝, ↑i)
x : ↑X.affineOpens
s : Set ↑X.affineOpens
x✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, ↑i)
⊢ ⨆ x ∈ s, ↑x = ⨆ i ∈ s, ↑i

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = y ^ n.succ * (↑m' * ↑m' ^ n)
⊢ x = 0

Tactic:
← pow_succ',

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = y ^ n.succ * ↑m' ^ (n + 1)
⊢ x = 0
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
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.appLE f ⊤ ((↑(S i)).ι ''ᵁ ⊤) ⋯))
⊢ (↑(S i)).ι ''ᵁ ⊤ = ↑(S i)

Tactic:
by simp

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
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀
⊢ ↑(U i) = (↑(U i)).ι ''ᵁ ⊤

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
have hP : RingHom.RespectsIso (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
    RingHom.toMorphismProperty_respectsIso_iff.mpr
      (inferInstanceAs (P.inverseImage Scheme.Spec).unop.RespectsIso)
  constructor
  · intro R S _ _ f r R' S' _ _ _ _ _ _ H
    refine (RingHom.RespectsIso.isLocalization_away_iff hP ..).mp ?_
    exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) r)).mp (IsZariskiLocalAtTarget.restrict H (basicOpen r))
  · intro R S _ _ f s hs H
    apply IsZariskiLocalAtSource.of_openCover (Scheme.affineOpenCoverOfSpanRangeEqTop
      (fun i : s ↦ (i : S)) (by simpa)).openCover
    intro i
    simp only [CommRingCat.coe_of, ← Spec.map_comp,
      Scheme.AffineOpenCover.openCover_f, Scheme.affineOpenCoverOfSpanRangeEqTop_f]
    exact H i
  · intro R S _ _ f s hs H
    apply IsZariskiLocalAtTarget.of_iSup_eq_top _ (PrimeSpectrum.iSup_basicOpen_eq_top_iff
      (f := fun i : s ↦ (i : R)).mpr (by simpa))
    intro i
    exact (MorphismProperty.arrow_mk_iso_iff P (SpecMapRestrictBasicOpenIso
      (CommRingCat.ofHom f) i.1)).mpr (H i)
  · intro R S T _ _ _ _ r _ f hf
    have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization (S := T) r
    change P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap _ _)))
    rw [Spec.map_comp]
    exact IsZariskiLocalAtSource.comp hf ..

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ Cardinal.mk ↑{x} ≤ 1

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange f = ⊤

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
⊢ ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (⊥ U) = ⊥ (X.affineBasicOpen f)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
h : U.carrier.Nonempty
⊢ _root_.IsReduced ↑Γ(X, U)

Tactic:
have : Nonempty U := by simpa
    infer_instance

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 Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
⊢ Set.range ⇑i = Set.range ⇑(Scheme.Hom.opensRange i).ι

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
⊢ (⨅ i ∈ ∅, I i).ideal = ⨅ i ∈ ∅, (I i).ideal

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s✝ : Set ι
hs✝ : s✝.Finite
i : ι
s : Set ι
his : i ∉ s
hs : s.Finite
e : (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal
⊢ (⨅ i_1 ∈ insert i s, I i_1).ideal = ⨅ i_1 ∈ insert i s, (I i_1).ideal

Tactic:
simp only [iInf_insert, e, ideal_inf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: 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 * b) = (ConcreteCategory.hom (X.presheaf.germ U x hxU)) 0
⊢ False

Tactic:
rw [map_mul, map_zero] at e

Goal state after:
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
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
⊢ RingHom.ker (algebraMap (↑R) (↑R ⧸ Ideal.span {e})) = Ideal.span {1 - (1 - e)}

Tactic:
by simp

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
⊢ PrimeSpectrum.zeroLocus ↑(RingHom.ker (Ideal.Quotient.mk (Ideal.span {e}))) = PrimeSpectrum.zeroLocus {e}

Tactic:
by simp

Goal state after:
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_1 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
intro R S _ _ f

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.glueDataObjι U ≫ (↑U).ι = Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
rw [glueDataObjι, Category.assoc]; rfl

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ x ∈ ⇑f '' U ↔ x ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier

Tactic:
exact ⟨fun ⟨x, _, _⟩ ↦ by have := 𝒰.exists_eq x; simp; grind, by simp; grind⟩

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

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
inst✝ : IsAffine X
I : X.IdealSheafData
⊢ (ofIdealTop ((fun x ↦ x.ideal ⟨⊤, ⋯⟩) I)).ideal ⟨⊤, ⋯⟩ = I.ideal ⟨⊤, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
inst✝ : IsAffine X
I : Ideal ↑Γ(X, ⊤)
⊢ (fun x ↦ x.ideal ⟨⊤, ⋯⟩) (ofIdealTop I) = I

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
inst✝ : IsAffine X
⊢ ∀ (x y : X.IdealSheafData), (x * y).ideal ⟨⊤, ⋯⟩ = x.ideal ⟨⊤, ⋯⟩ * y.ideal ⟨⊤, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
inst✝ : IsAffine X
⊢ ∀ (x y : X.IdealSheafData), (x + y).ideal ⟨⊤, ⋯⟩ = x.ideal ⟨⊤, ⋯⟩ + y.ideal ⟨⊤, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Tactic:
Iso.eq_inv_comp,

Goal state after:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ (IsAffineOpen.isoSpec ⋯).hom ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    X.homOfLE h
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
⊢ ∃ V_1,
    ∃ (hV : V_1 ≤ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))),
      p ∈ V_1 ∧
        (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op))
            ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
          (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op)) 0

Tactic:
refine ⟨(I.glueDataObjι U ⁻¹ᵁ U.1.ι ⁻¹ᵁ X.basicOpen f),
    fun x hx ↦ X.basicOpen_le g (hfg ▸ hx), hf, ?_⟩

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
⊢ (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op))
      ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
    (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op)) 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ f ⁻¹ᵁ Y.basicOpen s = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ ↑U ⊓ ↑V ≤ ↑V ⊓ ↑U

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Tactic:
← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ ⋯.fromSpecStalk trivial = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ ker (inv f ≫ f ≫ g) ≤ ker g

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑⟨⊤, ⋯⟩)) ≤
    (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal ⟨⊤, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : f (closedPoint ↑R) ∈ ↑U
this : Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = (Spec R).isoSpec.inv ≫ f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑R)) = f

Tactic:
Iso.eq_inv_comp,

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : f (closedPoint ↑R) ∈ ↑U
this : (Spec R).isoSpec.hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑R)) = f