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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
have heq : 1 - PowerSeries.X = ((1 - X : F[X]) : F⟦X⟧) := by simp only [coe_sub, coe_one, coe_X]

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (⇑derivative)^[n] (X ^ n * (1 - X) ^ n) = (⇑derivative)^[n] ((X - X ^ 2) ^ n)

Tactic:
by
    rw [← mul_pow, mul_one_sub, ← pow_two]

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}
p : R[X] := C a * X ^ 2 + C b * X + C c
⊢ 2 ≤ p.natDegree

Tactic:
convert! p.card_roots'

Goal state after:
case e'_3
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}
p : R[X] := C a * X ^ 2 + C b * X + C c
⊢ 2 = p.roots.card
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝ : Field R
a b c x1 x2 : R
ha : a ≠ 0
⊢ b = -a * (x1 + x2) ∧ c = a * x1 * x2 ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a

Tactic:
grind

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

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
P : { P // P.FG }
u : ↥↑P ⊗[R] N
this :
  ↑(directLimit R M N) ∘ₗ
      Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun x x_1 hPQ ↦ rTensor N (inclusion hPQ)) P =
    rTensor N (↑P).subtype
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) P) u) =
    (rTensor N (↑P).subtype) u

Tactic:
exact DFunLike.congr_fun this u

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
t : Unit →₀ ℕ
⊢ Finsupp.single () (t ()) = t

Tactic:
grind

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ (coeff n) (X * largeSchroderSeries) = (n - 1).largeSchroder

Tactic:
simp only [coeff_mul, coeff_largeSchroderSeries,
    Nat.sum_antidiagonal_eq_sum_range_succ (coeff · X * largeSchroder ·),
    succ_eq_add_one]

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∑ k ∈ range (n + 1), (coeff k) X * (n - k).largeSchroder = (n - 1).largeSchroder
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
this :
  ↑(directLimit R M N) ∘ₗ
      Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q =
    lTensor M (↑Q).subtype
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q) u) =
    (lTensor M (↑Q).subtype) u

Tactic:
exact DFunLike.congr_fun this u

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
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ ↑0 • f = 0

Tactic:
simp only [Nat.cast_zero, zero_smul f]

Goal state after:
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
x : ℕ
hx : x ∈ Ico 1 n
⊢ 0 < x

Tactic:
grind

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (if n + 1 = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1 + 1) / ↑(n + 1))) * (↑n + 1) = (algebraMap ℚ A) ((-1) ^ n)

Tactic:
grind

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : N →ₚₗ[R] P
x✝³ : Type u
x✝² : CommSemiring x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] N
⊢ (g.comp id).toFun' x✝³ x✝ = g.toFun' x✝³ x✝

Tactic:
rfl

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
x✝³ : Type u
x✝² : CommSemiring x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (id.comp f).toFun' x✝³ x✝ = f.toFun' x✝³ x✝

Tactic:
rfl

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
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'

Tactic:
let j : P →ₗ[R] P₁ := (Subalgebra.toSubmodule A).subtype.restrict
      (fun p hp ↦ by
        simp only [coe_subtype, Submodule.map_sup, P₁]
        exact Submodule.mem_sup_left ⟨p, hp, rfl⟩)

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 ⋯
⊢ ∃ B,
    ∃ (hAB : A ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'
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 := ⋯
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := ⋯
j' : ↥P' →ₗ[R] ↥P₁ := ⋯
u₁ : ↥P₁ ⊗[R] N := ⋯
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := ⋯
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := ⋯
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
x✝ : ↥P
⊢ ↑(((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype) x✝) = ↑((inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j) x✝)

Tactic:
rfl

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 := ⋯
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := ⋯
j' : ↥P' →ₗ[R] ↥P₁ := ⋯
u₁ : ↥P₁ ⊗[R] N := ⋯
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := ⋯
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := ⋯
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j
x✝ : ↥P'
⊢ ↑(((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype) x✝) = ↑((inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j') x✝)

Tactic:
rfl

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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A'.val.toLinearMap) t'
x✝ : ↥A
⊢ ((A ⊔ A').val.comp (Subalgebra.inclusion ⋯)) x✝ = A.val x✝

Tactic:
rfl

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
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor M (Subalgebra.inclusion hA'B').toLinearMap) u' =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hA'B)).toLinearMap) u'

Tactic:
rfl

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 : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A'.val.toLinearMap) t'
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
x✝ : ↥A'
⊢ ((A ⊔ A').val.comp (Subalgebra.inclusion ⋯)) x✝ = A'.val x✝

Tactic:
rfl

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

Goal state before:
pp: case e_f
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
x✝¹ : ↥(φ R s).range
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor M (Subalgebra.inclusion hAB').toLinearMap)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          (rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ rTensor M (Subalgebra.inclusion hAB).toLinearMap))
        x✝¹)
      x✝

Tactic:
rfl

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

Goal state before:
pp: case pos
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.div f) = (coeff i) (f - g * H.div f)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
have fg' := (maximalIdeal R).fg_of_isNoetherianRing

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)
⊢ HasProjectiveDimensionLT M 0

Tactic:
have : Subsingleton (M ⟶ M) := Ext.homEquiv₀.subsingleton_congr.mp (h M ‹_›)

Goal state after:
case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)
this : Subsingleton (M ⟶ M)
⊢ HasProjectiveDimensionLT M 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
⊢ f /ₘ g * g = f - f %ₘ g

Tactic:
by rw [Polynomial.modByMonic_eq_sub_mul_div]; ring

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
this : f.degree = ↑n
⊢ WithBot.unbotD 0 ↑n = n

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Nontrivial M ∧
    ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
hM1 : Nontrivial M
hM2 : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
p : Submodule R M
h : p.mkQ = 0
⊢ p = ⊤

Tactic:
by simpa [Submodule.ext_iff, LinearMap.ext_iff] using h

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)

Tactic:
rw [imageOfDf, ofPred_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]
  exact isOpen_iUnion fun i => isOpen_basicOpen

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∃ x ∈ l, f x ∈ I
⊢ (List.map f l).prod ∈ I

Tactic:
induction l with
  | nil => simp only [List.not_mem_nil, false_and, exists_false] at hl
  | cons x l ih =>
    simp only [List.mem_cons, exists_eq_or_imp] at hl
    rcases hl with h | hal
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_left _ _ <| ih hal

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : f r = s ^ n
⊢ ↑(basicOpen (f r)) = comap f ⁻¹' ↑(basicOpen r)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
r✝ : R ⧸ J
x : R
⊢ ((comap (Ideal.Quotient.mk J) v).onQuot ⋯) (Quot.mk (⇑(Submodule.quotientRel J)) x) =
    v (Quot.mk (⇑(Submodule.quotientRel J)) x)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst✝² : LinearOrderedCommGroupWithZero ΓR
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
r : ↥vR.integer
a : ↥vA.integer
⊢ ↑(r • a) = ↑r • ↑a

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst✝² : LinearOrderedCommGroupWithZero ΓR
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
r : ↥vR.integer
⊢ ↑((algebraMap ↥vR.integer ↥vA.integer) r) = (algebraMap R A) ↑r

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : ZMod (p ^ n)
⊢ p ^ n ∣ p ^ n

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ((zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))) x =
    (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)

Tactic:
rfl

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

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
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ verschiebung (frobenius x) = (⇑verschiebung ∘ ⇑frobenius) x

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProdRemainder p n + ↑p ^ n * wittMul p n =
    ∑ x ∈ range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ False

Tactic:
zero_pow

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False

p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ p - 1 ≠ 0
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this✝ : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
this : ∃ k, p = k.succ
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
grind

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

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
i : Fin (n + 1)
⊢ (mk p (frobeniusRotationCoeff p ha₁ ha₂)).coeff ↑i ^ p =
    TruncatedWittVector.coeff i fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
this : 2 ≤ p
⊢ p - 1 ≠ 0

Tactic:
grind

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
⊢ a ∈ S

Tactic:
grind

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

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

Tactic:
rfl

Goal state after: