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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
⊢ (hasseDeriv R k) ((hasseDeriv R l) f) = (k + l).choose k • (hasseDeriv R (k + l)) f

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
⊢ (⇑(derivative R))^[k] f = k.factorial • (hasseDeriv R k) f

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart = x

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart).coeff n = x.coeff n
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

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
inst✝¹¹ : p.IsPrime
Rₚ : Type u_3
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization.AtPrime Rₚ p
inst✝⁷ : IsLocalRing Rₚ
T : Type u_5
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra Rₚ T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsScalarTower R Rₚ T
Q : Ideal T
inst✝ : Q.LiesOver (maximalIdeal Rₚ)
⊢ (comap (algebraMap S T) Q).LiesOver p

Tactic:
by
  have : Q.LiesOver p := by
    have : (maximalIdeal Rₚ).LiesOver p := liesOver_maximalIdeal Rₚ p _
    exact LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p
  exact comap_liesOver Q p <| IsScalarTower.toAlgHom R S T

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

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
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
⊢ (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)

Tactic:
rw [liesOver_iff, eq_comm, ← map_eq_maximalIdeal p, over_def P p]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
⊢ under Rₚ (Ideal.map (algebraMap S Sₚ) P) = Ideal.map (algebraMap R Rₚ) (under R P)
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

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
inst✝¹⁴ : p.IsPrime
Rₚ : Type u_3
inst✝¹³ : CommRing Rₚ
inst✝¹² : Algebra R Rₚ
inst✝¹¹ : IsLocalization.AtPrime Rₚ p
inst✝¹⁰ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra S Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝⁵ : Algebra R Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
inst✝² : p.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
x : Rₚ
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((equivQuotMaximalIdeal p Rₚ).symm ((Ideal.Quotient.mk (maximalIdeal Rₚ)) x)) =
    (equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P))
        ((Ideal.Quotient.mk (maximalIdeal Rₚ)) x))

Tactic:
obtain ⟨x, s, rfl⟩ := mk'_surjective p.primeCompl x

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
p : Ideal R
inst✝¹⁴ : p.IsPrime
Rₚ : Type u_3
inst✝¹³ : CommRing Rₚ
inst✝¹² : Algebra R Rₚ
inst✝¹¹ : IsLocalization.AtPrime Rₚ p
inst✝¹⁰ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra S Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝⁵ : Algebra R Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
inst✝² : p.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
x : R × ↥p.primeCompl
⊢ (algebraMap (R ⧸ p) (S ⧸ P))
      ((equivQuotMaximalIdeal p Rₚ).symm
        ((Ideal.Quotient.mk (maximalIdeal Rₚ))
          ((fun x ↦
              match x with
              | (r, m) => mk' Rₚ r m)
            x))) =
    (equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P))
        ((Ideal.Quotient.mk (maximalIdeal Rₚ))
          ((fun x ↦
              match x with
              | (r, m) => mk' Rₚ r m)
            x)))
Module: Mathlib.RingTheory.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
n : ℕ
⊢ (map (iterateFrobenius R p n)) ((expand (p ^ n)) f) = f ^ p ^ n

Tactic:
induction n with

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
q : ℕ
hq : q ≠ 0
⊢ expand (p * q) ⋯ = (expand p hp).comp (expand q hq)

Tactic:
by
  ext1 i
  simp [expand, pow_mul, subst_comp_subst_apply (HasSubst.X_pow hq) (HasSubst.X_pow hp),
    subst_pow (HasSubst.X_pow hp), subst_X (HasSubst.X_pow hp)]

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 : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
⊢ (↑(DistribSMul.toAddMonoidHom M (single i i 1))).toFun (r • x) =
    (RingHom.id R) r • (↑(DistribSMul.toAddMonoidHom M (single i i 1))).toFun x

Tactic:
by
        dsimp
        have : Commute (diagonal fun x : ι ↦ r) (single i i 1) := by
          ext; simp [Matrix.single]
        rw [← smul_assoc r, smul_eq_diagonal_mul, this.eq, mul_smul, ← smul_one_eq_diagonal]
        nth_rw 1 [← one_smul (Matrix ι ι R) x]
        rw [smul_assoc]

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 : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module (Matrix ι ι R) M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R (Matrix ι ι R) M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module (Matrix ι ι R) N
i : ι
inst✝¹ : Module R N
inst✝ : IsScalarTower R (Matrix ι ι R) N
f : M →ₗ[Matrix ι ι R] N
y : M
hx : single i i 1 • y ∈ toModuleCatObj R M i
⊢ (↑R f) (single i i 1 • y) ∈ toModuleCatObj R N i

Tactic:
exact ⟨f y, map_smul _ _ _ |>.symm⟩

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ p • φ.order ≤ ((expand p hp) φ).order

Tactic:
refine MvPowerSeries.le_order fun d hd => ?_
      by_cases! h : ∀ i, p ∣ d i
      · obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
          by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
        rw [← hm, coeff_expand_smul, coeff_of_lt_order]
        simp only [← hm, map_nsmul, smul_eq_mul, Nat.cast_mul, nsmul_eq_mul] at hd
        exact lt_of_mul_lt_mul_left' hd
      · obtain ⟨i, hi⟩ := h
        exact coeff_expand_of_not_dvd p hp φ hi

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
φ : MvPolynomial σ R
⊢ (expand p hp) ↑φ = ↑((MvPolynomial.expand p) φ)

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ (coeff n) ((expand p hp) ↑φ) = (coeff n) ↑((MvPolynomial.expand p) φ)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : ℕ
⊢ (map (iterateFrobenius R p n)) ((expand (p ^ n) ⋯) f) = f ^ p ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case neg
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1

Tactic:
· simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]
        obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h
        simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ Quotient.out ((coeff (R ⧸ I) p (m + 1)) x) ^ p ≡ Quotient.out ((coeff (R ⧸ I) p m) x) [SMOD I]

Tactic:
by
    simp [SModEq.idealQuotientMk, coeff_pow_p']

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin n) k)
hi : I ≠ ⊤
⊢ ∃ s ≤ n, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
induction n with

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

Goal state before:
pp: p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Surjective f
x : 𝕎 β
⊢ mapFun f (mk p fun n ↦ Classical.choose ⋯) = x

Tactic:
ext n

Goal state after:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Surjective f
x : 𝕎 β
n : ℕ
⊢ (mapFun f (mk p fun n ↦ Classical.choose ⋯)).coeff n = x.coeff n
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : ℕ
⊢ i.unaryCast.ghostFun = ↑i

Tactic:
induction i <;> simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add]

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : 𝕎 R
⊢ (fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x.ghostFun = x

Tactic:
ext n

Goal state after:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x.ghostFun).coeff n = x.coeff n
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : ℕ → R
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x).ghostFun = x

Tactic:
ext n

Goal state after:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x).ghostFun n = x n
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case refine_2
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), f (x.coeff n) = 0
⊢ (map f) x = 0

Tactic:
ext n

Goal state after:
case refine_2
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), f (x.coeff n) = 0
n : ℕ
⊢ ((map f) x).coeff n = coeff 0 n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ (coeffMonoidHom M p n) ((powMulEquiv (Perfection M p) p).symm f) = (coeffMonoidHom M p (n + 1)) f

Tactic:
← coe_pthRootMonoidHom_eq_powMulEquiv_symm

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ (coeffMonoidHom M p n) ((pthRootMonoidHom M p) f) = (coeffMonoidHom M p (n + 1)) f
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ f x✝ = g x✝

Tactic:
ext n

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ (f x✝).coeff n = (g x✝).coeff n
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
⊢ w = 0

Tactic:
ext n

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ w.coeff n = coeff 0 n
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n k : ℕ
⊢ (bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k

Tactic:
induction n with

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

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
⊢ (WittVector.map g) (f x) = f ((WittVector.map g) x)

Tactic:
ext n

Goal state after:
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
g : R →+* S
x : 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
n : ℕ
⊢ ((WittVector.map g) (f x)).coeff n = (f ((WittVector.map g) x)).coeff n
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ f x✝ y✝ = g x✝ y✝

Tactic:
ext n

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ (f x✝ y✝).coeff n = (g x✝ y✝).coeff n
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)
⊢ C ↑p ^ i *
        (C ↑p ^ (j + 1) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1))) *
      C ⅟↑p ^ n =
    C ↑p *
      ((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)))))

Tactic:
mul_comm (C (p : ℚ) ^ i),

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)
⊢ C ↑p ^ (j + 1) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1)) *
        C ↑p ^ i *
      C ⅟↑p ^ n =
    C ↑p *
      ((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)))))
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n k : ℕ
⊢ ((⇑verschiebung)^[n] x).coeff (k + n) = x.coeff k

Tactic:
induction n with

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

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

Tactic:
induction n with

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n

Tactic:
induction n with

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

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
⊢ (WittVector.map g) (f x y) = f ((WittVector.map g) x) ((WittVector.map g) y)

Tactic:
ext n

Goal state after:
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
n : ℕ
⊢ ((WittVector.map g) (f x y)).coeff n = (f ((WittVector.map g) x) ((WittVector.map g) y)).coeff n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case inr.inr
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
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
have hfg : coeff (max m n + 1) (f * g) ≠ 0 := by
    rw [map_mul]
    refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_
    · rw [coeff_pow_p f]; assumption
    · rw [coeff_pow_p g]; assumption

Goal state after:
case inr.inr
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
hfg : (coeff (max m n + 1)) (f * g) ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ (map f) (teichmullerFun p r) = teichmullerFun p (f r)

Tactic:
ext n

Goal state after:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ ((map f) (teichmullerFun p r)).coeff n = (teichmullerFun p (f r)).coeff n
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x✝ : 𝕎 k
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ n • ⊤]
⊢ x✝ = 0

Tactic:
ext n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x✝ : 𝕎 k
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ n • ⊤]
n : ℕ
⊢ x✝.coeff n = coeff 0 n
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ hermite n = (fun p ↦ X * p - derivative p)^[n] 1

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ (hermite n).coeff n = 1

Tactic:
induction n with

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

Goal state before:
pp: 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)}

Tactic:
rintro _ ⟨x, rfl, hx⟩

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
x : K
hx : x ≠ 0
⊢ x + x⁻¹ ∈ {x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
this : ∀ (a b : R[X]), f = a * b → IsUnit (Polynomial.map ι b) → IsUnit a ∨ IsUnit b
hb : ¬IsUnit (Polynomial.map ι b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
exact (this b a (mul_comm a b ▸ h)
      (hi.2 (by rw [h, Polynomial.map_mul]) |>.resolve_right hb)).symm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case inl
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

pp: case inr
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
· rw [Nat.even_add, ← Nat.even_sub h_le] at hnk
    obtain ⟨m, hm⟩ := hnk
    rw [(by lia : n = 2 * m + k),
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]

Goal state after:
case inr
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)
Module: Mathlib.RingTheory.PowerSeries.Catalan

Goal state before:
pp: ⊢ catalanSeries ^ 2 * X + 1 = catalanSeries

Tactic:
ext n

Goal state after:
n : ℕ
⊢ (coeff n) (catalanSeries ^ 2 * X + 1) = (coeff n) catalanSeries