mathlib-initiative/mathlib-tactics huggingface dataset:
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
D : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ ↑(D.p i).coeffs
this : ↑p.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs
⊢ p ∈ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `rw`. 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. The original proof was:
  `grind [MvPolynomial.mem_range_map_iff_coeffs_subset, subalgebra,
    Subalgebra.setRange_algebraMap, Algebra.subset_adjoin]` -/

Goal state after:
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
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ ↑(D.p i).coeffs
this : ↑p.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs
⊢ p ∈ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
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
D : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ ↑(D.q i).coeffs
this : ↑q.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)
⊢ q ∈ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `rw`. 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. The original proof was:
  `grind [MvPolynomial.mem_range_map_iff_coeffs_subset, subalgebra,
    Subalgebra.setRange_algebraMap, Algebra.subset_adjoin]` -/

Goal state after:
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
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ ↑(D.q i).coeffs
this : ↑q.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)
⊢ q ∈ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
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
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
⊢ ∃ g, g.Etale

Tactic:
algebraize [φ.toRingHom, (algebraMap P.Ring S).comp φ.toRingHom]

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
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
⊢ ∃ g, g.Etale
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
D : DescentAux A B
⊢ ∃ σ₀,
    (Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
        σ₀ =
      AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))

Tactic:
by
  choose p hp using fun i ↦ (D.h i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_h_subset R i)
  refine ⟨?_, ?_⟩
  · refine Ideal.Quotient.liftₐ _ ((Ideal.Quotient.mkₐ _ _).comp <| aeval p) ?_
    simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]
    intro i
    simp only [← AlgHom.comap_ker, Ideal.coe_comap, Set.mem_preimage, SetLike.mem_coe]
    rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker,
      ← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]
    have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)
    rw [Ideal.mem_span_pow_iff_exists_isHomogeneous]
    obtain ⟨q, hq⟩ := (D.p i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_p_subset R i)
    refine ⟨q, .of_map hinj ?_, hinj ?_⟩
    · rw [hq]
      exact D.hphom i
    · simp_rw [map_eval, Function.comp_def, Presentation.map_relationOfHasCoeffs,
        hq, D.hp, MvPolynomial.map_aeval, hp]
      simp [MvPolynomial.eval₂_map_comp_C, Presentation.map_relationOfHasCoeffs, aeval_def]
  · have hf₀ : Function.Surjective f₀ := Ideal.Quotient.mk_surjective
    rw [← AlgHom.cancel_right hf₀]
    refine MvPolynomial.algHom_ext fun i ↦ ?_
    suffices h : ∃ p', p'.IsHomogeneous 1 ∧ (eval (D.P.relationOfHasCoeffs (D.subalgebra R))) p' =
        p i - X i by
      -- Reducible def-eq issues caused by `RingHom.ker f.toRingHom` discrepancies
      -- Can be fixed after #25138.
      apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
      simpa [Ideal.mem_span_iff_exists_isHomogeneous, hp]
    have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)
    obtain ⟨t, ht⟩ := (D.q i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_q_subset R i)
    refine ⟨t, .of_map hinj ?_, hinj ?_⟩
    · rw [ht]
      exact D.hqhom i
    · simp [MvPolynomial.map_eval, Function.comp_def,
        Presentation.map_relationOfHasCoeffs, ht, hq, hp]

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
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
P'✝ : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators := Algebra.Generators.ofSurjective (fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) ⋯;
  { toGenerators := __Generators, relation := ⇑e.symm ∘ P.relation, span_range_relation_eq_ker := ⋯, map := _root_.id,
    map_inj := ⋯ }
P' : Algebra.SubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  let __spread.0 := P'✝;
  { toPreSubmersivePresentation := __spread.0, jacobian_isUnit := ⋯ }
⊢ P'.dimension = 0

Tactic:
by simp [Algebra.Presentation.dimension]

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

Goal state before:
pp: X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : LocallyOfFinitePresentation g
⊢ f ⁻¹ᵁ smoothLocus g = smoothLocus (f ≫ g)

Tactic:
ext x
  refine (RingHom.FormallySmooth.respectsIso.cancel_right_isIso _ (f.stalkMap x)).symm.trans ?_
  rw [← CommRingCat.hom_comp, ← stalkMap_comp]
  rfl

Goal state after:
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''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
⊢ F''.totalDegree ≠ 0

Tactic:
contrapose hF''0

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'' : (aeval a) F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
⊢ F'' = 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
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] =
    ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addXYZ P Q z]

Tactic:
addXYZ_Z

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] =
    ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q]
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
⊢ IsDominant i

Tactic:
obtain ⟨n, hn⟩ := hi

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ IsDominant i
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case refine_1
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)
ψ₁ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
⊢ IsNilpotent (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))

Tactic:
obtain ⟨n, hn⟩ := hi

Goal state after:
case refine_1
X Y Z' Z : Scheme
i : Z' ⟶ Z
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)
ψ₁ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] ↑Γ(Z, W) := { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ IsNilpotent (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: 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 = ⊤
⊢ Algebra.IsAlgebraic (↥⊤) K

Tactic:
Algebra.isAlgebraic_iff_isIntegral

Goal state after:
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 = ⊤
⊢ Algebra.IsIntegral (↥⊤) 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
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective ⇑(algebraMap R S)
t : T
p : R[X]
hp : (aeval x) (map (algebraMap R S) p) * t = 0
⊢ (aeval x) p * t = 0

Tactic:
by simpa using hp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
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✝ : IsFractionRing S K
x : S
⊢ IsStronglyTranscendental R x ↔ Transcendental R ((algebraMap S K) x)

Tactic:
by
  have : FaithfulSMul R K := .trans R S K
  rw [← IsStronglyTranscendental.iff_of_isLocalization (T := K) le_rfl,
    isStronglyTranscendental_iff_of_field]

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_1
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
a : R
ha : a ∈ I
⊢ ⟨l a * (algebraMap R S) p, ⋯⟩ * (algebraMap R ↥R[x]) a ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
apply Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ ha)

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 : ℕ
⊢ (r * s) • (a ^ n * b ^ n) ∈ (algebraMap R S).range

Tactic:
mul_smul_mul_comm

Goal state after:
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 : ℕ
⊢ r • a ^ n * s • b ^ n ∈ (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
⊢ -∑ 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

Tactic:
← pow_add,

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 + x) ∈
    (algebraMap R S).range
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom

Tactic:
rw [Polynomial.eval₂_mul] at this

Goal state after:
case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

Tactic:
rw [Polynomial.eval₂_mul] at this

Goal state after:
case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
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
p✝ : S[X]
hp✝ : IsAlmostIntegral R[X] p✝
i : ℕ
q : S[X]
p : R[X]
hp : p ∈ R[X]⁰
hp' : ∀ (n : ℕ), p • q ^ n ∈ (algebraMap R[X] S[X]).range
⊢ p.leadingCoeff ∈ R⁰

Tactic:
by simpa using hp

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

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

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally @IsFinite] at ‹IsFinite f›
  rw [HasRingHomProperty.eq_affineLocally @LocallyQuasiFinite]
  refine ((targetAffineLocally_affineAnd_eq_affineLocally
    RingHom.QuasiFinite.propertyIsLocal).le f ?_).2
  exact targetAffineLocally_affineAnd_le (fun hf ↦ .of_finite hf) f ‹_›

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
algInst✝³ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) := (CommRingCat.Hom.hom αU).toAlgebra
algInst✝² : Algebra ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f))) := (CommRingCat.Hom.hom αUf).toAlgebra
algInst✝¹ : Algebra ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  (CommRingCat.Hom.hom (F.map ⋯.hom.op)).toAlgebra
algInst✝ : Algebra ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  ((CommRingCat.Hom.hom (F.map ⋯.hom.op)).comp (CommRingCat.Hom.hom αU)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op U)) ↑(F.obj (Opposite.op (U.basicOpen f))) :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑Γ(X, U.toOpens) ↑(F.obj (Opposite.op (U.basicOpen f)))))
this✝ : IsScalarTower ↑Γ(X, U.toOpens) ↑Γ(X, X.basicOpen f) ↑(F.obj (Opposite.op (U.basicOpen f)))
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (↑(F.1 (Opposite.op U))) (Submonoid.powers f))
      ↑(F.1 (Opposite.op (U.basicOpen f))) ↔
    IsLocalization.Away ((ConcreteCategory.hom αU) f) ↑(F.obj (Opposite.op (U.basicOpen f)))

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Goal state after: