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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
x✝ : ↥↑U
x : ↥Z
y : ↥Y
hy : g y = x
⊢ g' y = ⟨x, ⋯⟩

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion (pullback.fst f (g' ≫ U.ι))

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝¹ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this✝ : Surjective g'
this : IsOpenImmersion (pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion (pullback.fst f' g' ≫ pullback.fst f U.ι)

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsIso (pullback.fst f' g')

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝¹ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this✝ : Surjective g'
this : IsIso (pullback.fst f' g')
⊢ IsIso g'

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝² : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this✝¹ : Surjective g'
this✝ : IsIso (pullback.fst f' g')
this : IsIso g'
⊢ Set.range ⇑g ⊆ Set.range ⇑U.ι

Tactic:
by

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

Goal state before:
pp: ⊢ IsOpenImmersion.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
this : ∀ {Y : Scheme} (g : Y ⟶ Spec R), P (pullback.fst (Spec.map φ) g) → (∃ S, Y = Spec S) → P g
hY : ¬∃ S, Y = Spec S
i : Y.affineCover.I₀
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map φ

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
this : ∀ {Y : Scheme} (g : Y ⟶ Spec R), P (pullback.fst (Spec.map φ) g) → (∃ S, Y = Spec S) → P g
hY : ¬∃ S, Y = Spec S
i : Y.affineCover.I₀
⊢ (Y.affineCover.f i ≫ g) ≫ 𝟙 (Spec R) = Y.affineCover.f i ≫ g

Tactic:
by

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat

Tactic:
rw [inf_comm]

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
h : IsStronglyTranscendental R x
inst✝ : FaithfulSMul R S
p : R[X]
hp : (aeval x) p = 0
⊢ ∀ (n : ℕ), p.coeff n = coeff 0 n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
x : K
⊢ IsStronglyTranscendental R x ↔ Transcendental R x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
⊢ (aeval (f x)) p * f u = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).QuasiFinite ↔ Algebra.QuasiFinite R S

Tactic:
by

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

Goal state before:
pp: T : Type u_3
inst✝² : CommRing T
R : Type u_4
S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
⊢ (f.comp g).QuasiFinite

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
⊢ IsAffine Y

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by

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

Goal state before:
pp: T : Type u_3
inst✝² : CommRing T
R : Type u_4
S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : S →+* T
g : R →+* S
h : (f.comp g).QuasiFinite
⊢ f.QuasiFinite

Tactic:
by

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

Goal state before:
pp: T : Type u_3
inst✝¹ : CommRing T
S : Type u_5
inst✝ : CommRing S
f : S →+* T
hf : f.Finite
⊢ f.QuasiFinite

Tactic:
by

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

Goal state before:
pp: R S T : Type u_6
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : (algebraMap R T).QuasiFinite
⊢ (algebraMap S (TensorProduct R S T)).QuasiFinite

Tactic:
rw [quasiFinite_algebraMap] at H ⊢

Goal state after:
R S T : Type u_6
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : Algebra.QuasiFinite R T
⊢ Algebra.QuasiFinite S (TensorProduct R S T)
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
by

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

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst✝ : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (pullback.fst f g)
⊢ Set.univ ⊆ Set.range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
⊢ IsStronglyTranscendental R x

Tactic:
by

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

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal R
x✝ : P.IsPrime
r : ↥s
⊢ Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp : (aeval ((algebraMap S T) x)) p * IsLocalization.mk' T u s = 0
⊢ ∃ a ∈ M, a * ((aeval x) p * u) = 0

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst✝ : IsZariskiLocalAtTarget P
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp : (aeval ((algebraMap S T) x)) p * IsLocalization.mk' T u s = 0
a : S
haM : a ∈ M
e : a * ((aeval x) p * u) = 0
⊢ (aeval x) p * (a * u) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x a✝ b✝ : S
ha : a✝ ∈ {a | ∀ (b : S), a * b ∈ R[x]}
hb : b✝ ∈ {a | ∀ (b : S), a * b ∈ R[x]}
c : S
⊢ (a✝ + b✝) * c ∈ R[x]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x b : S
⊢ 0 * b ∈ R[x]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x c a : S
ha : a ∈ {a | ∀ (b : S), a * b ∈ R[x]}
b : S
⊢ c • a * b ∈ R[x]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
hy : y ∈ ↑(conductor R x)
⊢ y ∈ ↑R[x]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
h : R[x] = ⊤
⊢ conductor R x = ⊤

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this : ∀ {Y : Scheme} (g : Y ⟶ Spec R), P (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ S, Y = Spec S) → P g
hY : ¬∃ S, Y = Spec S
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map φ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp : (aeval ((algebraMap S T) x)) p * IsLocalization.mk' T u s = 0
a : S
haM : a ∈ M
e : a * ((aeval x) p * u) = 0
⊢ map (algebraMap R T) p * C (a • (algebraMap S T) u) = 0

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this : ∀ {Y : Scheme} (g : Y ⟶ Spec R), P (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ S, Y = Spec S) → P g
hY : ¬∃ S, Y = Spec S
⊢ (Y.isoSpec.inv ≫ g) ≫ 𝟙 (Spec R) = Y.isoSpec.inv ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
⊢ IsStronglyTranscendental R ((algebraMap S T) x)

Tactic:
by

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

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝¹ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this✝ : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : ↑(P.primesOver S) := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm { asIdeal := J, isPrime := ⋯ }
this : ¬↑s ⊆ ↑↑I
r : S
hrs : r ∈ ↑s
hrI : r ∉ ↑↑I
⊢ Submonoid.powers r ≤ Submonoid.comap Algebra.TensorProduct.includeRight.toRingHom J.primeCompl

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : (aeval x) p * t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
⊢ (aeval x) (IsLocalization.integerNormalization M p) = a • (aeval x) p

Tactic:
by

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

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (fun {R S} [CommRing R] [CommRing S] ↦ QuasiFinite) ((algebraMap S (Localization.Away ↑r)).comp f✝)
algInst✝ : Algebra R S := f✝.toAlgebra
P : Ideal R
x✝ : P.IsPrime
this✝¹ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this✝ : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : ↑(P.primesOver S) := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm { asIdeal := J, isPrime := ⋯ }
this : ¬↑s ⊆ ↑↑I
r : S
hrs : r ∈ ↑s
hrI : r ∉ ↑↑I
⊢ ∀ (r_1 : R),
    (↑↑(IsLocalization.map (Localization.AtPrime J) Algebra.TensorProduct.includeRight.toRingHom ⋯)).toFun
        ((algebraMap R (Localization.Away r)) r_1) =
      (algebraMap R (Localization.AtPrime J)) r_1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : (aeval x) p * t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H : (aeval x) (IsLocalization.integerNormalization M p) = a • (aeval x) p
⊢ (aeval x) (IsLocalization.integerNormalization M p) * t = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : FaithfulSMul S L
x : S
y : L
⊢ y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
P x y : R[X]
hx✝ : x ∈ Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
hy✝ : y ∈ Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
x✝ : ℕ × ℕ
j₁ j₂ : ℕ
hj : (j₁, j₂) ∈ Finset.antidiagonal i
⊢ j₁ + j₂ = i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
P : R[X]
hP : P ∈ Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
i : ℕ
⊢ P.coeff i ∈ I ^ i

Tactic:
by

Goal state after: