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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
i : σ
hi : ¬p ∣ n i
⊢ 0 = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

Tactic:
MvPolynomial.coeff_expand_of_not_dvd _ hi

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
i : σ
hi : ¬p ∣ n i
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ (fun x ↦ 0) n ≤ ‖(coeff n) (f + g)‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2

Tactic:
dsimp [Finsupp.prod]

Goal state after:
case refine_1
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ ‖(coeff n) (f + g)‖ * ∏ a ∈ n.support, |c a| ^ n a
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ d i
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
MvPolynomial.coeff_expand_of_not_dvd _ hi

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ d i
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ n.prod fun x1 x2 ↦ |c| x1 ^ x2

Tactic:
dsimp [Finsupp.prod]

Goal state after:
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ ∏ a ∈ n.support, |c a| ^ n a
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✝
k : Type u_3
A : Type u_4
K : Type u_5
inst✝⁶ : Field k
inst✝⁵ : Ring A
inst✝⁴ : Algebra k A
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : Algebra.IsAlgebraic k K
inst✝ : IsGeometricallyReduced k A
⊢ IsReduced (K ⊗[k] A)

Tactic:
have := (isGeometricallyReduced_field_iff k A).mp ‹_›

Goal state after:
k✝ : Type u_1
A✝ : Type u_2
inst✝⁹ : Field k✝
inst✝⁸ : Ring A✝
inst✝⁷ : Algebra k✝ A✝
k : Type u_3
A : Type u_4
K : Type u_5
inst✝⁶ : Field k
inst✝⁵ : Ring A
inst✝⁴ : Algebra k A
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : Algebra.IsAlgebraic k K
inst✝ : IsGeometricallyReduced k A
this : IsReduced (AlgebraicClosure k ⊗[k] A)
⊢ IsReduced (K ⊗[k] A)
Module: Mathlib.RingTheory.Noetherian.Filter

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ EventuallyConst (⇑f) atTop

Tactic:
simp_rw [eventuallyConst_atTop, eq_comm]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers K⟮X⟯ (idealX K)).toSubring
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)

Tactic:
· obtain ⟨F, hF⟩ := exists_powerSeries_of_memIntegers K H
    simp only [Subring.mem_map]
    exact ⟨F, ⟨F, trivial, rfl⟩, hF⟩

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

Goal state before:
pp: case e_a.e_a.e_a
p n k : ℕ
hk : k < n + 1
⊢ 1 + (n - k) = n - k + 1

Tactic:
← add_comm

Goal state after:
case e_a.e_a.e_a
p n k : ℕ
hk : k < n + 1
⊢ n - k + 1 = n - k + 1
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
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) f)).leadingCoeff

Tactic:
have coeff : (finSuccEquiv k n ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
      (finSuccEquiv k n ((T f) (h v))).leadingCoeff := by
    simp only [map_add, map_sum]
    rw [add_comm]
    apply leadingCoeff_add_of_degree_lt <| (lt_of_le_of_lt <| degree_sum_le _ _) ?_
    have h2 : h v ≠ 0 := by simpa [h] using mem_support_iff.mp vin
    replace h2 : (finSuccEquiv k n ((T f) (h v))) ≠ 0 := fun eq ↦ h2 <|
      by simpa only [map_eq_zero_iff _ (AlgEquiv.injective _)] using eq
    exact (Finset.sup_lt_iff <| Ne.bot_lt (fun x ↦ h2 <| degree_eq_bot.mp x)).mpr vs

Goal state after:
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
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) f)).leadingCoeff
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map ((RingHom.id (MvPolynomial (Fin (n + 1)) k)).comp ↑(T f)) I =
    Ideal.map (RingHom.id (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)

Tactic:
simp only [← Ideal.map_map, Ideal.map_coe]

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 w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
this : (T f).symm.toRingEquiv.toRingHom.comp ↑(T f) = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ I = Ideal.map (RingHom.id (MvPolynomial (Fin (n + 1)) k)) I

Tactic:
Ideal.map_id

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
this : (T f).symm.toRingEquiv.toRingHom.comp ↑(T f) = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ I = I
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
n : ℕ
⊢ ((map f) x).coeff n = coeff 0 n

Tactic:
simpa using h n

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ k * p ^ (n - k + 1)

Tactic:
← pow_add,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k + 1))
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + i + (n - i - m)

Tactic:
add_assoc,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + (i + (n - i - m))
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    X n ^ p + (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C ↑p * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
add_assoc,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    X n ^ p + ((∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C ↑p * X (n + 1)) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j ∈ (W_ ℚ k).vars
hx : (i, j) ∈ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1

Tactic:
rw [wittPolynomial_vars, Finset.mem_range] at hj

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = (aeval x✝.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)

Tactic:
aeval_eq_eval₂Hom,

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = (eval₂Hom (algebraMap ℤ R✝) x✝.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| (aeval fun k ↦ x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))

Tactic:
aeval_eq_eval₂Hom,

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
| (eval₂Hom (algebraMap (ZMod p) R) fun k ↦ x.coeff k)
    ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
y0 : P n
⊢ x.coeff n = x.coeff n + y.coeff n

pp: case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
y0 : ¬P n
⊢ y.coeff n = x.coeff n + y.coeff n

Tactic:
· rw [y0, add_zero]

Goal state after:
case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
y0 : ¬P n
⊢ y.coeff n = x.coeff n + y.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), (∀ (n : ℕ), x ≡ 0 [SMOD Ideal.span {↑p} ^ n • ⊤]) → x = 0

Tactic:
intro _ h

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 • ⊤]
⊢ x✝ = 0
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this✝ : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
m : ℕ
hma : (x a).coeff m ≠ 0
hmS' : ∑ s ∈ S', (x s).coeff m ≠ 0
b : α
hb : b ∈ S'
hb' : (x b).coeff m ≠ 0
this : a = b
⊢ False

Tactic:
exact ha (this ▸ hb)

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:
dickson_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
⊢ dickson 2 1 1 = Chebyshev.S R ↑1

Tactic:
dickson_one,

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

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

Tactic:
have h : (1 : R) = Int.castRingHom R 1 := by simp only [eq_intCast, Int.cast_one]

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = (dickson 1 1 m).comp (dickson 1 1 n)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case pn
n : ℕ
⊢ (hermite n).degree ≤ ↑n

Tactic:
simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]
    rintro m hnm
    exact coeff_hermite_of_lt hnm

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

Goal state before:
pp: case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ ↑(n.choose m) * ((-1) ^ m * (X ^ m * X ^ n)) = n.choose m • (-1) ^ m * X ^ (n + m)

pp: case e_a.a.h
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m ≤ n

Tactic:
← pow_add,

Goal state after:
case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ ↑(n.choose m) * ((-1) ^ m * X ^ (m + n)) = n.choose m • (-1) ^ m * X ^ (n + m)

case e_a.a.h
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m ≤ n
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝² : CommRing T
inst✝¹ : Field S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2} ↔
    x1 + x2 = -(algebraMap T S) b / (algebraMap T S) a ∧ x1 * x2 = (algebraMap T S) c / (algebraMap T S) a

Tactic:
rw [aroots_def, show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp]
  exact roots_quadratic_eq_pair_iff_of_ne_zero' ha

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∑ k ∈ range (n + 1), (coeff k) X * (n - k).largeSchroder = (n - 1).largeSchroder

Tactic:
simp only [coeff_X, ite_mul, one_mul, zero_mul, sum_ite_eq', mem_range, lt_add_iff_pos_left,
    ite_eq_left_iff, not_lt, nonpos_iff_eq_zero]

Goal state after:
n : ℕ
hn : 0 < n
⊢ n = 0 → 0 = (n - 1).largeSchroder
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∑ k ∈ range (n + 1), (coeff k) (X * largeSchroderSeries) * (coeff (n - k)) largeSchroderSeries =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
sum_range_succ

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (coeff (n - x)) largeSchroderSeries +
      (coeff n) (X * largeSchroderSeries) * (coeff (n - n)) largeSchroderSeries =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this✝ :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
this :
  (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) =
    ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder
⊢ ∑ k ∈ range (n - 1 + 1 - 1), (1 + k - 1).largeSchroder * (n - 1 + 1 - (1 + k)).largeSchroder +
      (n - 1 + 1 - 1).largeSchroder =
    ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 + 1 - 1 - i).largeSchroder

Tactic:
sum_range_succ

Goal state after:
n : ℕ
hn : 0 < n
this✝ :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
this :
  (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) =
    ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder
⊢ ∑ k ∈ range (n - 1 + 1 - 1), (1 + k - 1).largeSchroder * (n - 1 + 1 - (1 + k)).largeSchroder +
      (n - 1 + 1 - 1).largeSchroder =
    ∑ x ∈ range (n - 1), x.largeSchroder * (n - 1 + 1 - 1 - x).largeSchroder +
      (n - 1).largeSchroder * (n - 1 + 1 - 1 - (n - 1)).largeSchroder
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
f x y : M →ₚₗ[R] N
⊢ (x + y).ground = x.ground + y.ground

Tactic:
ext m; simp [ground]

Goal state after:
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
f : M →ₚₗ[R] N
r : R
x : M →ₚₗ[R] N
⊢ (r • x).ground = (RingHom.id R) r • x.ground

Tactic:
ext m; simp [ground]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
this✝ : IsLocalRing R'
this : IsNoetherianRing R'
⊢ IsRegularLocalRing R'

Tactic:
rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
hb : π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t
⊢ (rTensor P (φ R s).toLinearMap) ((g.comp f).toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor P (φ R s).toLinearMap) (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))

Tactic:
comp_toFun',

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
hb : π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t
⊢ (rTensor P (φ R s).toLinearMap)
      ((g.toFun' (MvPolynomial (Fin s.card) R) ∘ f.toFun' (MvPolynomial (Fin s.card) R)) p) =
    (rTensor P (φ R s).toLinearMap) (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))
Module: Mathlib.RingTheory.Spectrum.Maximal.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | x.asIdeal.IsMaximal}

Tactic:
ext ⟨x, _⟩

Goal state after:
R : Type u
inst✝ : CommRing R
x : Ideal R
isPrime✝ : x.IsPrime
⊢ { asIdeal := x, isPrime := isPrime✝ } ∈ range toPrimeSpectrum ↔
    { asIdeal := x, isPrime := isPrime✝ } ∈ {x | x.asIdeal.IsMaximal}
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ { asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ } ∈ (zeroLocus {f})ᶜ

Tactic:
rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ f ∉ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I ^ 2 = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker

Tactic:
rw [pow_two] at sq

Goal state after:
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case mem_mul_mem
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz : J.toCotangent w = f (J.toCotangent ⟨z, hz⟩)
⊢ f (J.toCotangent ⟨y * z, ⋯⟩) = 0

Tactic:
have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)

Goal state after:
case mem_mul_mem
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz : J.toCotangent w = f (J.toCotangent ⟨z, hz⟩)
mem_bot : y * (Submodule.subtype J) w ∈ I * (I * J)
⊢ f (J.toCotangent ⟨y * z, ⋯⟩) = 0