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

Goal state before:
pp: R : Type u
inst✝¹² : CommRing R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst✝⁹ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁸ : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (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 v'
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (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)
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I)
P : Ideal R
⊢ ∀ (x : P.IsMaximal), Injective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)

Tactic:
hP

Goal state after:
R : Type u
inst✝¹² : CommRing R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst✝⁹ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁸ : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (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 v'
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (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)
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I)
P : Ideal R
hP : P.IsMaximal
⊢ Injective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
⊢ Subsingleton ↑M → Subsingleton (LocalizedModule S ↑M)

Tactic:
intro _

Goal state after:
case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
a✝ : Subsingleton ↑M
⊢ Subsingleton (LocalizedModule S ↑M)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
⊢ Subsingleton ↑M → Subsingleton (LocalizedModule S ↑M)

Tactic:
intro _

Goal state after:
case bot
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
a✝ : Subsingleton ↑M
⊢ Subsingleton (LocalizedModule S ↑M)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
⊢ projectiveDimension M = ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl)

Tactic:
have aux (n : ℕ) : projectiveDimension M ≤ n ↔ ⨆ (p : MaximalSpectrum R), projectiveDimension
    (M.localizedModule p.1.primeCompl) ≤ n := by
    simp only [projectiveDimension_le_iff, iSup_le_iff]
    exact M.hasProjectiveDimensionLE_iff_forall_maximalSpectrum n

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
⊢ projectiveDimension M = ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
⊢ ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}

Tactic:
intro _

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
a✝ : K⸨X⸩
⊢ a✝ ∈ ⋂ n ∈ Set.Iio D, φ n → a✝ ∈ {x | ∀ d < D, coeff hℱ d = x.coeff d}
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := ⋯
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
⊢ ∀ (x : K⸨X⸩), (∀ d < D, coeff hℱ d = x.coeff d) → x ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}

Tactic:
intro _

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
x✝ : K⸨X⸩
⊢ (∀ d < D, coeff hℱ d = x✝.coeff d) → x✝ ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ ∀ {V : Set (K⸨X⸩ × K⸨X⸩)},
    V ∈ uniformity K⸨X⸩ → SetRel.IsSymm V → ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V

Tactic:
intro V hV h_symm

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : V ∈ uniformity K⸨X⸩
h_symm : SetRel.IsSymm V
⊢ ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
⊢ Antitone ⇑(ofLex (supDegree (⇑toLex) p))

Tactic:
by
  obtain rfl | h0 := eq_or_ne p 0
  · rw [supDegree_zero, bot_eq_zero (α := Lex (σ →₀ ℕ))]
    exact Pi.zero_mono
  rw [Antitone]
  by_contra! ⟨i, j, hle, hlt⟩
  apply (le_sup (s := p.support) (f := toLex) _).not_gt
  pick_goal 3
  · rw [← hp (Equiv.swap i j), mem_support_iff, coeff_rename_mapDomain _ (Equiv.injective _)]
    rw [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_toLex] at h0
    assumption
  refine ⟨i, fun k hk ↦ ?_, ?_⟩
  all_goals dsimp only [Pi.toLex_apply, ofLex_toLex]
  · conv_rhs => rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]
    rw [Finsupp.mapDomain_apply (Equiv.injective _), supDegree]; rfl
  · apply hlt.trans_eq
    simp_rw [Finsupp.mapDomain_equiv_apply, Equiv.symm_swap, Equiv.swap_apply_left]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝⁵ : Field k
inst✝⁴ : Ring A
inst✝³ : Algebra k A
B : Type u_3
inst✝² : Ring B
inst✝¹ : Algebra k B
f : A →ₐ[k] B
hf : Function.Injective ⇑f
inst✝ : IsGeometricallyReduced k B
⊢ IsGeometricallyReduced k A

Tactic:
by
  rw [isGeometricallyReduced_field_iff]
  exact isReduced_of_injective (Algebra.TensorProduct.map 1 f)
    (Module.Flat.lTensor_preserves_injective_linearMap _ hf)

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
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.C (MvPolynomial.coeff v f)))).leadingCoeff *
      ∏ i, ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
algHom_C,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
          ((algebraMap k (MvPolynomial (Fin (n + 1)) k)) (MvPolynomial.coeff v f))).leadingCoeff *
      ∏ i, ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.C (MvPolynomial.coeff v f) *
      ∏ x, ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X x))).leadingCoeff ^ v x =
    MvPolynomial.C (MvPolynomial.coeff v f)

Tactic:
have : ∀ j, ((finSuccEquiv k n) ((T1 f) 1 (X j))).leadingCoeff = 1 := fun j ↦ by
      by_cases h : j = 0
      · simp [h, finSuccEquiv_apply]
      · 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:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
this : ∀ (j : Fin (n + 1)), ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1
⊢ MvPolynomial.C (MvPolynomial.coeff v f) *
      ∏ x, ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X x))).leadingCoeff ^ v x =
    MvPolynomial.C (MvPolynomial.coeff v f)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = (expand p) (C (↑p ^ k)) * (X k ^ p) ^ p ^ (n - k)

Tactic:
algHom_C,

Goal state after:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) =
    (algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1))))) (↑p ^ k) * (X k ^ p) ^ p ^ (n - k)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case pos
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : I = 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

pp: case neg
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
· have bij : Function.Bijective (Quotient.mkₐ k I) :=
        (Quotient.mk_bijective_iff_eq_bot I).mpr eqi
      exact ⟨d + 1, le_rfl, _, bij.1, isIntegral_of_surjective _ bij.2⟩

Goal state after:
case neg
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - (bind₁ (W_ R)) (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))) *
      (bind₁ (W_ R)) (C (⅟↑p ^ n)) =
    X n

Tactic:
algHom_C,

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - (bind₁ (W_ R)) (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))) *
      (algebraMap R (MvPolynomial ℕ R)) (⅟↑p ^ n) =
    X n
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) = (bind₁ (W_ R)) (C (↑p ^ i)) * (bind₁ (W_ R)) (xInTermsOfW p R i) ^ p ^ (n - i)

Tactic:
algHom_C,

Goal state after:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ C (↑p ^ i) * X i ^ p ^ (n - i) =
    (algebraMap R (MvPolynomial ℕ R)) (↑p ^ i) * (bind₁ (W_ R)) (xInTermsOfW p R i) ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

pp: case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0

Tactic:
· intro i _hi hi0
    simp only [onePoly, if_neg hi0, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, map_pow,
      bind₁_X_right, map_mul]

Goal state after:
case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
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 ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) =
    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:
rw [← C_eq_coe_nat]

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) * (C ↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) =
    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.Domain

Goal state before:
pp: case succ.h
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
⊢ ∀ i < k + 1, x.coeff i = 0

Tactic:
· exact h

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

Goal state before:
pp: case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung)^[i] x * (⇑verschiebung)^[j] y).coeff (i + j) =
    ((⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j)

Tactic:
iterate_verschiebung_mul

Goal state after:
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j) =
    ((⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂),
    (TruncatedWittVector.truncate hk).comp ((fun k ↦ (truncate k).comp g) k₂) = (fun k ↦ (truncate k).comp g) k₁

Tactic:
intro _

Goal state after:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
k₁✝ : ℕ
⊢ ∀ (k₂ : ℕ) (hk : k₁✝ ≤ k₂),
    (TruncatedWittVector.truncate hk).comp ((fun k ↦ (truncate k).comp g) k₂) = (fun k ↦ (truncate k).comp g) k₁✝
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), (∀ (n : ℕ), x ≡ 0 [SMOD Ideal.span {↑p} ^ n • ⊤]) → x = 0

Tactic:
intro _

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
⊢ (∀ (n : ℕ), x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ n • ⊤]) → x✝ = 0
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
x : R♭
⊢ (fontaineThetaModPPow R p n) ((teichmuller p) x) = (Ideal.Quotient.mk (𝔭 ^ (n + 1))) (untilt x)

Tactic:
by
  simp [fontaineThetaModPPow]

Goal state after:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
x✝¹ : IsHausdorff (Ideal.map (fontaineTheta R p) (span {↑p})) R
x✝ : 𝕎 R♭
⊢ (⇑(Ideal.Quotient.mk 𝔭) ∘ ⇑(fontaineTheta R p)) x✝ = ((fun x ↦ (PreTilt.coeff 0) x) ∘ fun x ↦ x.coeff 0) x✝

Tactic:
simp [mk_fontaineTheta]

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

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

Tactic:
rw [dickson_one, Nat.cast_one, Chebyshev.C_one]

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

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ 0 - (↑(n + k + 1) + 2) * (hermite n).coeff (n + (k + 2) + 1) = 0

Tactic:
ih (k + 2),

Goal state after:
case succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ 0 - (↑(n + k + 1) + 2) * 0 = 0
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
⊢ dickson 1 1 (n * m) = (dickson 1 1 n).comp (dickson 1 1 m)

Tactic:
dickson_one_one_mul

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
⊢ (dickson 1 1 n).comp (dickson 1 1 m) = (dickson 1 1 n).comp (dickson 1 1 m)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ (↑d !)⁻¹ • ((ascPochhammer F d).comp (X - C (↑k - 1))).leadingCoeff = (↑d !)⁻¹

Tactic:
by
    simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
      (monic_ascPochhammer _ _), leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (rTensor N (P₁.subtype ∘ₗ j)) u = (rTensor N (P₁.subtype ∘ₗ j')) u'

Tactic:
rw [hj₁, hj'₁]

Goal state after:
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (rTensor N (A.val.toLinearMap ∘ₗ P.subtype)) u = (rTensor N (A.val.toLinearMap ∘ₗ P'.subtype)) u'
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
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N ((ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)).comp (mkₐ R (RingCon.ker ↑φ))).toLinearMap)
      (f.toFun' A p) =
    (rTensor N (ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp (mkₐ R (RingCon.ker ↑ψ)))).toLinearMap)
      (f.toFun' B q)

Tactic:
simp only [AlgHom.comp_toLinearMap, rTensor_comp_apply]

Goal state after:
R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N ψ.range.val.toLinearMap)
      ((rTensor N (↑(quotientKerEquivRangeₐ ψ)).toLinearMap)
        ((rTensor N θ.toLinearMap) ((rTensor N (mkₐ R (RingCon.ker ↑φ)).toLinearMap) (f.toFun' A p)))) =
    (rTensor N ψ.range.val.toLinearMap)
      ((rTensor N (↑(quotientKerEquivRangeₐ ψ)).toLinearMap)
        ((rTensor N (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) (f.toFun' B q)))
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
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:
simp_rw [Nat.mem_primeFactors, Function.Embedding.toFun_eq_coe, Nat.castEmbedding_apply] at h
    obtain ⟨n, ⟨pn, dn, -⟩, rfl⟩ := h
    rw [Int.natCast_dvd, ← Nat.prime_iff_prime_int]
    exact ⟨pn, by simp, dn⟩

Goal state after: