mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case h
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⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1 * (algebraMap R (Rₜ ⟨a, ha⟩)) (a ^ 1) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1

Tactic:
mul_comm,

Goal state after:
case h
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⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ (algebraMap R (Rₜ ⟨a, ha⟩)) (a ^ 1) * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1 =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₁
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ SpecializingMap ⇑f

Tactic:
exact f.isClosedMap.specializingMap

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
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
⊢ Associated (↑b) (↑b * (algebraMap S (Localization.Away ↑a)) (↑a ^ (IsLocalization.Away.sec ↑a ↑b).2))

Tactic:
apply associated_mul_unit_right

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
⊢ IsUnit ((algebraMap S (Localization.Away ↑a)) (↑a ^ (IsLocalization.Away.sec ↑a ↑b).2))
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
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)
⊢ P ((algebraMap T (Localization.Away ((algebraMap S T) a))).comp ((algebraMap S T).comp f))

Tactic:
← comp_assoc,

Goal state after:
case refine_2
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)
⊢ P (((algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)).comp 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 := ⋯
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),
    ∃ T x x_1,
      ∃ (_ : IsLocalization.Away (↑r) T),
        Q ((algebraMap (↑Γ(X, ↑U)) T).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))

Tactic:
rintro r

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
⊢ ∃ T x x_1,
    ∃ (_ : IsLocalization.Away (↑r) T),
      Q ((algebraMap (↑Γ(X, ↑U)) T).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)))
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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝟙 ↑(𝟙 X ⁻¹ᵁ ↑U))))

Tactic:
Scheme.Hom.id_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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ Q (CommRingCat.Hom.hom (𝟙 Γ(↑(𝟙 X ⁻¹ᵁ ↑U), ⊤)))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Y → P (f ≫ g)
hY : ¬IsAffine Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i ≫ f ≫ g)

Tactic:
← Scheme.Cover.pullbackHom_map_assoc

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Y → P (f ≫ g)
hY : ¬IsAffine Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ P (Scheme.Cover.pullbackHom Y.affineCover f i ≫ Y.affineCover.f i ≫ g)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : ∀ (x : ↥X), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hx)) s = 0

Tactic:
exact (hs.map _).eq_zero

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.f j)
i : Set.range ⇑(X.affineBasisCover.f j) ⊆ ↑U
U' : Opens ↥X := { carrier := Set.range ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
h₂' : P ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.f j))
⊢ P U'

Tactic:
apply h₂'

Goal state after:
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.f j)
i : Set.range ⇑(X.affineBasisCover.f j) ⊆ ↑U
U' : Opens ↥X := ⋯
i' : U' ⟶ U := ⋯
h₂' : P ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.f j))
⊢ P ⊤
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : (ConcreteCategory.hom (𝟙 Γ(Spec R, ⊤))) s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
CommRingCat.id_apply

Goal state after:
case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
H : ¬IsPreirreducible Set.univ
⊢ False

Tactic:
isPreirreducible_iff_isClosed_union_isClosed,

Goal state after:
X : Scheme
inst✝ : IsIntegral X
H : ¬∀ (z₁ z₂ : Set ↥X), IsClosed z₁ → IsClosed z₂ → Set.univ ⊆ z₁ ∪ z₂ → Set.univ ⊆ z₁ ∨ Set.univ ⊆ z₂
⊢ False
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : Subsingleton ↥X
⊢ IsField ↑Γ(X, ⊤)

Tactic:
rw [← PrimeSpectrum.t1Space_iff_isField]
  apply X.isoSpec.hom.homeomorph.t1Space

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

Goal state before:
pp: case mp
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 φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
this : f = φ ≫ i.inv
⊢ Ideal.comap (CommRingCat.Hom.hom φ) (Ideal.comap (CommRingCat.Hom.hom i.inv) ⊥) = Ideal.span {e}

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
case mp
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 φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
this : f = φ ≫ i.inv
⊢ Ideal.comap (CommRingCat.Hom.hom φ) (RingHom.ker (CommRingCat.Hom.hom i.inv)) = Ideal.span {e}
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ideal : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)
supportSet : Set ↥X
supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet

Tactic:
exact (supportSet_inter ⟨U, hU⟩ x hxU).trans
      (I'.mem_support_iff_of_mem (U := ⟨U, hU⟩) hxU).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
U✝ V : X✝.Opens
hU✝ : IsAffineOpen U✝
hV : IsAffineOpen V
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
this : IsPreimmersion (Spec.map (X.presheaf.germ U x hx))
⊢ IsPreimmersion (Spec.map (X.presheaf.germ U x hx) ≫ hU.fromSpec)

Tactic:
apply IsPreimmersion.comp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : ↑Y.affineOpens
x✝ : ↑Γ(Y, ↑U)
⊢ x✝ ∈ (ker f).ideal U ↔ x✝ ∈ ⊥.ideal U

Tactic:
simp [map_eq_zero_iff _ (ConcreteCategory.bijective_of_isIso (f.app U)).1]

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

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : (𝒰.f i) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    0

Tactic:
← RingEquiv.coe_toRingHom,

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : (𝒰.f i) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ↑(appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
⊢ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U = f.ker.ideal U

Tactic:
by
  refine le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f U)
  intro s hs
  simp only [Hom.ker_apply, RingHom.mem_ker]
  apply X.IsSheaf.section_ext
  rintro x hxU
  obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
  simp only [homOfLE_leOfHom, map_zero, exists_and_left]
  refine ⟨𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ U.1, ⟨_, hxU, rfl⟩,
    Set.image_preimage_subset (𝒰.f i) (f ⁻¹ᵁ U), ?_⟩
  apply ((𝒰.f i).appIso _).commRingCatIsoToRingEquiv.injective
  rw [map_zero, ← RingEquiv.coe_toRingHom, Iso.commRingCatIsoToRingEquiv_toRingHom,
    Scheme.Hom.appIso_hom']
  simp only [homOfLE_leOfHom, Scheme.Hom.app_eq_appLE, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, Scheme.Hom.appLE_map, Scheme.Hom.appLE_comp_appLE]
  simpa [Scheme.Hom.appLE] using! ideal_ker_le _ _ (Ideal.mem_iInf.mp hs i)

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

Goal state before:
pp: case e'_3.e'_7
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
this✝ :
  I.subschemeCover.f U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  (((Hom.app I.subschemeι ↑U ≫ Hom.app (I.subschemeCover.f U) (I.subschemeι ⁻¹ᵁ ↑U)) ≫
          inv ((Spec (I.subschemeCover.X U)).presheaf.map (eqToHom ⋯))) ≫
        inv
          ((Spec (I.subschemeCover.X U)).presheaf.map
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map
                (eqToHom ⋯).unop).op)) ≫
      inv (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).inv =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ I.subscheme.presheaf.map
      ((homOfLE ⋯).op ≫
        ((Hom.opensFunctor (I.subschemeCover.f U)).map
              ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map (eqToHom ⋯) ≫
                eqToHom ⋯)).op ≫
          eqToHom ⋯) =
    𝟙 Γ(I.subscheme, I.subschemeι ⁻¹ᵁ ↑U)

Tactic:
exact CategoryTheory.Functor.map_id _ _

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder f)

Tactic:
have : IsPreimmersion f.liftCoborder := .of_comp f.liftCoborder f.coborderRange.ι

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ RingHom.ker
      ((CommRingCat.Hom.hom (Hom.app f ((Hom.coborderRange f).ι ''ᵁ ↑U))).comp
        (RingHom.id ↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ ↑U))) =
    RingHom.ker (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) ↑U))

Tactic:
rw [RingHomCompTriple.comp_eq, liftCoborder_app,
    CommRingCat.hom_comp, RingHom.ker_comp_of_injective]

Goal state after:
case hf
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ Function.Injective ⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op))
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case inr
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
this :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))),
    IsOpen U → (∃ f, U = ↑(basicOpen f)) → IsOpen (comap (algebraMap A (A ⊗[K] B)) '' U)
hU' : ¬∃ f, U = ↑(basicOpen f)
⊢ IsOpen (comap (algebraMap A (A ⊗[K] B)) '' U)

pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
hU' : ∃ f, U = ↑(basicOpen f)
⊢ IsOpen (comap (algebraMap A (A ⊗[K] B)) '' U)

Tactic:
· rw [eq_biUnion_of_isOpen hU, Set.image_iUnion₂]
    exact isOpen_iUnion fun _ ↦ isOpen_iUnion fun _ ↦ this _ (basicOpen _).isOpen ⟨_, rfl⟩

Goal state after:
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
hU' : ∃ f, U = ↑(basicOpen f)
⊢ IsOpen (comap (algebraMap A (A ⊗[K] B)) '' U)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
have e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A]
      (A ⧸ (Ideal.span ∅ : Ideal A)) ⊗[R] x.asIdeal.ResidueField := by
    refine Algebra.TensorProduct.congr ?f AlgEquiv.refl
    rw [Ideal.span_empty]
    exact { __ := (RingEquiv.quotientBot A).symm, __ := Algebra.ofId _ _ }

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f ((Scheme.SpecToEquivOfField K Y).symm ⟨y, φ⟩)
⊢ fst ≫ f = (snd ≫ Spec.map φ) ≫ Y.fromSpecResidueField y

Tactic:
by simp [h.w, Scheme.SpecToEquivOfField]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ NoetherianSpace ↑Set.univ

Tactic:
rw [← 𝒰.iUnion_range]

Goal state after:
X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ NoetherianSpace ↑(⋃ i, Set.range ⇑(𝒰.f i))
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsOpenImmersion ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op))

Tactic:
have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r

Goal state after:
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ IsOpenImmersion ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op))
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝ : CompactSpace ↥X
this : X.IsQuasiAffine
r : ↑Γ(Y, ⊤)
⊢ IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
    (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)

Tactic:
have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
r : ↑Γ(Y, ⊤)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
⊢ IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
    (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case e'_7
n : Type u
S T : Scheme
f : S ⟶ T
e_3✝ : 𝔸(n; S) = pullback (terminal.from S) (terminal.from (Spec ℤ[n]))
⊢ map n f ≫ toSpecMvPoly n T = toSpecMvPoly n S

Tactic:
map_toSpecMvPoly

Goal state after:
case e'_7
n : Type u
S T : Scheme
f : S ⟶ T
e_3✝ : 𝔸(n; S) = pullback (terminal.from S) (terminal.from (Spec ℤ[n]))
⊢ toSpecMvPoly n S = toSpecMvPoly n S