mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
h₂ : (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P
⊢ ↑s * (x * s') - x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) P)

Tactic:
comap_map_eq_self_of_isMaximal _ IsPrime.ne_top',

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
h₂ : (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P
⊢ ↑s * (x * s') - x ∈ P
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
obtain ⟨f, hf⟩ := forall_mem_nonempty_iff_neBot.mpr hℱ.1 (S ∩ T) (inter_mem_iff.mpr ⟨hS, hT⟩)

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN : ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ S ×ˢ T
⊢ g ∈ {x | (fun f ↦ ∀ n < N, f.coeff n = 0) x}

Tactic:
refine hN g (le_of_lt ?_)

Goal state after:
case h
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN : ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ S ×ˢ T
⊢ Valued.v (g - f) < 1
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ ((if hi : ↑⟨m - 1, ⋯⟩ < m then s ⟨↑⟨m - 1, ⋯⟩, hi⟩ else 0) -
      if hi : ↑⟨m - 1, ⋯⟩ + 1 < m then s ⟨↑⟨m - 1, ⋯⟩ + 1, hi⟩ else 0) =
    s ⟨m - 1, hm⟩

pp: case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ ∀ (j : Fin n), m ≤ ↑j → invAccumulate n m s j = 0

Tactic:
dif_pos hm,

Goal state after:
case refine_2
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ (s ⟨↑⟨m - 1, ⋯⟩, hm⟩ - if hi : ↑⟨m - 1, ⋯⟩ + 1 < m then s ⟨↑⟨m - 1, ⋯⟩ + 1, hi⟩ else 0) = s ⟨m - 1, hm⟩

case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ ∀ (j : Fin n), m ≤ ↑j → invAccumulate n m s j = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : ∃ x ∈ Iic ⟨i, him⟩, x ∉ t
ht' : #t = #(Iic ⟨i, him⟩)
⊢ toLex (Finsupp.indicator t fun x x_1 ↦ 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1)

Tactic:
← mem_sdiff

Goal state after:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
⊢ toLex (Finsupp.indicator t fun x x_1 ↦ 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1)
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:
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.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ antidiagonal k
⊢ ∑ A ∈ powersetCard a.1 univ, ∑ j, weight σ R k (A, j) = (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2

Tactic:
by
  simp only [esymm, psum, weight, ← mul_assoc, mul_sum]
  rw [sum_comm]
  refine sum_congr rfl fun x _ ↦ ?_
  rw [sum_mul]
  refine sum_congr rfl fun s hs ↦ ?_
  rw [mem_powersetCard_univ.mp hs, ← mem_antidiagonal.mp ha, add_sub_self_left]

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 : ¬p ∣ m i
⊢ (coeff m) ((expand p hp) φ) = 0

Tactic:
classical
  contrapose! h
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
  obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
  have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [this, coeff_monomial] at hd
  have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
  simp [meq]

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

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
this : Module R ↑M := Module.compHom (↑M) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : ↑M
⊢ (r • m) • x = ((Matrix.scalar ι) r * m) • x

Tactic:
Matrix.scalar_apply,

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
this : Module R ↑M := Module.compHom (↑M) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : ↑M
⊢ (r • m) • x = ((Matrix.diagonal fun x ↦ r) * m) • x
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
i : σ
hi : m i > n i
⊢ ¬p • m i ≤ p • n i

Tactic:
simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m✝ m : ℕ
ih : (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f
⊢ (coeffMonoidHom M p (n + m.succ)) ((⇑(powMonoidHom p))^[m.succ] f) = (coeffMonoidHom M p n) f

Tactic:
by
    rw [Function.iterate_succ_apply', Nat.add_succ, coeffMonoidHom_powMonoidHom, ih]

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

Goal state before:
pp: case succ
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 : ℕ
⊢ (x * (↑n + ↑1)).coeff k = (aeval x.coeff) ((fun k ↦ (bind₁ (Function.uncurry ![wittMulN p n, X])) (wittAdd p k)) k)

Tactic:
Nat.cast_one,

Goal state after:
case succ
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 : ℕ
⊢ (x * (↑n + 1)).coeff k = (aeval x.coeff) ((fun k ↦ (bind₁ (Function.uncurry ![wittMulN p n, X])) (wittAdd p k)) k)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ C (↑p ^ i) *
          (∑ k ∈ range (p ^ (n - i)),
              (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
                  (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
                ↑((p ^ (n - i)).choose (k + 1)) +
            (X i ^ p) ^ p ^ (n - i) * ↑1) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))

Tactic:
Nat.cast_one,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ C (↑p ^ i) *
          (∑ k ∈ range (p ^ (n - i)),
              (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
                  (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
                ↑((p ^ (n - i)).choose (k + 1)) +
            (X i ^ p) ^ p ^ (n - i) * 1) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ (x * ↑p ^ n * ↑p).coeff (m' + 1) = 0

Tactic:
rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
      simpa using h

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * C ↑p ^ (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1)) *
        C ↑p ^ i *
      C ⅟↑p ^ n =
    (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) *
      C ↑p

Tactic:
simp only [mul_assoc]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
      ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        (C ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)))) =
    (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
      ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        (C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) *
          C ↑p))
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (select P x).coeff n = (aeval x.coeff) (selectPoly P n)

Tactic:
dsimp [select, selectPoly]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (if P n then x.coeff n else 0) = (aeval x.coeff) (if P n then X n else 0)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2
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
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ (coeff (max m n + 1)) g ^ p ≠ 0

Tactic:
rw [coeff_pow_p g]; assumption

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ X = Chebyshev.C R ↑1

Tactic:
Nat.cast_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ X = Chebyshev.C R 1
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ X = Chebyshev.S R ↑1

Tactic:
Nat.cast_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ X = Chebyshev.S R 1
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
⊢ (hermite (n + 1)).coeff (k + 1) = (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)

Tactic:
rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]
  norm_cast

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ ∃ K x, ∃ (_ : CharP K p), Infinite K

Tactic:
refine ⟨K, ?_, ?_, ?_⟩

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ Field K

case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ CharP K p

case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ Infinite K
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}.Infinite

Tactic:
apply @Set.Infinite.mono _ { x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0 }

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0} ⊆ {x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}

case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Infinite
Module: Mathlib.RingTheory.Polynomial.Opposites

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

Tactic:
simp_rw [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff]

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ (IsLeftCancelMulZero R ∧ IsCancelAdd R) ∧ IsRightCancelMulZero R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr.refine_1
z : ℤ
hz : z ≠ 0
p : ℤ
x✝ : Prime p ∧ 0 ≤ p ∧ p ∣ z
pp : Prime p
nnp : 0 ≤ p
dp : p ∣ z
⊢ ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = p

pp: case inr.refine_2
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z

Tactic:
· lift p to ℕ using nnp
    rw [← Nat.prime_iff_prime_int] at pp
    rw [Int.natCast_dvd] at dp
    exact ⟨p, by simp_all, rfl⟩

Goal state after:
case inr.refine_2
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module S N
inst✝⁵ : IsScalarTower R S N
p : Ideal R
inst✝⁴ : p.IsPrime
inst✝³ : IsLocalization.AtPrime S p
inst✝² : Nontrivial N
inst✝¹ : Module.Finite S N
f : M →ₗ[R] N
inst✝ : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
⊢ IsRegular N (List.map (⇑(algebraMap R S)) rs)

Tactic:
refine (IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal (fun _ hr ↦ ?_)).mpr <|
    reg.of_isLocalizedModule S p.primeCompl f

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module S N
inst✝⁵ : IsScalarTower R S N
p : Ideal R
inst✝⁴ : p.IsPrime
inst✝³ : IsLocalization.AtPrime S p
inst✝² : Nontrivial N
inst✝¹ : Module.Finite S N
f : M →ₗ[R] N
inst✝ : IsLocalizedModule.AtPrime p f
rs : List R
reg : IsWeaklyRegular M rs
mem : ∀ r ∈ rs, r ∈ p
this : IsLocalRing S
x✝ : S
hr : x✝ ∈ List.map (⇑(algebraMap R S)) rs
⊢ x✝ ∈ IsLocalRing.maximalIdeal S
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := ⋯
s : A⟦X⟧ := ⋯
n : ℕ := ⋯
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := ⋯
s₁ : A⟦X⟧ := ⋯
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := ⋯
⊢ s + g * (q - q') = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹

Tactic:
q'

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ s + g * (q - (q + s₁ * ↑⋯.unit⁻¹)) = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = g * q' + ↑r' - ↑r
⊢ g * (q - q') = ↑(r' - r)

Tactic:
rw [Polynomial.coe_sub, mul_sub, heq]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = g * q' + ↑r' - ↑r
⊢ g * q' + ↑r' - ↑r - g * q' = ↑r' - ↑r
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + (↑n + ↑1)

Tactic:
Nat.cast_one,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + (↑n + 1)
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q : PrimeSpectrum S
⊢ ∀ ⦃a₂ : PrimeSpectrum S⦄, comap f q = comap f a₂ → q = a₂

Tactic:
q'

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
⊢ comap f q = comap f q' → q = q'
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : ↑p = C ↑p
⊢ (C ↑p).vars ⊆ univ ×ˢ range n

Tactic:
vars_C

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : ↑p = C ↑p
⊢ ∅ ⊆ univ ×ˢ range n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n

Tactic:
enter [1, 2, 2]

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]

Tactic:
let f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k := by
    intro x y
    apply f₀
    rintro ⟨a, ha⟩
    apply Function.uncurry ![x, y]
    let S : Set (Fin 2 × ℕ) := { a | a.2 = n ∨ a.2 < n }
    have ha' : a ∈ S := by grind
    refine ⟨a.fst, ⟨a.snd, ?_⟩⟩
    obtain ⟨ha, ha⟩ := ha' <;> lia

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]