mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (MvPolynomial.map (algebraMap R₀ R)) (P.jacobianOfHasCoeffs R₀) = P.jacobiMatrix.det

Tactic:
rw [jacobianOfHasCoeffs, @RingHom.map_det]

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ ((MvPolynomial.map (algebraMap R₀ R)).mapMatrix (P.ofHasCoeffs R₀).jacobiMatrix).det = P.jacobiMatrix.det
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
⊢ (cotangentCompAwaySec g P x) (cMulXSubOneCotangent T g) = x

Tactic:
by
  rw [← basisCotangentAway_apply _ (), cotangentCompAwaySec, Module.Basis.constr_basis]

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q).IsHomogeneous 2

pp: case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) q) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i))

Tactic:
· rw [hq]
      exact D.hphom i

Goal state after:
case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) q) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : f x ∈ V₂
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : ↑Γ(Y, ↑⟨V₂, hV₂⟩)
s : ↑Γ(X, ↑⟨V₁', hV₁'⟩)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
⊢ Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (algebraMap ↑Γ(Y, V₂) ↑Γ(Y, Y.basicOpen r)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁

Tactic:
rw [RingHom.algebraMap_toAlgebra, CommRingCat.ofHom_hom,
        g.appLE_map_assoc, Scheme.Hom.appLE_comp_appLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.negAddY P Q = -addU P Q

Tactic:
by
  rw [addU, neg_div, neg_neg, ← mul_div_mul_right _ _ <| mul_ne_zero hPz hQz,
    ← negAddY_of_X_eq' hP hQ hx, ← sq,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
x✝ : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P (((Scheme.Hom.isoOpensRange (𝒰.f (𝒰.idx x))).inv ≫ 𝒰.f (𝒰.idx x)) ≫ f)

Tactic:
Category.assoc,

Goal state after:
case refine_1
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
x✝ : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P ((Scheme.Hom.isoOpensRange (𝒰.f (𝒰.idx x))).inv ≫ 𝒰.f (𝒰.idx x) ≫ f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q = -(Q y ^ 2 * P z) * P y

Tactic:
negAddY_of_Z_eq_zero_right hQ hQz,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -(-(Q y ^ 2 * P z) * W'.negY P) - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q = -(Q y ^ 2 * P z) * P y
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P' ((T.isoSpec.inv ≫ p) ≫ f)

Tactic:
Category.assoc,

Goal state after:
case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P' (T.isoSpec.inv ≫ p ≫ f)
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:
intro _ _ f hf
    rwa [← flat_and_surjective_SpecMap_iff, and_comm]

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

Goal state before:
pp: case inr.refine_1
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
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) ((Y.isoSpec.inv ≫ p) ≫ f)

Tactic:
Category.assoc,

Goal state after:
case inr.refine_1
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
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) (Y.isoSpec.inv ≫ p ≫ f)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case mul
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 * y).coeff i ∈ I ^ i

Tactic:
coeff_mul

Goal state after:
case mul
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_1 ∈ Finset.antidiagonal i, x.coeff x_1.1 * y.coeff x_1.2 ∈ I ^ i
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
K : Type u_4
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : IsScalarTower R S K
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S K
x : S
H : Transcendental R ((algebraMap S K) x)
⊢ IsStronglyTranscendental R x

Tactic:
by
  have : FaithfulSMul R K := .trans R S K
  rw [← isStronglyTranscendental_iff_of_field] at H
  exact .of_map (f := IsScalarTower.toAlgHom R S K) (FaithfulSMul.algebraMap_injective _ _) H

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
⊢ ∀ x_1 ∈ l.support,
    (fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) x_1 (l x_1) ∈
      ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
intro y hy
    exact lem ((Finsupp.mem_supported _ l).mp H hy)

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

Goal state before:
pp: case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ -∑ x ∈ Finset.range (minpoly R s).natDegree, b • (s ^ (n - (minpoly R s).natDegree) * (minpoly R s).coeff x • s ^ x) ∈
    (algebraMap R S).range

Tactic:
mul_smul_comm,

Goal state after:
case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ -∑ x ∈ Finset.range (minpoly R s).natDegree, b • (minpoly R s).coeff x • (s ^ (n - (minpoly R s).natDegree) * s ^ x) ∈
    (algebraMap R S).range
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
i : ℕ
hi : i ∈ Finset.range (minpoly R s).natDegree
⊢ n - (minpoly R s).natDegree + i < n

Tactic:
simp only [Finset.mem_range] at hi

Goal state after:
case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
i : ℕ
hi : i < (minpoly R s).natDegree
⊢ n - (minpoly R s).natDegree + i < n
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Transcendental K Polynomial.X

Tactic:
exact Polynomial.transcendental_X K

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

Goal state before:
pp: case insert
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 : ℕ
⊢ IsIntegral R ((p a * ∏ x ∈ s, p x).coeff j)

Tactic:
coeff_mul

Goal state after:
case insert
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 : ℕ
⊢ IsIntegral R (∑ x ∈ Finset.antidiagonal j, (p a).coeff x.1 * (∏ x ∈ s, p x).coeff x.2)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case pos
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
hp : IsAlmostIntegral R[X] (C p)
hn : (C p).natDegree = n
hp' : (C p).natDegree = 0
⊢ IsAlmostIntegral R ((C p).coeff i)

Tactic:
simp only [coeff_C]

Goal state after:
case pos
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
hp : IsAlmostIntegral R[X] (C p)
hn : (C p).natDegree = n
hp' : (C p).natDegree = 0
⊢ IsAlmostIntegral R (if i = 0 then p else 0)
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
i : ℕ
hi : i ∈ Finset.range q.natDegree
⊢ (q.coeff i * (X ^ m) ^ i).natDegree < m * q.natDegree

Tactic:
simp only [Finset.mem_range] at hi

Goal state after:
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
i : ℕ
hi : i < q.natDegree
⊢ (q.coeff i * (X ^ m) ^ i).natDegree < m * q.natDegree
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyQuasiFinite f

Tactic:
rw [← f.liftCoborder_ι]
  have := HasRingHomProperty.of_isOpenImmersion (P := @LocallyQuasiFinite)
    RingHom.QuasiFinite.holdsForLocalizationAway.containsIdentities (f := f.coborderRange.ι)
  infer_instance

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

Goal state before:
pp: K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ { toFractionRing := Localization.mk 1 1 }.liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk 1 1 }

Tactic:
liftOn_ofFractionRing_mk,

Goal state after:
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (if h : φ ↑1 ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ 1) ⟨φ ↑1, h⟩ } else 0) =
    { toFractionRing := Localization.mk 1 1 }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (p * p') (q * q') }.liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk p q }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p' q' }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯

Tactic:
liftOn_ofFractionRing_mk,

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ (if h : φ ↑(q * q') ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ (p * p')) ⟨φ ↑(q * q'), h⟩ } else 0) =
    (if h : φ ↑q ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, h⟩ } else 0) *
      if h : φ ↑q' ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ p') ⟨φ ↑q', h⟩ } else 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ { toFractionRing := Localization.mk 0 1 }.liftOn (fun p q ↦ φ p / φ q) ⋯ = 0

Tactic:
liftOn_ofFractionRing_mk,

Goal state after:
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ φ 0 / φ ↑1 = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ { toFractionRing := Localization.mk 1 1 }.liftOn (fun p q ↦ φ p / φ q) ⋯ = 1

Tactic:
liftOn_ofFractionRing_mk,

Goal state after:
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ φ 1 / φ ↑1 = 1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ✝ : K[X] →ₐ[S] L
hφ✝ : K[X]⁰ ≤ Submonoid.comap φ✝ L⁰
φ : K[X] →ₐ[S] R[X]
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
r : S
⊢ (map φ hφ) ((algebraMap S K⟮X⟯) r) = (algebraMap S R⟮X⟯) r

Tactic:
algebraMap_apply r,

Goal state after:
K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ✝ : K[X] →ₐ[S] L
hφ✝ : K[X]⁰ ≤ Submonoid.comap φ✝ L⁰
φ : K[X] →ₐ[S] R[X]
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
r : S
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) ((algebraMap S K[X]) r) / (algebraMap K[X] K⟮X⟯) 1) =
    (algebraMap R[X] R⟮X⟯) ((algebraMap S R[X]) r) / (algebraMap R[X] R⟮X⟯) 1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ : K[X] →ₐ[S] L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
r : S
⊢ (liftRingHom ↑φ ⋯) ((algebraMap S K⟮X⟯) r) = (algebraMap S L) r

Tactic:
algebraMap_apply r,

Goal state after:
K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ : K[X] →ₐ[S] L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
r : S
⊢ (liftRingHom ↑φ ⋯) ((algebraMap K[X] K⟮X⟯) ((algebraMap S K[X]) r) / (algebraMap K[X] K⟮X⟯) 1) = (algebraMap S L) r