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
P : Presentation 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₀
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp (P.tensorModelOfHasCoeffsInv R₀) = AlgHom.id R S

Tactic:
have h : Function.Surjective
      ((P.quotientEquiv.restrictScalars R).toAlgHom.comp (Ideal.Quotient.mkₐ _ _)) :=
    (P.quotientEquiv.restrictScalars R).surjective.comp Ideal.Quotient.mk_surjective

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
P : Presentation 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₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp (P.tensorModelOfHasCoeffsInv R₀) = AlgHom.id R S
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
P : Presentation 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₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ ((P.tensorModelOfHasCoeffsHom R₀).comp
          ((Ideal.Quotient.liftₐ P.ker
                ((TensorProduct.map (AlgHom.id R R)
                      (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
                  ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
                ⋯).comp
            ↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm)).comp
      ((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)

Tactic:
AlgHom.comp_assoc,

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
P : Presentation 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₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      (((Ideal.Quotient.liftₐ P.ker
                ((TensorProduct.map (AlgHom.id R R)
                      (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
                  ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
                ⋯).comp
            ↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm).comp
        ((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)
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
P : Presentation 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₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      (((Ideal.Quotient.liftₐ P.ker
                ((TensorProduct.map (AlgHom.id R R)
                      (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
                  ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
                ⋯).comp
            ↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm).comp
        ((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)

Tactic:
AlgHom.comp_assoc,

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
P : Presentation 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₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        ((↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm).comp
          ((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)))) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)
Module: Mathlib.RingTheory.Extension.Cotangent.Free

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
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
x : P.toExtension.CotangentSpace
hx : x ∈ ↑P.toExtension.toKaehler.ker
hxs : x ∈ ↑(Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
⊢ x = 0

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
x : P.toExtension.CotangentSpace
hx : x ∈ ↑P.toExtension.toKaehler.ker
hxs : x ∈ Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x))
⊢ x = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.addZ (u • P) (v • Q) = (u * v) ^ 2 * W'.addZ P Q

Tactic:
simp only [addZ, smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q z) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P z) +
                        (u * P y) ^ 2 * (v * Q z) ^ 2 -
                      (v * Q y) ^ 2 * (u * P z) ^ 2 +
                    W'.a₁ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
                  W'.a₁ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 -
                W'.a₂ * (u * P x) ^ 2 * (v * Q z) ^ 2 +
              W'.a₂ * (v * Q x) ^ 2 * (u * P z) ^ 2 +
            W'.a₃ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
          W'.a₃ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) -
        W'.a₄ * (u * P x) * (u * P z) * (v * Q z) ^ 2 +
      W'.a₄ * (v * Q x) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
                      W'.a₁ * P x * P y * Q z ^ 2 -
                    W'.a₁ * Q x * Q y * P z ^ 2 -
                  W'.a₂ * P x ^ 2 * Q z ^ 2 +
                W'.a₂ * Q x ^ 2 * P z ^ 2 +
              W'.a₃ * P y * P z * Q z ^ 2 -
            W'.a₃ * Q y * P z ^ 2 * Q z -
          W'.a₄ * P x * P z * Q z ^ 2 +
        W'.a₄ * Q x * P z ^ 2 * Q z)
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case 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
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ D.P.coeffs.Finite

Tactic:
exact Presentation.finite_coeffs

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

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ Nat.card ι - Nat.card σ = n

Tactic:
← e,

Goal state after:
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ Nat.card ι - Nat.card σ = P.dimension
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case 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
⊢ ∃ p_1,
    p_1.IsHomogeneous 2 ∧
      (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p_1 =
        (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i)

Tactic:
refine ⟨q, .of_map hinj ?_, hinj ?_⟩

Goal state after:
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

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.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addX P Q = P y ^ 2 * Q z * Q x

Tactic:
rw [addX, hPz, X_eq_zero_of_Z_eq_zero hP hPz]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -0 * Q y ^ 2 * 0 + Q x * P y ^ 2 * Q z - 2 * 0 * P y * Q y * Q z + 2 * Q x * P y * Q y * 0 -
                            W'.a₁ * 0 ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * 0 +
                        W'.a₂ * 0 ^ 2 * Q x * Q z -
                      W'.a₂ * 0 * Q x ^ 2 * 0 -
                    W'.a₃ * 0 * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * 0 ^ 2 -
                2 * W'.a₃ * 0 * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * 0 ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * 0 ^ 2 +
        3 * W'.a₆ * 0 * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q x
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Etale ↔ IsStandardSmoothOfRelativeDimension 0 f

Tactic:
algebraize [f]
  exact Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
rw [← formallySmooth_algebraMap]
    exact RingHom.FormallySmooth.respectsIso.arrow_mk_iso_iff
      (IsAffineOpen.arrowStalkMapIso f U hU V hV hVU hx)

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

Goal state before:
pp: ⊢ @Etale = @SmoothOfRelativeDimension 0

Tactic:
apply HasRingHomProperty.ext

Goal state after:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    f.Etale ↔ RingHom.Locally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0

Tactic:
obtain ⟨g, hg, eq⟩ := (((minpoly k' (a i)).separable_or p (minpoly.irreducible
    (isAlgebraic_iff_isIntegral.mp <| isAlgebraic_adjoin_iff.mpr alg))).resolve_left Hsep).2

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq : (Polynomial.expand (↥k') p) g = minpoly (↥k') (a i)
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝¹ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(Z, W) := (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst✝ : Algebra.FormallyUnramified ↑Γ(Y, U) ↑Γ(X, V)
r : ↑Γ(Y, U)
⊢ (↑↑(CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯))).toFun ((algebraMap ↑Γ(Y, U) ↑Γ(X, V)) r) =
    (algebraMap ↑Γ(Y, U) ↑Γ(Z, W)) r

Tactic:
by
    simp [RingHom.algebraMap_toAlgebra, ← CategoryTheory.comp_apply, -CommRingCat.hom_comp,
      Scheme.Hom.appLE_comp_appLE]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr
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
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this : ExpChar k p
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
have : CharP K p := .of_ringHom_of_ne_zero (algebraMap k K) p hp.out.ne_zero

Goal state after:
case inr
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
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K
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
this : map (algebraMap S T) (map (algebraMap R S) (IsLocalization.integerNormalization M p)) * C t = 0
⊢ map (algebraMap S T) p * C t = 0

Tactic:
ha₂

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
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
this : map (algebraMap S T) (a • p) * C t = 0
⊢ map (algebraMap S T) p * C t = 0
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
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval x) p * u ∈ q
this✝¹ : q.IsPrime
this✝ : Ring.KrullDimLE 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := ⋯.toField
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0

Tactic:
obtain ⟨⟨m, hmq⟩, hm⟩ := (IsLocalization.map_eq_zero_iff q.primeCompl (Localization.AtPrime q)
    (aeval x p * u)).mp (by rw [← Ideal.mem_bot, ← IsLocalRing.maximalIdeal_eq_bot,
      ← Localization.AtPrime.map_eq_maximalIdeal]; exact Ideal.mem_map_of_mem _ e)

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval x) p * u ∈ q
this✝¹ : q.IsPrime
this✝ : Ring.KrullDimLE 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := ⋯.toField
m : S
hmq : m ∈ q.primeCompl
hm : ↑⟨m, hmq⟩ * ((aeval x) p * u) = 0
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0
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
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
⊢ (l.sum fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) ∈
    ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
have lem : ∀ {a : R}, a ∈ I → l a • algebraMap R S a * algebraMap R S p ∈
      algebraMap R<x> S '' I.map (algebraMap R R<x>) := by
    intro a ha
    rw [smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]
    refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?h⟩) ?_
    case h =>
      rw [mul_comm]
      exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _
    · refine ⟨?_, ?_⟩
      · rw [mul_comm]
        apply Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ ha)
      · simp only [map_mul, mul_comm (algebraMap R S p) (l a)]
        rfl

Goal state after:
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)
⊢ (l.sum fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) ∈
    ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
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
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
n : ℕ
a : R
ha : (algebraMap R S) a = r • s ^ n
this :
  (algebraMap S (Localization.Away ((algebraMap R S) r))) (s ^ n) *
        (algebraMap S (Localization.Away ((algebraMap R S) r))) ((algebraMap R S) r) *
      Localization.Away.invSelf ((algebraMap R S) r) =
    (algebraMap S (Localization.Away ((algebraMap R S) r))) (s ^ n)
⊢ a • Localization.Away.invSelf ((algebraMap R S) r) =
    (IsScalarTower.toAlgHom R S (Localization.Away ((algebraMap R S) r))).toLinearMap ((fun x ↦ s ^ x) n)

Tactic:
by
      simpa [Algebra.smul_def, IsScalarTower.algebraMap_apply R S (Localization.Away _),
        ha, mul_assoc, mul_left_comm] using this

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
⊢ J.primeCompl ≤
    Submonoid.comap
      ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField)))
      (IsUnit.submonoid (RatFunc I.ResidueField))

Tactic:
rintro x (hx : x ∉ J)
      suffices ∃ i, x.coeff i ∉ I by simpa [IsUnit.mem_submonoid_iff, Polynomial.ext_iff]
      contrapose! hx
      rwa [hJ, Ideal.mem_map_C_iff]

Goal state after: