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

Goal state before:
pp: case refine_4
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₁
x✝ y✝ : S
⊢ liftFun f (x✝ + y✝) - (liftFun f x✝ + liftFun f y✝) ∈ ⊥

Tactic:
← iInf_ker_truncate,

Goal state after:
case refine_4
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₁
x✝ y✝ : S
⊢ liftFun f (x✝ + y✝) - (liftFun f x✝ + liftFun f y✝) ∈ ⨅ i, RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p : ℕ
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 : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ (lift f f_compat) x - g x ∈ ⊥

Tactic:
← iInf_ker_truncate,

Goal state after:
p : ℕ
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 : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
⊢ (lift f f_compat) x - g x ∈ ⨅ i, RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: case e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n = (⇑((frobeniusEquiv p k).symm.trans (frobeniusEquiv p k)))^[n] (x.shift n)

Tactic:
simp

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
n : ℕ
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ n]
this : x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ (n + 1)]
⊢ x✝.coeff n = coeff 0 n

Tactic:
simp only [Ideal.span_singleton_pow, SModEq.zero,
        mem_span_p_pow_iff_le_coeff_eq_zero] at this

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 : ℕ
h : ∀ (n : ℕ), x✝ ≡ 0 [SMOD Ideal.span {↑p} ^ n]
this : ∀ m < n + 1, x✝.coeff m = 0
⊢ x✝.coeff n = coeff 0 n
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case empty
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ ∅ ∧ (x r).coeff n ≠ 0}
n : ℕ
⊢ (∑ s ∈ ∅, x s).coeff n = ∑ s ∈ ∅, (x s).coeff n

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : R♭
⊢ (fontaineTheta R p) ((teichmuller p) x) ≡ untilt x [SMOD 𝔭 ^ 0]

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ f x =
    f (x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) +
      f (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i)

Tactic:
simp

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

Goal state before:
pp: case succ
n : ℕ
ih : (hermite n).coeff n = 1
⊢ n < n + 2

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ g (x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) +
      g (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) =
    g x

Tactic:
simp

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ ((2 * Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n)).comp (C ⅟2 * X) =
    (((2 * Chebyshev.T ℚ ↑m).comp (C ⅟2 * X)).comp (2 * Chebyshev.T ℚ ↑n)).comp (C ⅟2 * X)

Tactic:
apply eval₂_congr rfl rfl

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ (2 * Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n) = ((2 * Chebyshev.T ℚ ↑m).comp (C ⅟2 * X)).comp (2 * Chebyshev.T ℚ ↑n)
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ DifferentiableAt ℝ (fun y ↦ -(y ^ 2 / 2)) x

Tactic:
simp

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

Goal state before:
pp: x✝ : ℕ
⊢ (hermite (2 * 0 + x✝)).coeff x✝ = (-1) ^ 0 * ↑(2 * 0 - 1)‼ * ↑((2 * 0 + x✝).choose x✝)

Tactic:
simp

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

Goal state before:
pp: case e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + 0).choose 0) = -(hermite (2 * n + 1)).coeff 1

Tactic:
rw [coeff_hermite_explicit n 1, (by grind : 2 * (n + 1) - 1 = 2 * n + 1),
      Nat.doubleFactorial_add_one, Nat.choose_zero_right,
      Nat.choose_one_right, pow_succ]

Goal state after:
case e'_3
n : ℕ
⊢ (-1) ^ n * -1 * ↑((2 * n + 1) * (2 * n - 1)‼) * ↑1 = -((-1) ^ n * ↑(2 * n - 1)‼ * ↑(2 * n + 1))
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 K p

Tactic:
← f.charP_iff_charP

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ -(x ^ 2 / 2)) x

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
d k : ℕ
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ (X ^ k).support, (X ^ k).coeff i • preHilbertPoly F d i) =
    preHilbertPoly F d k

Tactic:
simp

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (aeval x) (hermite n) * (-1) ^ (n * 2)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
⊢ Irreducible f

Tactic:
refine ⟨fun h ↦ hi.1 <| (mapRingHom ι).isUnit_map h, fun a b h ↦ ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : Rᵐᵒᵖ
⊢ (opRingEquiv R) ((opRingEquiv R).symm ((monomial n) r)) = (opRingEquiv R) (op ((monomial n) (unop r)))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
a✝ : ℕ
⊢ a✝ ∈ ((opRingEquiv R) p).support ↔ a✝ ∈ (unop p).support

Tactic:
simp

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

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (p * (1 - X) ^ 0).hilbertPoly (d + 0) = p.hilbertPoly d

Tactic:
simp

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

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

Tactic:
rw [sub_eq_add_neg, add_comm, add_pow]

Goal state after:
case e_a
n : ℕ
⊢ ∑ m ∈ range (n + 1), (-X ^ 2) ^ m * X ^ (n - m) * ↑(n.choose m) =
    ∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ n.choose x • (-1) ^ x = C (n.choose x • (-1) ^ x)

Tactic:
simp

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

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2}
⊢ 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)

Tactic:
simp

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

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ 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)

Tactic:
simp

Goal state after:
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
⊢ 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)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ n ≤ n + n

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ (coeff 0) (catalanSeries ^ 2 * X + 1) = (coeff 0) catalanSeries

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
hg : ∀ i ≤ n, (coeff i) g ∈ I
⊢ ∀ i ≤ n, (coeff i) f ∈ ⊤

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
hg : ∀ (i : ℕ), (coeff i) g ∈ I
⊢ ∀ (i : ℕ), (coeff i) f ∈ ⊤

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
inst✝ : I.IsTwoSided
hf : ∀ i ≤ n, (coeff i) f ∈ I
⊢ ∀ i ≤ n, (coeff i) g ∈ 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
inst✝ : I.IsTwoSided
hf : ∀ (i : ℕ), (coeff i) f ∈ I
⊢ ∀ (i : ℕ), (coeff i) g ∈ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq { P // P.FG }
x : M
⊢ (Module.DirectLimit.lift R { P // P.FG } (fun P ↦ ↥↑P) (fun ⦃P Q⦄ h ↦ inclusion h) (fun P ↦ (↑P).subtype) ⋯)
      ((Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P) (fun ⦃P Q⦄ h ↦ inclusion h) ⟨R ∙ x, ⋯⟩) ⟨x, ⋯⟩) =
    x

Tactic:
simp

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

Goal state before:
pp: R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : F k ⊗[R] N
⊢ (LinearMap.rTensor N (f h')) ((LinearMap.rTensor N (f h)) t) = (LinearMap.rTensor N (f ⋯)) t

Tactic:
rw [← comp_apply, ← rTensor_comp]

Goal state after:
R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : F k ⊗[R] N
⊢ (LinearMap.rTensor N (f h' ∘ₗ f h)) t = (LinearMap.rTensor N (f ⋯)) t
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
⊢ (expand 1 ⋯) f = f

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ (coeff 0) φ = constantCoeff φ

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
H : Tendsto ((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) cofinite (𝓝 0)
n : ℕ
⊢ (((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) ∘ ⇑(Finsupp.uniqueEquiv ()).symm) n =
    ‖(coeff n) f‖ * c ^ n

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff 1) (log A) = 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : Nontrivial A
⊢ (coeff 1) (log A) ≠ 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑n + 1 = (algebraMap ℚ A) (↑n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inl
⊢ primeFactors 0 = Finset.map Nat.castEmbedding (Int.natAbs 0).primeFactors

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
⊢ 0 ≤ ↑n

Tactic:
simp

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
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 θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M
          (((↑(quotientKerEquivRangeₐ ψ).symm).comp ↑(quotientKerEquivRangeₐ ψ)).comp
              (mkₐ R (RingCon.ker ↑ψ))).toLinearMap)
        q) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)

Tactic:
simp

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
A : Type u
inst✝³ : CommSemiring A
inst✝² : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
q : B ⊗[R] M
ψ : B →ₐ[R] S
h : φ.range ≤ ψ.range
hpq :
  (rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
x : ↥φ.range
⊢ (ψ.range.val.comp (Subalgebra.inclusion h)) x = ((AlgHom.id R S).comp φ.range.val) x

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: case nil
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Flat R S
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsWeaklyRegular M []
⊢ IsWeaklyRegular N (List.map ⇑(algebraMap R S) [])

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Flat R S
x : R
tail✝ : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : AddCommGroup N]
    [inst_3 : Module R N] [inst_4 : Module S N] [inst_5 : IsScalarTower R S N] {f : M →ₗ[R] N},
    IsBaseChange S f → IsWeaklyRegular M tail✝ → IsWeaklyRegular N (List.map (⇑(algebraMap R S)) tail✝)
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsSMulRegular M x ∧ IsWeaklyRegular (QuotSMulTop x M) tail✝
e : TensorProduct R S (QuotSMulTop x M) ≃ₗ[S] QuotSMulTop ((algebraMap R S) x) N
x✝ : QuotSMulTop x M
⊢ e (1 ⊗ₜ[R] x✝) = (↑R ↑e ∘ₗ (TensorProduct.mk R S (QuotSMulTop x M)) 1) x✝

Tactic:
simp

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

Goal state before:
pp: case eq_mul_add
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ 0 = g * 0 + ↑0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
hI : I ≠ ⊤
⊢ ↑g = ↑g * 1

Tactic:
simp

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

Goal state before:
pp: case zero
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.seq f 0) ∈ I ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
fg : g.ker.FG
y : I →₀ R
hy : y ∈ g.ker
⊢ y ∈ x • g.ker

Tactic:
have : y ∈ x • (⊤ : Submodule R (I →₀ R)) := by simp [← kerf, ← hg, LinearMap.mem_ker.mp hy]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this✝ : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
fg : g.ker.FG
y : I →₀ R
hy : y ∈ g.ker
this : y ∈ x • ⊤
⊢ y ∈ x • g.ker
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i✝¹ : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i✝¹ ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
i✝ i : ℕ
⊢ i + n ≥ n

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i✝ i : ℕ
⊢ i + ((map (Ideal.Quotient.mk I)) g).order.toNat ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (rTensor M φ.rangeRestrict.toLinearMap) p = (rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (rTensor M φ.toLinearMap) p = (rTensor M (φ.range.val.comp φ.rangeRestrict).toLinearMap) p

Tactic:
simp

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

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ 0

Tactic:
simp

Goal state after: