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⟩
⊢ x * (algebraMap R (Rₜ ⟨a, ha⟩)) (a ^ ((sec a x).2 + 1)) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1

Tactic:
pow_add,

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⟩
⊢ x * (algebraMap R (Rₜ ⟨a, ha⟩)) (a ^ (sec a x).2 * a ^ 1) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1
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⟩)
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
have h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span
      (algebraMap R (Rₜ ⟨a, ha⟩) '' Set.range (IsLocalization.Away.mulNumerator s p)) := by
    rw [Ideal.span_le]
    intro x hx
    rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]
    refine ⟨a * (IsLocalization.Away.sec a x).1, Ideal.subset_span ⟨⟨⟨a, ha⟩, ⟨x, hx⟩⟩, rfl⟩, ?_⟩
    use ⟨a ^ ((IsLocalization.Away.sec a x).2 + 1), _, rfl⟩
    rw [IsLocalization.eq_mk'_iff_mul_eq, map_pow, map_mul, ← map_pow, pow_add, map_mul,
      ← mul_assoc, IsLocalization.Away.sec_spec a x, mul_comm, pow_one]

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))
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case succ
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 : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x ^ (1 + n) * y ∈ J
⊢ y ∈ J

Tactic:
pow_add,

Goal state after:
case succ
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 : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x ^ 1 * x ^ n * y ∈ J
⊢ y ∈ J
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
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))
⊢ ∀ (i : (a : ↑s) × ↑(t a)),
    P
      ((algebraMap S
            ((fun x ↦
                match x with
                | ⟨a, b⟩ => Localization.Away ↑b)
              i)).comp
        f)

Tactic:
intro ⟨a, b⟩

Goal state after:
case refine_2
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))
a : ↑s
b : ↑(t a)
⊢ P
    ((algebraMap S
          ((fun x ↦
              match x with
              | ⟨a, b⟩ => Localization.Away ↑b)
            ⟨a, b⟩)).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
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)
⊢ ∀ (i : ↥sf × ↥sg),
    P
      ((algebraMap T
            ((fun x ↦
                match x with
                | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
              i)).comp
        (g.comp f))

Tactic:
intro ⟨a, b⟩

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
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)
a : ↥sf
b : ↥sg
⊢ P
    ((algebraMap T
          ((fun x ↦
              match x with
              | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
            (a, b))).comp
      (g.comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ (AffineTargetMorphismProperty.diagonal fun X x x_1 x_2 ↦ CompactSpace ↥X) = fun X x x_1 x_2 ↦ QuasiSeparatedSpace ↥X

Tactic:
by ext; exact quasiCompact_affineProperty_iff_quasiSeparatedSpace _

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

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

Tactic:
introv R _ _

Goal state after:
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
⊢ IsReduced S
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case zero
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
e : x ^ 0 = 0
⊢ x = 0

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
⊢ x = 0

Tactic:
· simpa using congr_arg (· * x) e

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
⊢ x = 0
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
⊢ x = 0

Tactic:
apply eq_zero_of_localization

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
⊢ ∀ (J : Ideal R) (x_1 : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) x = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height

Tactic:
refine le_iInf₂ (fun p hp ↦ ?_)

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ.refine_3
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
⊢ ↑(r + 1) ≤ (J ⊔ span {x}).height

Tactic:
refine le_iInf₂ (fun p hp ↦ ?_)

Goal state after:
case succ.refine_3
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
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
⊢ ↑(r + 1) ≤ p.primeHeight
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case refine_1
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₂ + n₁) * x ∈ I.ideal U

Tactic:
pow_add,

Goal state after:
case refine_1
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₂ * f ^ n₁ * x ∈ I.ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ J.ideal U

Tactic:
pow_add,

Goal state after:
case refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * f ^ n₂ * x ∈ J.ideal 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
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
P : Ideal ↑S
hP : P.IsPrime
H : Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP }))
⊢ Q (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)

Tactic:
hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)

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 : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
P : Ideal ↑S
hP : P.IsPrime
H :
  Q
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) { asIdeal := P, isPrime := hP }).asIdeal
          { asIdeal := P, isPrime := hP }.asIdeal (CommRingCat.Hom.hom φ) ⋯)))
⊢ Q (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hxU : x ∈ U
⊢ (hU.fromSpecStalk hxU) (closedPoint ↑(X.presheaf.stalk x)) = x

Tactic:
by
  rw [IsAffineOpen.fromSpecStalk, Scheme.Hom.comp_apply]
  rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ S.fromSpecResidueField (f T.x) =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ S.fromSpecResidueField (g T.y)

Tactic:
rw [← residueFieldCongr_fromSpecResidueField T.hx.symm,
    ← residueFieldCongr_fromSpecResidueField T.hy.symm]

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x) ≫ Hom.residueFieldMap (pullback.fst f g) t =
    ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y) ≫ Hom.residueFieldMap (pullback.snd f g) t

Tactic:
by
  simp [← residueFieldMap_comp, Scheme.Hom.residueFieldMap_congr pullback.condition]

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

Goal state before:
pp: X Y Z✝ : Scheme
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑g ∘ ⇑f)
Z : Set ↥X
hZ : IsClosed Z
⊢ IsClosed (⇑g '' ⇑f '' Z)

Tactic:
← Set.image_comp

Goal state after:
X Y Z✝ : Scheme
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑g ∘ ⇑f)
Z : Set ↥X
hZ : IsClosed Z
⊢ IsClosed (⇑g ∘ ⇑f '' Z)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsSeparated

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderComposition @IsSeparated

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsSeparated

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]
  infer_instance

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

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

Tactic:
rw [isSeparated_eq_diagonal_isClosedImmersion]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion ((pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv)

Tactic:
convert (inferInstance : IsClosedImmersion (pullback.mapDesc f (𝟙 _) g))

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv = pullback.mapDesc f (𝟙 Y) g
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).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder f)

Tactic:
refine .of_isPreimmersion _ ?_

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)
⊢ IsClosed (Set.range ⇑(Scheme.Hom.liftCoborder f))
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι : Type u_3
s : ι → S
hs : Ideal.span (Set.range s) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommRing (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (s i) (T i)
inst✝ : ∀ (i : ι), FinitePresentation R (T i)
⊢ FinitePresentation R S

Tactic:
by
  apply of_span_eq_top_target _ hs
  rintro - ⟨i, rfl⟩
  exact .equiv <| (IsLocalization.algEquiv (.powers <| s i) _ (T i)).symm |>.restrictScalars R

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
⊢ IsIso f

Tactic:
rw [IsClosedImmersion.isIso_iff_ker_eq_bot, ← Scheme.IdealSheafData.support_eq_top_iff,
    ← SetLike.coe_injective.eq_iff, Scheme.Hom.support_ker]
  simp

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

Goal state before:
pp: case inr
Y : Scheme
inst✝ : Subsingleton ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme} [Subsingleton ↥Y] (R : CommRingCat) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R),
    g ≫ f = 𝟙 Y → (∃ S, Y = Spec S) → IsClosedImmersion g
hY : ¬∃ S, Y = Spec S
inst : Subsingleton ↥(Spec Γ(Y, ⊤))
⊢ IsClosedImmersion (Y.isoSpec.inv ≫ g)

Tactic:
exact this R (f ≫ (Scheme.isoSpec Y).hom) ((Scheme.isoSpec Y).inv ≫ g)
      (by simp [reassoc_of% hg]) ⟨_, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
s : ↥S
K : Type u
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
⊢ IrreducibleSpace ↥(pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x)

Tactic:
let i : pullback ((f ≫ g).fiberToSpecResidueField s) x ⟶
      pullback (g.fiberToSpecResidueField s) x :=
    pullback.map _ _ _ _ (pullback.map _ _ _ _ f (𝟙 _) (𝟙 _) (by simp) (by simp)) (𝟙 _) (𝟙 _)
      (by simp [Scheme.Hom.fiberToSpecResidueField]) (by simp)

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
s : ↥S
K : Type u
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
⊢ IrreducibleSpace ↥(pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: X Y Z S : Scheme
⊢ HasAffineProperty @IsIntegralHom fun X x f x_1 ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral

Tactic:
change HasAffineProperty @IsIntegralHom (affineAnd RingHom.IsIntegral)

Goal state after:
X Y Z S : Scheme
⊢ HasAffineProperty (@IsIntegralHom) (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ RingHom.IsIntegral)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (s ∩ ↑(Scheme.Hom.opensRange (𝒰.f i)))

Tactic:
rw [Scheme.Hom.coe_opensRange, ← Set.image_preimage_eq_inter_range]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(𝒰.f i) '' ⇑(𝒰.f i) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ f = g

Tactic:
suffices f.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom =
      g.hom.comp (MvPolynomial.mapEquiv _ ULift.ringEquiv.symm).toRingHom by
    ext x
    · obtain ⟨x⟩ := x
      simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (C x)
    · simpa [-map_intCast, -eq_intCast] using! DFunLike.congr_fun this (X x)

Goal state after:
n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : Finite n
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ LocallyOfFinitePresentation (terminal.from (Spec ℤ[n]))

Tactic:
rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
    MorphismProperty.cancel_right_of_respectsIso (P := @LocallyOfFinitePresentation),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation), RingHom.FinitePresentation]

Goal state after:
n : Type u
S : Scheme
inst✝ : Finite n
this : IsIso (terminal.from (Spec (CommRingCat.of (ULift.{u, 0} ℤ))))
⊢ Algebra.FinitePresentation ↑(CommRingCat.of (ULift.{u, 0} ℤ)) ↑ℤ[n]