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

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r

Tactic:
simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
      (TopologicalSpace.Opens.mem_top x)

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

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A Ω[A⁄R]

Tactic:
rw [← PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Module.basicOpen_subset_freeLocus_iff]
    have := IsLocalizedModule.iso (.powers f)
        (KaehlerDifferential.map R R A (Localization.Away f))
    have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
    exact ⟨fun _ ↦ .of_equiv this.symm, fun _ ↦ .of_equiv this⟩

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
have hg₃ : ∀ x y (h : x ∈ K⟮y⟯), g y ⟨x, h⟩ = g x (IntermediateField.AdjoinSimple.gen K x) := by
    intro x y h
    have e : K⟮x⟯ ≤ K⟮y⟯ := by
      rw [IntermediateField.adjoin_le_iff]
      rintro _ rfl
      exact h
    rw [← hg₂ _ ((g _).comp (IntermediateField.inclusion e))]
    · rfl
    apply AlgHom.ext
    rw [← AlgHom.comp_assoc, hg₁, AlgHom.comp_assoc]
    simp

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.smul
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
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * s✝ • n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (s✝ • n✝) +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
rw [mul_comm, smul_mul_assoc, map_smul, mul_comm, e,
            map_smul, smul_add, smul_comm, smul_assoc]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
⊢ FormallySmooth R S

Tactic:
let P' := Localization M'

Goal state after:
R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
⊢ FormallySmooth R S
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.addX (P x / P z) (P x / P z) (-n / P z / d) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3)

Tactic:
simp [field]

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ n * (n + -(P z * d * W.toAffine.a₁)) - P z ^ 2 * d ^ 2 * W.toAffine.a₂ - P z * d ^ 2 * P x - P z * d ^ 2 * P x =
    n * (n - P z * d * W.toAffine.a₁) - P z ^ 2 * d ^ 2 * W.toAffine.a₂ - P z * d ^ 2 * P x * 2
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
I : Ideal R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(map I f)

Tactic:
obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (range f)
  rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
  intro x
  apply AdicCompletion.induction_on I M x (fun a ↦ ?_)
  intro hx
  refine AdicCompletion.mk_zero_of _ _ _ ⟨42, fun n _ ↦ ⟨n + k, by lia, n, by lia, ?_⟩⟩
  rw [← Submodule.comap_map_eq_of_injective hf (I ^ n • ⊤ : Submodule R M),
    Submodule.map_smul'', Submodule.map_top]
  apply (smul_mono_right _ inf_le_right : I ^ n • (I ^ k • ⊤ ⊓ (range f)) ≤ _)
  nth_rw 1 [show n = n + k - k by lia]
  rw [← hk (n + k) (show n + k ≥ k by lia)]
  exact ⟨by simpa using congrArg (fun x ↦ x.val (n + k)) hx, ⟨a (n + k), rfl⟩⟩

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ sum I M ∘ₗ sumInv I M = LinearMap.id

Tactic:
by
  ext f n
  simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq, mk_apply_coe,
    Submodule.mkQ_apply]
  rw [← DirectSum.sum_univ_of (((sumInv I M) ((AdicCompletion.mk I (⨁ (j : ι), M j)) f)))]
  simp only [sumInv_apply, map_mk, map_sum, sum_of, val_sum_apply, mk_apply_coe,
    AdicCauchySequence.map_apply_coe]
  simp only [← Submodule.mkQ_apply, ← map_sum, ← apply_eq_component, lof_eq_of,
    DirectSum.sum_univ_of]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallySmooth R A
I : Ideal S
f : A →ₐ[R] S ⧸ I
⊢ ∃ g, (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp g = f

Tactic:
refine ⟨AdicCompletion.liftAlgHom I (liftAdicCompletionAux I f)
    (factorₐ_comp_liftAdicCompletionAux_of_le I f), ?_⟩
  ext
  simp [liftAdicCompletionAux]

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
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i : σ'
j : σ
⊢ (Q.comp P).jacobiMatrix.toBlocks₁₂ i j = 0 i j

Tactic:
simp [Matrix.toBlocks₁₂, jacobiMatrix_comp_inl_inr]

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

Goal state before:
pp: n m : ℕ
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
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsStandardSmoothOfRelativeDimension n R S
w✝³ w✝² : Type
w✝¹ : Finite w✝²
w✝ : Finite w✝³
P : SubmersivePresentation R S w✝³ w✝²
hP : P.dimension = n
⊢ ∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = n

Tactic:
exact ⟨_, _, _, inferInstance, P.baseChange T, hP⟩

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / P z / d *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3) -
          P x / P z) +
      P y / P z =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Tactic:
simp [field]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.addX (P x / P z) (Q x / Q z) (n / d) =
    (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 - Q x * P z * d ^ 2) *
          d /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Tactic:
simp [field]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / d *
        ((n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                  Q x * P z * d ^ 2) *
                d /
              (P z * Q z) ^ 2 /
            (d ^ 3 / (P z * Q z)) -
          P x / P z) +
      P y / P z =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Tactic:
simp [field]

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')
s t : ↥F.support
h : σ' ↑s = σ' ↑t
i : ι
⊢ (p • σ' ↑s) i = ↑t i

Tactic:
hσ' _ t.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
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')
s t : ↥F.support
h : σ' ↑s = σ' ↑t
i : ι
⊢ (p • σ' ↑s) i = (p • σ' ↑t) i
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
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
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
s : Finset K
hs : (fun t ↦ IsTranscendenceBasis k Subtype.val) ↑s
Hs :
  ∀ ⦃j : Set K⦄,
    (fun t ↦ IsTranscendenceBasis k Subtype.val) j →
      (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j →
        (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s
n : K
hn : ¬IsSeparable (↥(adjoin k ↑s)) n
hns : n ∉ s
i : K
hi₁ : IsTranscendenceBasis k fun j ↦ id ↑j
hi₂ : IsSeparable (↥(adjoin k (insert n ↑s \ {i}))) (id i)
⊢ n ∈ (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) (insert n ↑s \ {i})

Tactic:
· obtain rfl | ne := eq_or_ne n i
    exacts [hi₂, le_restrictScalars_separableClosure _ (subset_adjoin _ _ ⟨.inl rfl, ne⟩)]

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

Goal state before:
pp: R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective ⇑f
⊢ (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) g →
    (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) (g.comp f)

Tactic:
hg

Goal state after:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(g.comp f)
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
⊢ IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g

Tactic:
hg

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)
⊢ IsOpenImmersion g
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 S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
u : T
p : R[X]
hp : (aeval ((algebraMap S T) x)) p * u = 0
⊢ map (algebraMap R T) p * C u = 0

Tactic:
obtain ⟨u, s, rfl⟩ := IsLocalization.exists_mk'_eq M u

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 S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
p : R[X]
u : S
s : ↥M
hp : (aeval ((algebraMap S T) x)) p * IsLocalization.mk' T u s = 0
⊢ map (algebraMap R T) p * C (IsLocalization.mk' T u s) = 0
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 : ∑ i ∈ Finset.range ((minpoly R s).natDegree + 1), (minpoly R s).coeff i • s ^ i = 0
⊢ b • s ^ n ∈ (algebraMap R S).range

Tactic:
Finset.sum_range_succ,

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 :
  ∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x +
      (minpoly R s).coeff (minpoly R s).natDegree • s ^ (minpoly R s).natDegree =
    0
⊢ b • s ^ n ∈ (algebraMap R S).range
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ (q.coeff q.natDegree * (X ^ m) ^ q.natDegree).Monic

Tactic:
by simp [q, minpoly.monic hp, ← pow_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ m * q.natDegree = (q.coeff q.natDegree * (X ^ m) ^ q.natDegree).natDegree

Tactic:
by simp [q, minpoly.monic hp, ← pow_mul]

Goal state after:
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
σ : Type w
hσ : Finite σ
⊢ ∀ {α β : Type w} (a : α ≃ β),
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial β S},
        (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f → ∀ (n : β →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
intro α β e IH f H n

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ IsIntegral R (coeff n f)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_5.hX
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 α →₀ ℕ
i : Option α
m : Option α →₀ ℕ
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X i)) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X i))

Tactic:
· cases i <;> aesop

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ map (algebraMap R P.ResidueField) r * ↑⋯.unit⁻¹ ∈ Ideal.span {map (algebraMap R P.ResidueField) r}

Tactic:
exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _)

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

Goal state before:
pp: case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen f₂ ⊓ X.basicOpen f₃ = toOpens ⟨X.basicOpen f₁, hV⟩

Tactic:
hf₃,

Goal state after:
case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen f₂ ⊓ X.basicOpen f₁ = toOpens ⟨X.basicOpen f₁, hV⟩
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ q)

Tactic:
have hq' : φ q ≠ 0 := nonZeroDivisors.ne_zero (hφ (mem_nonZeroDivisors_iff_ne_zero.mpr hq))
  simp only [← mk_eq_div, mk_eq_localization_mk _ hq, map_apply_ofFractionRing_mk,
    mk_eq_localization_mk _ hq']

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

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.num ∣ p

Tactic:
rintro ⟨q, hq, rfl⟩

Goal state after:
case mpr
K : Type u
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num ∣ p