mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ PresheafedSpace.IsOpenImmersion (D.ι i).hom

Tactic:
rw [← D.ι_isoPresheafedSpace_inv]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ PresheafedSpace.IsOpenImmersion (D.toPresheafedSpaceGlueData.ι i ≫ D.isoPresheafedSpace.inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g : Y ⟶ Z
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
hf : P f
inst✝ : Surjective f
⊢ Presieve.singleton f ∈ (precoverage P).coverings S

Tactic:
by
    rw [singleton_mem_precoverage_iff]
    exact ⟨f.surjective, hf⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m n : ℕ
hc : ↑⟨(fun x ↦ a ^ x) n, ⋯⟩ * (↑⟨(fun x ↦ a ^ x) m, ⋯⟩ * 1) = ↑⟨(fun x ↦ a ^ x) n, ⋯⟩ * (↑1 * y)
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
simp only [OneMemClass.coe_one, one_mul, mul_one] at hc

Goal state after:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m n : ℕ
hc : a ^ n * a ^ m = a ^ n * y
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Ideal.span (Set.range s) = ⊤
Sₜ : ι → Type u
inst✝² : (i : ι) → CommRing (Sₜ i)
inst✝¹ : (i : ι) → Algebra S (Sₜ i)
inst✝ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)
i : ι
e : Localization.Away (s i) ≃+* Sₜ i :=
  (IsLocalization.algEquiv (Submonoid.powers (s i)) (Localization.Away (s i)) (Sₜ i)).toRingEquiv
this : algebraMap S (Localization.Away (s i)) = e.symm.toRingHom.comp (algebraMap S (Sₜ i))
⊢ P ((e.symm.toRingHom.comp (algebraMap S (Sₜ i))).comp f)

Tactic:
RingHom.comp_assoc

Goal state after:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
ι : Type u_1
s : ι → S
hsone : Ideal.span (Set.range s) = ⊤
Sₜ : ι → Type u
inst✝² : (i : ι) → CommRing (Sₜ i)
inst✝¹ : (i : ι) → Algebra S (Sₜ i)
inst✝ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)
hf : ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)
i : ι
e : Localization.Away (s i) ≃+* Sₜ i :=
  (IsLocalization.algEquiv (Submonoid.powers (s i)) (Localization.Away (s i)) (Sₜ i)).toRingEquiv
this : algebraMap S (Localization.Away (s i)) = e.symm.toRingHom.comp (algebraMap S (Sₜ i))
⊢ P (e.symm.toRingHom.comp ((algebraMap S (Sₜ i)).comp f))
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
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
this : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t))
⊢ P ((e.toRingHom.comp (algebraMap S (Localization.Away t))).comp f)

Tactic:
RingHom.comp_assoc

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
this : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t))
⊢ P (e.toRingHom.comp ((algebraMap S (Localization.Away t)).comp f))
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P ((e'.toRingHom.comp (algebraMap S (Localization.Away a))).comp f)

Tactic:
RingHom.comp_assoc

Goal state after:
case refine_2
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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
e' : Localization.Away a ≃+* Localization.Away (e a) :=
  IsLocalization.ringEquivOfRingEquiv (Localization.Away a) (Localization.Away (e a)) e ⋯
this :
  (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a))
⊢ P (e'.toRingHom.comp ((algebraMap S (Localization.Away a)).comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (U.ι ≫ pullback.diagonal f)

Tactic:
apply IsZariskiLocalAtSource.comp

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (pullback.diagonal f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top.a
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
⊢ ∀ (i : ι), P (f' ∣_ i₂ ⁻¹ᵁ U i)

Tactic:
rintro i

Goal state after:
case of_sSup_eq_top.a
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ f
i : ι
⊢ P (f' ∣_ i₂ ⁻¹ᵁ U i)
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'
    intro T g _
    rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (𝒰.pullback₁ <| pullback.snd g f)]
    intro i
    dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_X, PreZeroHypercover.pullback₁_f]
    rw [← pullbackLeftPullbackSndIso_hom_fst, P.cancel_left_of_respectsIso]
    exact hf i _ _ _ (IsPullback.of_hasPullback ..)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : SurjectiveOnStalks f
hf : Function.Injective ⇑f
⊢ Mono f

Tactic:
by
  refine (Scheme.forgetToLocallyRingedSpace ⋙
    LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_
  apply SheafedSpace.mono_of_base_injective_of_stalk_epi
  · exact hf
  · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)

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

Goal state before:
pp: X : Scheme
⊢ QuasiSeparated (terminal.from X) ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)

Tactic:
quasiSeparated_iff

Goal state after:
X : Scheme
⊢ autoParam (QuasiCompact (pullback.diagonal (terminal.from X))) QuasiSeparated.quasiCompact_diagonal._autoParam ↔
    QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
⊢ I.height = 0 ↔ I = ⊥

Tactic:
by
  refine ⟨fun hI ↦ ?_, fun hI0 ↦ by simp [hI0]⟩
  rcases exists_isPrime_height_eq hI with ⟨p, _, hIp, hp0⟩
  rw [CharP.cast_eq_zero, height_eq_zero_iff, IsDomain.minimalPrimes_eq_singleton_bot,
    Set.mem_singleton_iff] at hp0
  exact bot_unique (hIp.trans_eq hp0)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
P : Ideal S := Ideal.map (algebraMap R S) p
⊢ (Ideal.map (algebraMap R S) p).height = p.height

Tactic:
have : P.IsPrime := isPrime_of_isPrime_disjoint M S p ‹_› h

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
P : Ideal S := Ideal.map (algebraMap R S) p
this : P.IsPrime
⊢ (Ideal.map (algebraMap R S) p).height = p.height
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ¬Set.univ ⊆ S
h₃ : ¬Set.univ ⊆ T
⊢ False

Tactic:
Set.not_univ_subset

Goal state after:
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ IsOpenImmersion (Spec.map f) → ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

pp: case mpr
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ (∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}) → IsOpenImmersion (Spec.map f)

Tactic:
· intro H
    obtain ⟨e, he, he'⟩ := PrimeSpectrum.isClopen_iff_zeroLocus.mp
      ⟨PrimeSpectrum.isClosed_range_comap_of_surjective _ _ hf,
        (Spec.map f).isOpenEmbedding.isOpen_range⟩
    refine ⟨e, he, ?_⟩
    let φ : R ⟶ _ := (CommRingCat.ofHom (Ideal.Quotient.mk (.span {e})))
    have : IsOpenImmersion (Spec.map φ) :=
      have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span {e}) :=
        IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
      IsOpenImmersion.of_isLocalization (1 - e)
    have H : Set.range (Spec.map φ) = Set.range (Spec.map f) :=
      ((range_comap_of_surjective _ _
        Ideal.Quotient.mk_surjective).trans (by simp)).trans he'.symm
    let i : S ≅ .of _ := (Scheme.Spec.preimageIso
      (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
    have hi : Function.Injective i.inv.hom := (ConcreteCategory.bijective_of_isIso i.inv).1
    have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]
    rw [this, CommRingCat.hom_comp, RingHom.ker_eq_comap_bot, ← Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, (RingHom.injective_iff_ker_eq_bot i.inv.hom).mp hi,
      ← RingHom.ker_eq_comap_bot]
    simp [φ]

Goal state after:
case mpr
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ (∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}) → IsOpenImmersion (Spec.map f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ I J K x✝ : X.IdealSheafData
⊢ x✝ ^ 0 = 1

Tactic:
by ext; simp [show (1 : X.IdealSheafData) = ⊤ from rfl]

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

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ I.ideal U ≤ J.ideal U

Tactic:
← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) I (le_top (a := U.1)),

Goal state after:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal ⟨⊤, ⋯⟩) ≤ J.ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case e'_2.e'_6
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
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ (CommRingCat.Hom.hom (Hom.app (I.glueDataObjι (X.affineBasicOpen f)) ⊤))
      ((CommRingCat.Hom.hom
          (X.presheaf.map
            ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ ((Hom.opensFunctor (X.basicOpen f).ι).map (eqToHom ⋯).op.unop).op)))
        x) =
    0

Tactic:
← RingHom.mem_ker,

Goal state after:
case e'_2.e'_6
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
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ (CommRingCat.Hom.hom
        (X.presheaf.map
          ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ ((Hom.opensFunctor (X.basicOpen f).ι).map (eqToHom ⋯).op.unop).op)))
      x ∈
    RingHom.ker (CommRingCat.Hom.hom (Hom.app (I.glueDataObjι (X.affineBasicOpen f)) ⊤))
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 (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op ≪≫ ΓSpecIso R).hom) ≫
      IsAffineOpen.fromSpec hU =
    f

