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

Goal state before:
pp: case refine_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
r : ↥Z
x✝ : r • x ∈ ⊤
s : ↥Z
⊢ (s * r) • (x * x) = (r * s) • (x * x)

Tactic:
mul_comm

Goal state after:
case refine_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
r : ↥Z
x✝ : r • x ∈ ⊤
s : ↥Z
⊢ (r * s) • (x * x) = (r * s) • (x * x)
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
this : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
⊢ ((Finset.filter (Membership.mem s) t).inf fun a ↦ a) = ⨅ q ∈ s, q

Tactic:
Finset.filter_mem_eq_inter,

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
this : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
⊢ ((t ∩ s).inf fun a ↦ a) = ⨅ q ∈ s, q
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N

Tactic:
rcases h with ⟨-, h⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (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
inst✝ : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing (Rₚ P)
this✝ : IsNoetherianRing R
P : Ideal R
hP : P.IsMaximal
this : IsDomain (Rₚ P)
⊢ IsIntegrallyClosed (Rₚ P)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u
inst✝¹⁰ : Group G
inst✝⁹ : MulSemiringAction G B
inst✝⁸ : SMulCommClass G A B
P✝ : Ideal A
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝ : Q.LiesOver P
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
⊢ Finite
    { σ' //
      { toRingHom := Ideal.quotientMap Q ↑(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).val ⋯, commutes' := ⋯ }.comp
          ↑((stabilizerHom (Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
              σ') =
        (↑σ).comp
          { toRingHom := Ideal.quotientMap Q ↑(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).val ⋯, commutes' := ⋯ } }

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
D : WithZero (Multiplicative ℤ)
hD : D ≠ 0
f : K⸨X⸩
⊢ Valued.v f ≤ D ↔ ∀ n < -D.log, f.coeff n = 0

Tactic:
by
  cases D
  · simp_all
  · rename_i D
    cases D
    rename_i D
    rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ∀ (x : ℕ), ¬False

Tactic:
intro

Goal state after:
case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n x✝ : ℕ
⊢ ¬False
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ∀ (x : ℕ), ¬↑x = n✝

Tactic:
intro

Goal state after:
case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
x✝ : ℕ
⊢ ¬↑x✝ = n✝
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_1.e_a.h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : (m.sum fun i c ↦ c • w i) = n
⊢ ∀ (i : σ), 0 • w i = 0

Tactic:
intro

Goal state after:
case refine_1.e_a.h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : (m.sum fun i c ↦ c • w i) = n
i✝ : σ
⊢ 0 • w i✝ = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_2
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x✝ : K⸨X⸩ × K⸨X⸩
hP : x✝ ∈ {P | Valued.v (P.2 - P.1) < ↑γ}
⊢ (x✝.1.coeff d, x✝.2.coeff d) ∈ S

Tactic:
· simpa [eq_coeff_of_valuation_sub_lt K hP.le (lt_add_one _)] using mem_uniformity_of_eq hS rfl

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R), p = a * b → a.totalDegree ≤ b.totalDegree → IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ a * b = b * a

Tactic:
mul_comm

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R), p = a * b → a.totalDegree ≤ b.totalDegree → IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ b * a = b * a
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 : ¬Iic ⟨i, him⟩ ⊆ 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:
not_subset

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
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)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (if j ≤ ⟨↑i, him⟩ then 1 else 0) = if ↑j ≤ ↑i then 1 else 0

Tactic:
Fin.le_def

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

Goal state before:
pp: case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #t.1 + 1 ≤ k

Tactic:
exact (le_iff_eq_or_lt.mp h.left).resolve_left h.right

Goal state after:
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 : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
n : ℕ
⊢ -1 * (-1) ^ n = (-1) ^ n * -1

Tactic:
mul_comm

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
n : ℕ
⊢ (-1) ^ n * -1 = (-1) ^ n * -1
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a✝ : Finset σ × σ
⊢ a✝ ∈
      {x ∈ pairs σ k |
        match x with
        | (s, snd) => #s < k} ↔
    a✝ ∈ (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯ ×ˢ univ

Tactic:
aesop (add unsafe le_of_lt)

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:
isGeometricallyReduced_field_iff

Goal state after:
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
⊢ IsReduced (AlgebraicClosure k ⊗[k] 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
h : ∀ (B : Subalgebra k A), B.FG → IsGeometricallyReduced k ↥B
⊢ IsGeometricallyReduced k A

Tactic:
isGeometricallyReduced_field_iff

Goal state after:
k : Type u_1
A : Type u_2
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
h : ∀ (B : Subalgebra k A), B.FG → IsReduced (AlgebraicClosure k ⊗[k] ↥B)
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩

Goal state after:
case refine_1
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
x✝ : x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
f : K⸨X⸩
F : K⟦X⟧
left✝ : F ∈ ⊤.carrier
coe_F : (ofPowerSeries ℤ K) F = f
hF : (LaurentSeriesRingEquiv K).toRingHom f = x
⊢ x ∈ (adicCompletionIntegers K⟮X⟯ (idealX K)).toSubring

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)
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) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
i : Fin n
x✝ : i ∈ Finset.univ
⊢ v i.succ * up ^ ↑i.succ = up ^ ↑i.succ * v i.succ

Tactic:
mul_comm

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
i : Fin n
x✝ : i ∈ Finset.univ
⊢ up ^ ↑i.succ * v i.succ = up ^ ↑i.succ * v i.succ
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 ^ (n - k))

Tactic:
rw [map_mul (expand p), map_pow (expand p), expand_X, algHom_C, ← pow_mul, ← pow_succ']

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 ^ (n - k + 1)
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
this : (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)
⊢ ↑p ^ (n - i + 1) * ↑p ^ i ∣ ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
mul_comm

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
this : (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)
⊢ ↑p ^ i * ↑p ^ (n - i + 1) ∣ ↑p ^ i * x.coeff i ^ p ^ (n - i)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Perfection R p
n : ℕ
hfn : (coeff R p n) f ≠ 0
k✝ k : ℕ
ih : (coeff R p (n + k)) f ≠ 0
h : (coeff R p (n + k.succ)) f = 0
⊢ (coeff R p (n + k)) f = 0

Tactic:
rw [Nat.add_succ] at h

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Perfection R p
n : ℕ
hfn : (coeff R p n) f ≠ 0
k✝ k : ℕ
ih : (coeff R p (n + k)) f ≠ 0
h : (coeff R p (n + k).succ) f = 0
⊢ (coeff R p (n + k)) f = 0
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) (wittMulN p (n + 1) k)

Tactic:
wittMulN,

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.MulP

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

Tactic:
wittMulN,

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih : (bind₁ (wittMulN p n)) (wittPolynomial p ℤ k) = ↑n * wittPolynomial p ℤ k
⊢ (bind₁ fun k ↦ (bind₁ (Function.uncurry ![wittMulN p n, X])) (wittAdd p k)) (wittPolynomial p ℤ k) =
    ↑(n + 1) * wittPolynomial p ℤ k
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case calc_3
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] ((⇑frobenius)^[i] y)) =
    (⇑verschiebung)^[i] ((⇑verschiebung)^[j] ((⇑frobenius)^[i] y) * x)

Tactic:
mul_comm

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

Goal state before:
pp: case calc_6
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)^[i] y * (⇑frobenius)^[j] x) =
    (⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)

Tactic:
mul_comm

Goal state after:
case calc_6
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) =
    (⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case h
p n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ P : ℕ → Prop
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (select P x).coeff = fun n ↦ (aeval x.coeff) (selectPoly P n)

Tactic:
rintro R _Rcr x

Goal state after:
case h
p n : ℕ
R✝ : Type u_1
inst✝ : CommRing R✝
P✝ P : ℕ → Prop
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
⊢ (select P x).coeff = fun n ↦ (aeval x.coeff) (selectPoly P n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg.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
m n k : ℕ
hm : (Perfection.coeff (ModP O p) p (max (max m n) k)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max (max m n) k)) g ≠ 0
hk : (Perfection.coeff (ModP O p) p (max (max m n) k)) (f + g) ≠ 0
h :
  ModP.preVal K v O p ((coeff (max (max m n) k)) f + (coeff (max (max m n) k)) g) ≤
    ModP.preVal K v O p ((coeff (max (max m n) k)) g)
⊢ ModP.preVal K v O p ((coeff (max (max m n) k)) f + (coeff (max (max m n) k)) g) ^ p ^ max (max m n) k ≤
    max (ModP.preVal K v O p ((coeff (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O p ((coeff (max (max m n) k)) g) ^ p ^ max (max m n) k)

Tactic:
· exact le_max_of_le_right (pow_le_pow_left' h _)

Goal state after:
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
⊢ (∃ c, x = ↑p * c) ↔ x.coeff 0 = 0

Tactic:
mul_comm

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
⊢ (∃ c, x = c * ↑p) ↔ x.coeff 0 = 0
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 : ℕ
⊢ (∃ c, x = ↑p ^ n * c) ↔ ∀ m < n, x.coeff m = 0

Tactic:
mul_comm

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 : ℕ
⊢ (∃ c, x = c * ↑p ^ n) ↔ ∀ m < n, x.coeff m = 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
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
⊢ IsHausdorff 𝔭 R

Tactic:
infer_instance

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

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

Tactic:
mul_comm

Goal state after:
n k : ℕ
⊢ (hermite n).coeff k - (↑(k + 1) + 1) * (hermite n).coeff (k + 1 + 1) =
    (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)
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
⊢ CharP (ZMod p) p

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

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

Tactic:
· rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ op ((unop p).coeff (unop p).natDegree) = op (unop p).leadingCoeff

Tactic:
leadingCoeff

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ op ((unop p).coeff (unop p).natDegree) = op ((unop p).coeff (unop p).natDegree)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
⊢ p = q * (X - 1) ^ rootMultiplicity 1 p

Tactic:
exact hq1.trans (mul_comm _ _)

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
⊢ p = q * (X - 1) ^ rootMultiplicity 1 p

Tactic:
exact hq1.trans (mul_comm _ _)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
hroots : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
⊢ c = a * x1 * x2

Tactic:
by
  let p : R[X] := C a * X ^ 2 + C b * X + C c
  have hp_natDegree : p.natDegree = 2 := le_antisymm natDegree_quadratic_le
    (by convert! p.card_roots'; rw [hroots, Multiset.card_pair])
  have hp_roots_card : p.roots.card = p.natDegree := by
    rw [hp_natDegree, hroots, Multiset.card_pair]
  simpa [leadingCoeff, hp_natDegree, p, hroots, mul_assoc, add_comm x1] using
    coeff_eq_esymm_roots_of_card hp_roots_card (k := 0) (by simp [hp_natDegree])

Goal state after: