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₀
inst✝¹ : Finite ι
inst✝ : Finite σ
⊢ FinitePresentation R₀ (ModelOfHasCoeffs R₀)

Tactic:
classical
  cases nonempty_fintype σ
  exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩

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 ι σ
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
⊢ ∑ i, ⋯.choose i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1

Tactic:
convert! P.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one.choose_spec

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 ι σ
this :
  Function.Injective
    (⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘
      ⇑(Finsupp.lcomapDomain P.map ⋯) ∘ ⇑P.cotangentSpaceBasis.repr ∘ ⇑P.toExtension.cotangentComplex)
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Tactic:
exact Function.Injective.of_comp (Function.Injective.of_comp <| Function.Injective.of_comp this)

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : Unit
⊢ (cotangentCompLocalizationAwayEquiv D.gbar D.presLeft.toGenerators ⋯).symm (0, cMulXSubOneCotangent S D.gbar) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩

Tactic:
exact cotangentCompLocalizationAwayEquiv_symm_inr _ _ _

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 := ⋯ }
i j : σ
⊢ e ((MvPolynomial.pderiv i) (e.symm (P.relation j))) = (MvPolynomial.pderiv (P.map i)) (P.relation j)

Tactic:
simp [e, ← MvPolynomial.pderiv_rename e₀.injective, show e₀ (Sum.inl i) = P.map i from 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
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
⊢ Irreducible (F.toPolynomialAdjoinImageCompl a i)

Tactic:
classical
  unfold toPolynomialAdjoinImageCompl
  have hc : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; simp
  let d : {j // j ≠ i} ≃ {j | j ≠ i} := .subtypeEquivRight (by simp)
  refine (congrArg Irreducible ?_).mp <|
    hF.map (renameEquiv k ((Equiv.optionSubtypeNe i).symm)) |>.map
      (optionEquivLeft k _) |>.map (Polynomial.mapAlgEquiv <|
        (renameEquiv k d).trans <| H.aevalEquiv.trans
        (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $hc.symm)))
  rw [Polynomial.coe_mapAlgEquiv, Polynomial.coe_mapAlgHom]
  refine congrFun (congrArg Polynomial.map ?_) _
  ext <;> simp [d]

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
⊢ (p * F''.support.sup fun s ↦ s.sum fun x e ↦ e) ≤ F.totalDegree

Tactic:
Finset.mul_sup₀,

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''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
⊢ (F''.support.sup fun x ↦ p * x.sum fun x e ↦ e) ≤ F.totalDegree
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblXYZ (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P

Tactic:
by
  simp only [dblXYZ, map_dblX, map_dblY, map_dblZ, comp_fin3]

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

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

Tactic:
rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝¹ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this✝ : Surjective g'
this : IsIso (pullback.fst f' g')
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f'

Tactic:
exact MorphismProperty.pullback_snd _ _ hf

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝² : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this✝¹ : Surjective g'
this✝ : IsIso (pullback.fst f' g')
this : IsIso g'
⊢ IsOpenImmersion g

Tactic:
rw [← IsOpenImmersion.lift_fac U.ι g (by simp [U])]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝² : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this✝¹ : Surjective g'
this✝ : IsIso (pullback.fst f' g')
this : IsIso g'
⊢ IsOpenImmersion (IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι)
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: T : Type u_3
inst✝² : CommRing T
R : Type u_4
S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
algInst✝² : Algebra S T := f.toAlgebra
algInst✝¹ : Algebra R S := g.toAlgebra
algInst✝ : Algebra R T := (f.comp g).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.QuasiFinite S T
algebraizeInst✝ : Algebra.QuasiFinite R S
⊢ (f.comp g).QuasiFinite

Tactic:
exact .trans R S T

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
P : Ideal R
x✝ : P.IsPrime
this✝ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
⊢ (algebraMap (P.Fiber S) (Localization.AtPrime J)) a = 0

Tactic:
let I := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm ⟨J, inferInstance⟩

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
this✝ : ∀ (r : ↥s), Module.Finite P.ResidueField (P.Fiber (Localization.Away ↑r))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away ↑r) :=
  fun r ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away ↑r))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away ↑r) := AlgHom.pi φ
this : IsNoetherian P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away ↑r))
a : P.Fiber S
ha : f a = 0
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : ↑(P.primesOver S) := (PrimeSpectrum.primesOverOrderIsoFiber R S P).symm { asIdeal := J, isPrime := ⋯ }
⊢ (algebraMap (P.Fiber S) (Localization.AtPrime J)) a = 0
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:
rw [coeff_mul]
    refine sum_mem fun ⟨j₁, j₂⟩ hj ↦ ?_
    obtain rfl : j₁ + j₂ = i := by simpa using hj
    exact pow_add I j₁ j₂ ▸ Ideal.mul_mem_mul (hx _) (hy _)

Goal state after:
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
a : R
ha : a ∈ I
⊢ (algebraMap R S) p * l a ∈ R[x]

Tactic:
exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

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 S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
hx0 : x = 0
⊢ x ∈ p

pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
hx0 : ¬x = 0
⊢ x ∈ p

Tactic:
· simp [hx0]

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
hx0 : ¬x = 0
⊢ x ∈ p
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 : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
⊢ IsIntegral R (q.coeff i)

