mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P : Fin 3 → F
⊢ (W'⁄K).dblU (⇑↑f ∘ P) = ↑f ((W'⁄F).dblU P)

Tactic:
← map_dblU,

Goal state after:
R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P : Fin 3 → F
⊢ (W'⁄K).dblU (⇑↑f ∘ P) = ((W'⁄F).map ↑f).dblU (⇑↑f ∘ P)
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q W : MorphismProperty C
A X✝ Y✝ Z : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z
g✝ : Y✝ ⟶ Z
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case e'_1
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
x✝ : K
⊢ ↑t = Set.range Subtype.val

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case e'_3.e'_2
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
e_1✝ : ↥(adjoin k ↑t) = ↥(adjoin k (Set.range Subtype.val))
⊢ ↑t = Set.range Subtype.val

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case e'_5
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
e_1✝ : ↥(adjoin k ↑t) = ↥(adjoin k (Set.range Subtype.val))
e_3✝ : (adjoin k ↑t).toField.toCommRing ≍ (adjoin k (Set.range Subtype.val)).toField.toCommRing
⊢ ↑t = Set.range Subtype.val

Tactic:
simp

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

Goal state before:
pp: R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
⊢ (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) f →
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
      (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)

Tactic:
hf

Goal state after:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective ⇑f
⊢ (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Injective ⇑(algebraMap S (S ⊗[R] T))
x✝ : S
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R T))) x✝) 1 =
    ((AlgebraTensorModule.curry (↑R (Algebra.linearMap S (S ⊗[R] T) ∘ₗ ↑(AlgebraTensorModule.rid R S S)))) x✝) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
x✝ : S
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R T))) x✝) 1 =
    ((AlgebraTensorModule.curry (↑R (Algebra.linearMap S (S ⊗[R] T) ∘ₗ ↑(AlgebraTensorModule.rid R S S)))) x✝) 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case e'_2.h₀
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯ ≫ pullback.fst Y.hom f =
    Over.Hom.left ((Over.pullback f).map a) ≫ pullback.fst Y.hom f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case h₁
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯ ≫ pullback.snd Y.hom f =
    Over.Hom.left ((Over.pullback f).map a) ≫ pullback.snd Y.hom f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case e'_3.h₀
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯ ≫ pullback.fst Y.hom f =
    Over.Hom.left ((Over.pullback f).map b) ≫ pullback.fst Y.hom f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case h₁
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯ ≫ pullback.snd Y.hom f =
    Over.Hom.left ((Over.pullback f).map b) ≫ pullback.snd Y.hom f

Tactic:
simp

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.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
g : Spec S ⟶ Spec R
h : P' f
hf : P (pullback.fst f g)
⊢ P g

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective g

Goal state after:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
h : P' f
φ : R ⟶ S
hf : P (pullback.fst f (Spec.map φ))
⊢ P (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this :
  ∀ {Y : Scheme} (g : Y ⟶ Spec R),
    IsIso (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ T, Y = Spec T) → isomorphisms Scheme g
hY : ¬∃ T, Y = Spec T
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map φ

Tactic:
simp

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

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this :
  ∀ {Y : Scheme} (g : Y ⟶ Spec R),
    IsIso (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ T, Y = Spec T) → isomorphisms Scheme g
hY : ¬∃ T, Y = Spec T
⊢ (Y.isoSpec.inv ≫ g) ≫ 𝟙 (Spec R) = Y.isoSpec.inv ≫ g

Tactic:
simp

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
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
⊢ (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → P g

Tactic:
hf

Goal state after:
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
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
⊢ P (pullback.fst f g) → P g
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_1
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine (Spec T)
ψ : R ⟶ T
hfst : IsIso (pullback.fst (Spec.map φ) (Spec.map ψ))
R✝ S✝ : CommRingCat
f : R✝ ⟶ S✝
⊢ (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
hf

Goal state after:
case refine_1
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine (Spec T)
ψ : R ⟶ T
hfst : IsIso (pullback.fst (Spec.map φ) (Spec.map ψ))
R✝ S✝ : CommRingCat
f : R✝ ⟶ S✝
hf : (@Surjective ⊓ @Flat) (Spec.map f)
⊢ (CommRingCat.Hom.hom f).FaithfullyFlat
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g

Tactic:
hf

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
⊢ IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g
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:
simp

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:
simp

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
this : (mapRingHom ↑f) (map (algebraMap R S) p * C u) = 0
⊢ map (algebraMap R S) p * C u = 0

Tactic:
map_eq_zero_iff

Goal state after:
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
this : map (algebraMap R S) p * C u = 0
⊢ map (algebraMap R S) p * C u = 0

case hf
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
this : (mapRingHom ↑f) (map (algebraMap R S) p * C u) = 0
⊢ Function.Injective ⇑(mapRingHom ↑f)
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:
simp

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

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

Tactic:
introv R hs H

Goal state after:
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)
⊢ f.QuasiFinite
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:
simp

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:
simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • a ^ n ∈ (algebraMap R S).range
s : R
hs : s ∈ R⁰
hs' : ∀ (n : ℕ), s • b ^ n ∈ (algebraMap R S).range
n i : ℕ
x✝ : i ∈ Finset.range (n + 1)
⊢ ↑(n.choose i) ∈ (algebraMap R S).range

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
s : R
t : ↥M
H : IsIntegral R (IsLocalization.mk' S s t)
⊢ ↑t • IsLocalization.mk' S s t ∈ (algebraMap R S).range

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsNoetherianRing R
inst✝¹ : IsDomain S
inst✝ : FaithfulSMul R S
s : S
H : IsAlmostIntegral R s
this : IsDomain R
x✝ : R
⊢ x✝ ∈ R⁰ → x✝ ∈ Submonoid.comap (algebraMap R S) S⁰

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ RatFunc.mk p 0 = { toFractionRing := 0 }

Tactic:
mk_eq_div',

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) 0 } =
    { toFractionRing := 0 }
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommSemiring A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : 1 < v w
p : A[X]
hp : p ≠ 0
⊢ p.natDegree ∈ Finset.range (p.natDegree + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
c : K
⊢ (C c).num.natDegree = 0 ∧ (C c).denom.natDegree = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : ι → S[X]
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) → ∀ (j : ℕ), IsIntegral R ((s.prod p).coeff j)
H : ∀ i ∈ insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
i : ℕ × ℕ
hi : i ∈ Finset.antidiagonal j
⊢ a ∈ insert a s

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset ι
p : ι → S[X]
H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R ((s.prod p).coeff j)

Tactic:
by
  classical
  induction s using Finset.induction generalizing j with
  | empty => simp [coeff_one, apply_ite, isIntegral_zero, isIntegral_one]
  | insert a s has IH =>
    rw [Finset.prod_insert has, coeff_mul]
    exact IsIntegral.sum _ fun i hi ↦ .mul (H _ (by simp) _) (IH (fun _ _ ↦ H _ (by aesop)) _)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n✝ : ℕ
IH : ∀ m < n✝, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n✝
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • p.leadingCoeff ^ n ∈ (algebraMap R S).range
n : ℕ
s : R
hs : (algebraMap R S) s = r • p.leadingCoeff ^ n
⊢ C r • C p.leadingCoeff ^ n ∈ (algebraMap R[X] S[X]).range

Tactic:
exact ⟨C s, by simp [Algebra.smul_def, hs]⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
⊢ (algebraMap R[X] S[X]) X = X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
⊢ ↑f.vars ⊆ Set.range Subtype.val

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ (rename Subtype.val) g = ((rename Subtype.val).comp (killCompl ⋯)).toRingHom ((rename Subtype.val) g)

Tactic:
simp

Goal state after: