mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
⊢ 1 - (Ideal.Quotient.mk J') (f₁ (Pi.single x 1)) = 0

Tactic:
← (Ideal.Quotient.mk J').map_one,

Goal state after:
case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
⊢ (Ideal.Quotient.mk J') 1 - (Ideal.Quotient.mk J') (f₁ (Pi.single x 1)) = 0
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ 1 - (Ideal.Quotient.mk J') (f₂ (Pi.single x 1)) = 0

Tactic:
← (Ideal.Quotient.mk J').map_one,

Goal state after:
case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ (Ideal.Quotient.mk J') 1 - (Ideal.Quotient.mk J') (f₂ (Pi.single x 1)) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
simp only [dblX, smul_fin3_ext]
  ring1

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
a : A
this : Algebra.IsPushout R A S B
b : A ⊗[R] S
⊢ (tensorKaehlerEquiv R S A B) ((Algebra.IsPushout.equiv R A S B) b ⊗ₜ[A] (D R A) a) =
    (Algebra.IsPushout.equiv R A S B) b • (D S B) ((algebraMap A B) a)

Tactic:
induction b with

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Finite σ
T : Type u_1
ι' : Type u_2
σ' : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Finite σ'
Q : SubmersivePresentation S T ι' σ'
P : SubmersivePresentation R S ι σ
⊢ IsUnit (Q.comp P.toPreSubmersivePresentation).jacobian

Tactic:
by
    rw [comp_jacobian_eq_jacobian_smul_jacobian, Algebra.smul_def, IsUnit.mul_iff]
    exact ⟨RingHom.isUnit_map _ <| P.jacobian_isUnit, Q.jacobian_isUnit⟩

Goal state after:
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.ofHasCoeffs R₀).jacobiMatrix.det = P.jacobiMatrix.det

Tactic:
@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.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
by
  simp only [negDblY, smul_fin3_ext]
  ring1

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

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 ι σ
⊢ Subsingleton P.toExtension.H1Cotangent

Tactic:
rw [Algebra.Extension.subsingleton_h1Cotangent]
  exact cotangentComplex_injective P

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a.a
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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : P.Ring
hx : x ∈ P.ker ^ 2
⊢ x ∈ Ideal.comap ((localizationAway T g).toComp P).toAlgHom (RingHom.ker (compLocalizationAwayAlgHom T g P))

Tactic:
simp only [Ideal.mem_comap, RingHom.mem_ker,
        compLocalizationAwayAlgHom_toAlgHom_toComp (T := T) g P x]

Goal state after:
case a.a
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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
x : P.Ring
hx : x ∈ P.ker ^ 2
⊢ (algebraMap P.Ring (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)))) x = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Smooth R S
⊢ ∃ s, Ideal.span s = ⊤ ∧ ∀ x ∈ s, IsStandardSmooth R (Localization.Away x)

Tactic:
by
  choose f hf₁ hf₂ using IsSmoothAt.exists_notMem_isStandardSmooth R (S := S)
  /- #adaptation_note Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), the original proof was:
  `refine ⟨Set.range (fun p : PrimeSpectrum S ↦ f p.asIdeal), ?_, by grind⟩`
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. -/
  refine ⟨Set.range (fun p : PrimeSpectrum S ↦ f p.asIdeal), ?_, by
    simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]; intro; apply hf₂⟩
  simp [← PrimeSpectrum.iSup_basicOpen_eq_top_iff, TopologicalSpace.Opens.ext_iff, Set.ext_iff]
  grind

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

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
inst✝² : Module.Flat R S
inst✝¹ : IsNoetherianRing S
inst✝ : FormallySmooth R A
this : Module.Flat R (AdicCompletion (RingHom.ker f) S)
⊢ Module.Flat R A

Tactic:
obtain ⟨g, hg⟩ := exists_kerProj_comp_eq_id f hf

Goal state after:
R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
inst✝² : Module.Flat R S
inst✝¹ : IsNoetherianRing S
inst✝ : FormallySmooth R A
this : Module.Flat R (AdicCompletion (RingHom.ker f) S)
g : A →ₐ[R] AdicCompletion (RingHom.ker f) S
hg : (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
⊢ Module.Flat R A
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

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_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ Set.range (Subtype.val ∘ D.f ∘ ⇑b) ⊆ ↑(RingHom.ker (aeval P.val))

Tactic:
Set.range_subset_iff

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_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ ∀ (y : σ), (Subtype.val ∘ D.f ∘ ⇑b) y ∈ ↑(RingHom.ker (aeval P.val))
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
⊢ Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)) ⊆
    ↑(RingHom.ker
        ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (RingHom.ker
                  (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                2)).comp
          (aeval p)))

Tactic:
Set.range_subset_iff

Goal state after:
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
⊢ ∀ (y : D.rels),
    Presentation.relationOfHasCoeffs (↥(subalgebra R D)) y ∈
      ↑(RingHom.ker
          ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                (RingHom.ker
                    (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                      (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                  2)).comp
            (aeval p)))
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: 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
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n A B
ι σ : Type
w✝¹ : Finite σ
w✝ : Finite ι
P : SubmersivePresentation A B ι σ
hP : P.dimension = n
A₀ : Subalgebra R A := adjoin R P.coeffs
this : P.HasCoeffs ↥A₀
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
exact ⟨A₀, (P.ModelOfHasCoeffs A₀:), inferInstance, inferInstance,
    ⟨P.finite_coeffs.toFinset, by simp [A₀]⟩, ⟨_, _, _, inferInstance,
      P.ofHasCoeffs A₀, hP⟩, ⟨(P.tensorModelOfHasCoeffsEquiv A₀).symm⟩⟩

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

Goal state before:
pp: n m : ℕ
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f

Tactic:
affineLocally_iff_forall_isAffineOpen

Goal state after:
n m : ℕ
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
⊢ smoothLocus f = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
⊢ ⊤ ≤ smoothLocus f
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := ⋯
⊢ (Scheme.Hom.appTop f).hom'.IsIntegral

Tactic:
exact isIntegral_appTop_of_universallyClosed f

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale) f

Tactic:
affineLocally_iff_forall_isAffineOpen

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale
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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF'' : (aeval a) (C (coeff 0 F'')) = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ F'' = 0

Tactic:
aeval_C,

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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF'' : (algebraMap k K) (coeff 0 F'') = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ F'' = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified) ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FormallyUnramified) f

Tactic:
affineLocally_iff_forall_isAffineOpen

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Goal state before:
pp: W P Q : MorphismProperty Scheme
X✝ Y✝ : Scheme
inst✝² : W.IsStableUnderBaseChange
inst✝¹ : Scheme.IsJointlySurjectivePreserving W
inst✝ : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
x✝ : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ g ≫ f)

Tactic:
rw [← Category.assoc]

Goal state after:
W P Q : MorphismProperty Scheme
X✝ Y✝ : Scheme
inst✝² : W.IsStableUnderBaseChange
inst✝¹ : Scheme.IsJointlySurjectivePreserving W
inst✝ : P.RespectsRight Q
X Y Z : Scheme
f : Y ⟶ Z
hf : Q f
g : X ⟶ Y
x✝ : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hg : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ g)
i : 𝒰.I₀
⊢ P ((𝒰.f i ≫ g) ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyOpen (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsOpen s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsOpen
    (⇑(pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)) ''
      ⇑(pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
            (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯) ⁻¹'
        s)

Tactic:
exact p.isOpenMap _ (hs.preimage r.continuous)

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

Goal state before:
pp: case inr.refine_2
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 (pullback.fst (Y.isoSpec.inv ≫ p) (pullback.fst f g))

Tactic:
exact P.pullback_fst _ _ h

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
⊢ f.QuasiFinite

Tactic:
refine ⟨fun P _ ↦ ?_⟩

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)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal R
x✝ : P.IsPrime
⊢ Module.Finite P.ResidueField (P.Fiber S)
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
  trans ∀ z, y * (algebraMap S L) z ∈ (R[x]).map (IsScalarTower.toAlgHom R S L)
  · simp only [coeSubmodule, Submodule.mem_map, linearMap_apply, Subalgebra.mem_map,
      IsScalarTower.coe_toAlgHom']
    constructor
    · rintro ⟨y, hy, rfl⟩ z
      exact ⟨_, hy z, map_mul _ _ _⟩
    · intro H
      obtain ⟨y, _, e⟩ := H 1
      rw [map_one, mul_one] at e
      subst e
      simp only [← map_mul, (FaithfulSMul.algebraMap_injective S L).eq_iff,
        exists_eq_right] at H
      exact ⟨_, H, rfl⟩
  · rw [AlgHom.map_adjoin, Set.image_singleton]; rfl

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

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
e : eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p = 0
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
⊢ (aeval x) q = 0

Tactic:
replace e := congr(($e).coeff p.natDegree)

Goal state after:
case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  (eval₂ (algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (C x * X) p).coeff p.natDegree =
    coeff 0 p.natDegree
⊢ (aeval x) q = 0
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
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed K[X]
⊢ IsIntegrallyClosedIn R[X] K[X]

Tactic:
refine isIntegrallyClosedIn_iff.mpr ⟨map_injective _ (IsFractionRing.injective _ _), ?_⟩

Goal state after:
R✝ : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S
inst✝³ : Algebra R✝ S
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
K : Type u_4 := FractionRing R
this : IsIntegrallyClosed K[X]
⊢ ∀ {x : K[X]}, IsIntegral R[X] x → ∃ y, (algebraMap R[X] K[X]) y = x