Tactic:
by
  nontriviality S
  obtain ⟨T, _, _, _, _, _, hqT⟩ := hq.exists_splits_map
  algebraize [(algebraMap S T).comp (algebraMap R S)]
  refine (isIntegral_algHom_iff (IsScalarTower.toAlgHom R S T)
    (FaithfulSMul.algebraMap_injective S _)).mp ?_
  rw [IsScalarTower.coe_toAlgHom', ← coeff_map]
  refine Polynomial.isIntegral_coeff_of_factors _ (by simp [hq.map, isIntegral_one]) hqT ?_ i
  intro x hx
  exact ⟨p, hp, by simpa using! aeval_eq_zero_of_dvd_aeval_eq_zero (x := x) H (by simp_all)⟩

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

Goal state before:
pp: case e'_5
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n : Option α →₀ ℕ
⊢ ((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
          (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
      (optionEquivLeft R α).toRingEquiv.toRingHom =
    algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)

Tactic:
ext i m
          · aesop
          · cases i <;> aesop

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

Goal state before:
pp: case h₂
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
f : J.ResidueField →+* RatFunc I.ResidueField := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ })).comp
        (algebraMap R[X] J.ResidueField))
      X =
    ((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)) X

Tactic:
simp [f, RatFunc.liftAlgHom]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
⊢ WeaklyQuasiFiniteAt R q

Tactic:
rw [Algebra.weaklyQuasiFiniteAt_iff]
  let Sq := Localization.AtPrime q
  let := Localization.AtPrime.algebraOfLiesOver p q
  let φ₁ : p.ResidueField →ₐ[R] Sq ⧸ p.map (algebraMap R Sq) :=
    Ideal.quotientMapₐ _ (IsScalarTower.toAlgHom _ _ _) (by
    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, Ideal.map_le_iff_le_comap,
      ← Ideal.comap_coe (F := AlgHom _ _ _), Ideal.comap_comap]
    simpa [← IsScalarTower.algebraMap_eq] using Ideal.le_comap_map)
  let φ₂ : p.Fiber S →ₐ[R] Sq ⧸ p.map (algebraMap R Sq) :=
    Algebra.TensorProduct.lift φ₁ (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _
  let φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ p.map (algebraMap R Sq) :=
    IsLocalization.liftAlgHom (M := Q.primeCompl) (f := φ₂) <| by
      rintro ⟨y, hy⟩
      obtain ⟨r, hrp, s, H⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ y
      suffices IsUnit (φ₂ (1 ⊗ₜ s)) by
        rw [← H, map_smul, Algebra.smul_def, IsUnit.mul_iff] at this
        exact this.2
      suffices s ∉ q by
        have := (IsLocalization.map_units (M := q.primeCompl) Sq ⟨_, this⟩).map
          (algebraMap _ (Sq ⧸ p.map (algebraMap R Sq)))
        simpa [φ₂, ← IsScalarTower.algebraMap_apply] using this
      suffices algebraMap _ _ r * y ∉ Q by simpa [← hQ, ← H, Algebra.smul_def]
      refine Q.primeCompl.mul_mem ?_ hy
      simpa only [Ideal.mem_primeCompl_iff, ← Ideal.mem_comap, ← Q.over_def p]
  have : Function.Surjective φ₃ := by
    intro x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
    refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩
    · simpa [← hQ] using hs
    · simp [φ₃, IsLocalization.lift_mk'_spec, φ₂, IsScalarTower.algebraMap_apply S Sq (Sq ⧸ _),
        -Ideal.Quotient.mk_algebraMap, ← map_mul]
  have inst : QuasiFiniteAt R Q := .trans _ p.ResidueField _
  obtain rfl := q.over_def p
  exact .of_surjective_algHom φ₃ this

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

Goal state before:
pp: X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
⊢ ∃ k hki hkj y, (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x

Tactic:
let a := (pullback.fst _ _ ≫ U.1.ι) x

Goal state after:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
⊢ ∃ k hki hkj y, (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (Spec.map (stalkMap f x))

Tactic:
HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite),

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ QuasiFiniteAt f x ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x y : R⟮X⟯
⊢ (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun (x + y) =
    (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun x +
      (↑(liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun y

Tactic:
simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe]
      cases subsingleton_or_nontrivial R
      · rw [Subsingleton.elim (x + y) y, Subsingleton.elim x 0, map_zero, zero_add]
      obtain ⟨x⟩ := x
      obtain ⟨y⟩ := y
      cases x using Localization.induction_on with | _ pq
      cases y using Localization.induction_on with | _ p'q'
      obtain ⟨p, q⟩ := pq
      obtain ⟨p', q'⟩ := p'q'
      rw [← ofFractionRing_add, Localization.add_mk]
      simp only [RingHom.toMonoidWithZeroHom_eq_coe,
        liftMonoidWithZeroHom_apply_ofFractionRing_mk]
      rw [div_add_div, div_eq_div_iff]
      · rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]
        simp only [map_add, map_mul, Submonoid.coe_mul]
      all_goals
        try simp only [← map_mul, ← Submonoid.coe_mul]
        exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

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

Goal state before:
pp: K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ (algebraMap R K⟮X⟯) x = (algebraMap K[X] K⟮X⟯) ((algebraMap R K[X]) x) / (algebraMap K[X] K⟮X⟯) 1

Tactic:
rw [← mk_eq_div]

Goal state after:
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ (algebraMap R K⟮X⟯) x = RatFunc.mk ((algebraMap R K[X]) x) 1