mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: case h_option
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
ι : Type u_2
inst✝¹ : Finite ι
α✝ : Type u_2
inst✝ : Fintype α✝
IH : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Nat.card α✝)
⊢ ringKrullDim (MvPolynomial (Option α✝) R) = ringKrullDim R + ↑(Nat.card (Option α✝))

Tactic:
| h_option IH =>

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ J' ∈ {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}

Tactic:
simp [hJ']

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalIso R S
hne : ¬Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} = ⊤
m : Ideal S
hm : m.IsMaximal
hms : Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} ≤ m
⊢ False

Tactic:
obtain ⟨g, hgm, hstd⟩ :=
    Algebra.IsLocalIso.exists_notMem_isStandardOpenImmersion (R := R) m

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalIso R S
hne : ¬Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} = ⊤
m : Ideal S
hm : m.IsMaximal
hms : Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} ≤ m
g : S
hgm : g ∉ m
hstd : IsStandardOpenImmersion R (Localization.Away g)
⊢ False
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
⊢ Submodule.localized' (Rₚ P) P.primeCompl (f P)
      (Submodule.span R ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))) =
    ⊤

Tactic:
rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]

Goal state after:
case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
⊢ ↑(s { asIdeal := P, isMaximal := hP }) ⊆
    ↑(Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))))
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
⊢ (aeval ((residue S) β)) (derivative (minpoly (ResidueField R) ((residue S) β))) ≠ 0

Tactic:
exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors =
    (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors

Tactic:
rw [Ideal.count_associates_factors_eq span_ne_zero.1
    (Ideal.span_singleton_prime Polynomial.X_ne_zero |>.mpr prime_X) span_ne_zero.2,
    Ideal.count_associates_factors_eq]
  on_goal 1 => convert! (normalized_count_X_eq_of_coe hP).symm
  exacts [Ideal.count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X,
    Ideal.count_span_normalizedFactors_eq_of_normUnit (by simp [hP]) normUnit_X X_prime,
    span_ne_zero'.1, (idealX K).isPrime, span_ne_zero'.2]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case h
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ⟨i, hin⟩ ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}

pp: case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∀ b ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}, b ≠ ⟨i, hin⟩ → t b = 0

Tactic:
· rw [mem_filter]; exact ⟨mem_univ _, le_rfl⟩

Goal state after:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∀ b ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}, b ≠ ⟨i, hin⟩ → t b = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((ofPowerSeries ℤ K) (F - ↑((trunc (d + 1)) F))) ≤ ↑(Multiplicative.ofAdd (-(↑d + 1)))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η

Tactic:
neg_add,

Goal state after:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((ofPowerSeries ℤ K) (F - ↑((trunc (d + 1)) F))) ≤ ↑(Multiplicative.ofAdd (-↑d + -1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mp
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
⊢ (∃ t,
      (∃ t_1 ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ S) →
    ∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
rintro ⟨T, ⟨⟨R, ⟨hR, pre_R⟩⟩, pre_T⟩⟩

Goal state after:
case mp
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
⊢ ∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ t ∈ pairs σ k with #t.1 < k, f t = ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)

Tactic:
by
  rw [filter_pairs_lt, sum_product, sum_disjiUnion]
  refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_ <;>
    simp +contextual [@eq_comm _ _ k, le_of_lt]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : 0 ≠ 0
hc : ∀ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) = 0
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
d : σ →₀ ℕ
hd : 0 ≠ 0
this : (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
hc : ¬m = p • d
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : φ n ≠ 0
hn₂ : (fun x ↦ p • x) n = d
hc : (expand p hp) φ (p • n) = 0
⊢ False

Tactic:
← coeff_apply φ,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : (coeff n) φ ≠ 0
hn₂ : (fun x ↦ p • x) n = d
hc : (expand p hp) φ (p • n) = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : 0 ≠ 0
hn₂ : (fun x ↦ p • x) n = d
hc : (expand p hp) φ (p • n) = 0
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: case e_a
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
⊢ (if j = i1 then x i j1 else 0) = ∑ c, if j = i1 ∧ c = j1 then x i c else 0

Tactic:
split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
h2 : (MvPolynomial.finSuccEquiv k n) ((T f) (h v)) ≠ 0
⊢ ((f.support \ {v}).sup fun b ↦ ((MvPolynomial.finSuccEquiv k n) ((T f) (h b))).degree) <
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree

Tactic:
exact (Finset.sup_lt_iff <| Ne.bot_lt (fun x ↦ h2 <| degree_eq_bot.mp x)).mpr vs

Goal state after:
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittSub p 0 = X (0, 0) - X (1, 0)

Tactic:
by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittSub, wittStructureRat, map_sub, rename_X, xInTermsOfW_zero, map_X,
    wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case «0»
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i ↦ i) ⟨0, ⋯⟩, i))

Tactic:
simp [Function.uncurry, Matrix.cons_val_zero, ih]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
h : x ≠ 0
⊢ preVal K v O p x ≠ 0

Tactic:
exact ((v_p_lt_preVal hv).2 h).ne_zero

Goal state after:
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m : ℕ
h : m < 0
⊢ (x * ↑p ^ 0).coeff m = 0

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ (verschiebung (frobenius x)).coeff (n✝ + 1) = (x * ↑p).coeff (n✝ + 1)

Tactic:
· rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
m : ℕ
h : m < 0
⊢ ((⇑verschiebung)^[0] x).coeff m = 0

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
ih : (∀ i < k, x.coeff i = 0) → x = (⇑verschiebung)^[k] (x.shift k)
h : ∀ i < k + 1, x.coeff i = 0
⊢ x = (⇑verschiebung)^[k + 1] (x.shift (k + 1))

Tactic:
dsimp; rw [verschiebung_shift]
    · exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))
    · exact h

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

Tactic:
obtain rfl | hf := eq_or_ne f 0
  · simp
  obtain rfl | hg := eq_or_ne g 0
  · simp
  by_cases hfg : f + g = 0
  · simp [hfg]
  replace hf : ∃ n, coeff n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
  replace hg : ∃ n, coeff n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
  replace hfg : ∃ n, coeff n (f + g) ≠ 0 := not_forall.1 fun h => hfg <| Perfection.ext h
  obtain ⟨m, hm⟩ := hf; obtain ⟨n, hn⟩ := hg; obtain ⟨k, hk⟩ := hfg
  replace hm := coeff_ne_zero_of_le hm (le_trans (le_max_left m n) (le_max_left _ k))
  replace hn := coeff_ne_zero_of_le hn (le_trans (le_max_right m n) (le_max_left _ k))
  replace hk := coeff_ne_zero_of_le hk (le_max_right (max m n) k)
  rw [valAux_eq hv hm, valAux_eq hv hn, valAux_eq hv hk, map_add]
  rcases le_max_iff.1
      (ModP.preVal_add hv (coeff (max (max m n) k) f)
      (coeff (max (max m n) k) g)) with h | h
  · exact le_max_of_le_left (pow_le_pow_left' h _)
  · exact le_max_of_le_right (pow_le_pow_left' h _)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ dickson 1 1 (n + 2) = Chebyshev.C R ↑(n + 2)

Tactic:
rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.C_add_two,
      dickson_one_one_eq_chebyshev_C (n + 1), dickson_one_one_eq_chebyshev_C n]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.C R ↑(n + 1) - 1 * Chebyshev.C R ↑n = X * Chebyshev.C R (↑n + 1) - Chebyshev.C R ↑n
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
⊢ (a • p).hilbertPoly d = a • p.hilbertPoly d

Tactic:
delta hilbertPoly
  induction d with
  | zero => simp only [smul_zero]
  | succ d _ =>
      simp only
      rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
        sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]
      simp only [smul_assoc]

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

Goal state before:
pp: case succ.refine_3
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((d + n - x).choose d) = p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))

Tactic:
Nat.add_sub_assoc (h_le ⟨x, hx⟩),

Goal state after:
case succ.refine_3
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((d + (n - ↑⟨x, hx⟩)).choose d) = p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsCancelMulZero R[X] ↔ IsCancelMulZero R ∧ IsCancelAdd R

Tactic:
isCancelMulZero_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ IsLeftCancelMulZero R[X] ∧ IsRightCancelMulZero R[X] ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = ↑(n ! * ((x + n)! / (x ! * n !)))

Tactic:
← Nat.mul_div_assoc

Goal state after:
case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = ↑(n ! * (x + n)! / (x ! * n !))

case a.e_a.H
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ x ! * n ! ∣ (x + n)!
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this : C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2)
h1 : C a * (X - C x1) ≠ 0
h2 : C a * (X - C x1) * (X - C x2) ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}

Tactic:
simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]

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

Goal state before:
pp: case refine_2
n : ℕ
⊢ (shiftedLegendre n).coeff n ≠ 0

Tactic:
· simp [coeff_shiftedLegendre, (choose_pos (show n ≤ n + n by simp)).ne']

Goal state after:
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
⊢ Free R M

Tactic:
let b := Module.Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
⊢ Free R M
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
⊢ Function.Injective ⇑g

Tactic:
← LinearMap.ker_eq_bot

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
⊢ g.ker = ⊥
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
⊢ ∃ A, ∃ (_ : A.FG), ∃ u, (LinearMap.baseChange (↥A) f) u = 0 ∧ (rTensor M A.val.toLinearMap) u = t

Tactic:
have := TensorProduct.Algebra.eq_of_fg_of_subtype_eq hA (t := f.baseChange _ u) (t' := 0)

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = (rTensor N A.val.toLinearMap) 0 →
    ∃ B,
      ∃ (hAB : A ≤ B),
        B.FG ∧
          (rTensor N (Subalgebra.inclusion hAB).toLinearMap) ((LinearMap.baseChange (↥A) f) u) =
            (rTensor N (Subalgebra.inclusion hAB).toLinearMap) 0
⊢ ∃ A, ∃ (_ : A.FG), ∃ u, (LinearMap.baseChange (↥A) f) u = 0 ∧ (rTensor M A.val.toLinearMap) u = t
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ ∃ a, π R M S a = t

Tactic:
obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ (rTensor M B.val.toLinearMap).range
⊢ ∃ a, π R M S a = t