Tactic:
simpa only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Category.assoc,
    Hom.app_eq_appLE, Hom.appLE_map_assoc, Spec.map_comp_assoc]

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso

Tactic:
by
  refine RespectsIso.mk _ ?_ ?_
  · intro X Y Z e f ⟨hZ, ⟨hY, hf⟩⟩
    simpa [hP.cancel_right_isIso, IsAffine.of_isIso e.hom]
  · intro X Y Z e f ⟨hZ, hf⟩
    simpa [AffineTargetMorphismProperty.toProperty, IsAffine.of_isIso e.inv, hP.cancel_left_isIso]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.appLE (pullback.snd f (↑U).ι ≫ (↑U).ι) ((↑U).ι ''ᵁ ⊤) ⊤ ⋯ = Hom.appLE (pullback.snd f (↑U).ι ≫ 𝟙 ↑↑U) ⊤ ⊤ ⋯

Tactic:
rw [Hom.comp_appLE, Opens.ι_app]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ Hom.appLE (pullback.snd f (↑U).ι) ((↑U).ι ⁻¹ᵁ (↑U).ι ''ᵁ ⊤) ⊤ ⋯ =
    Hom.appLE (pullback.snd f (↑U).ι ≫ 𝟙 ↑↑U) ⊤ ⊤ ⋯
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: R✝ S✝ : Type u_5
inst✝² : CommRing R✝
inst✝¹ : CommRing S✝
inst✝ : Algebra R✝ S✝
s : Set R✝
hs : Ideal.span s = ⊤
h : ∀ r ∈ s, Algebra.FiniteType (Localization.Away r) (Localization.Away r ⊗[R✝] S✝)
⊢ Algebra.FiniteType R✝ S✝

Tactic:
exact Algebra.FiniteType.of_span_eq_top_source s hs h

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case mp
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal (Algebra.ofId R A) ⋯) ⋯
this : (algebraMap A q.asIdeal.ResidueField) f = 0
⊢ False

Tactic:
← RingHom.mem_ker,

Goal state after:
case mp
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal (Algebra.ofId R A) ⋯) ⋯
this : f ∈ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
⊢ False
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsLocallyNoetherian X

Tactic:
by
  refine ⟨fun U => ?_⟩
  induction U using of_affine_open_cover S hS with
  | basicOpen U f hN =>
    have := U.prop.isLocalization_basicOpen f
    exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN
  | openCover U s _ hN =>
    apply isNoetherianRing_of_away s ‹_›
    intro ⟨f, hf⟩
    have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩
    have := U.prop.isLocalization_basicOpen f
    have hEq := IsLocalization.algEquiv (.powers f) (Localization.Away f) Γ(X, X.basicOpen f)
    exact isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv
  | hU => exact hS' _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ ↑↑V ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
· rw [IsAffineOpen.range_fromSpec]
    exact Set.inter_subset_left

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
z : ↥(pullback f q)
hz : z ∈ Z
hzt : fT z = t
⊢ False

Tactic:
suffices ∃ i, fT z ∈ Ti i ∧ p z ∈ U i from hz (by simpa)

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
z : ↥(pullback f q)
hz : z ∈ Z
hzt : fT z = t
⊢ ∃ i, fT z ∈ Ti i ∧ p z ∈ U i
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
inst✝² : CommRing R₀
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ 1 ≤ coeffSubmodule R₀ e

Tactic:
by
  rw [Submodule.one_eq_span, Submodule.span_le, Set.singleton_subset_iff]
  exact one_mem_coeffSubmodule

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply (ΓSpec.adjunction.homEquiv _ _).symm.injective
    apply Quiver.Hom.unop_inj
    rw [Adjunction.homEquiv_symm_apply, Adjunction.homEquiv_symm_apply]
    dsimp
    simp only [Scheme.toSpecΓ_appTop, Scheme.ΓSpecIso_naturality, Iso.inv_hom_id_assoc]
    apply of_mvPolynomial_int_ext
    intro i
    rw [ConcreteCategory.hom_ofHom, coe_eval₂Hom, eval₂_X]
    rfl

Goal state after: