mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∈ Finset.range (n + 1), ↑p ^ (n + 1) ∣ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
intro i

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 : ℕ
⊢ i ∈ Finset.range (n + 1) → ↑p ^ (n + 1) ∣ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)

Tactic:
rw [map_sum]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ∑ x ∈ Finset.range n, (map (Int.castRingHom ℚ)) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ∀ x ∈ Finset.range n,
    (map (Int.castRingHom ℚ)) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
      C (↑p ^ x) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) x ^ p ^ (n - x)

Tactic:
intro i

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
⊢ i ∈ Finset.range n →
    (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
      C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑p ^ n = ↑↑(p ^ n)

Tactic:
norm_cast

Goal state after:
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 ∈ range n,
    C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x) * C (⅟↑p ^ n) -
        C (↑p ^ x) * X x ^ p ^ (n + 1 - x) * C (⅟↑p ^ n) =
      ∑ i ∈ range (p ^ (n - x)),
        C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            ((X x ^ p) ^ (p ^ (n - x) - (i + 1)) * frobeniusPolyAux p x ^ (i + 1) *
              C ↑((p ^ (n - x)).choose (i + 1) / p ^ (n - x - v p (i + 1)) * p ^ (i - v p (i + 1))))

Tactic:
intro i

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
i : ℕ
⊢ i ∈ range n →
    C (↑p ^ i) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ i) ^ p ^ (n - i) * C (⅟↑p ^ n) -
        C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
      ∑ i_1 ∈ range (p ^ (n - i)),
        C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
              C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))
Module: Mathlib.RingTheory.WittVector.IsPoly

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

Tactic:
intro i

Goal state after:
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
⊢ i ∈ Finset.range (n + 1) → i ≠ 0 → (bind₁ onePoly) (C (↑p ^ i) * X i ^ p ^ (n - i)) = 0
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
h : ∀ i < 0, x.coeff i = 0
⊢ x = (⇑verschiebung)^[0] (x.shift 0)

Tactic:
cases x; simp [shift]

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

Goal state before:
pp: case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0

Tactic:
intro i

Goal state after:
case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n i : ℕ
⊢ i ∈ Finset.range (n + 1) → i ≠ 0 → ↑p ^ i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:

Tactic:
(x + y).coeff n = z.coeff n := by rw [← hx, ← hy, select_add_select_not P z]
    _ = x.coeff n + y.coeff n := by
      simp only [z, mk.eq_1]
      split_ifs with y0
      · rw [y0, add_zero]
      · rw [h n |>.resolve_right y0, zero_add]

Goal state after:
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
⊢ ∀ (i : ℕ), (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)

Tactic:
intro i

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
i : ℕ
⊢ (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: case h
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 : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i
⊢ ∀ i < n, (x n).coeff i = (mk p fun n ↦ (x (n + 1)).coeff n).coeff i

Tactic:
intro i

Goal state after:
case h
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 : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i
i : ℕ
⊢ i < n → (x n).coeff i = (mk p fun n ↦ (x (n + 1)).coeff n).coeff i
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
x : 𝕎 R
n : ℕ
⊢ ∀ i < n + 1,
    x.coeff i = (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i

Tactic:
intro i

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
⊢ i < n + 1 →
    x.coeff i = (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
this : Nontrivial R
mapf : (PowerSeries.map (Ideal.Quotient.mk I)) f = ↑(X ^ g.natDegree) * (PowerSeries.map (Ideal.Quotient.mk I)) h
⊢ ∀ i < g.natDegree, (PowerSeries.coeff i) ((PowerSeries.map (Ideal.Quotient.mk I)) f) = 0

Tactic:
intro i

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
this : Nontrivial R
mapf : (PowerSeries.map (Ideal.Quotient.mk I)) f = ↑(X ^ g.natDegree) * (PowerSeries.map (Ideal.Quotient.mk I)) h
i : ℕ
⊢ i < g.natDegree → (PowerSeries.coeff i) ((PowerSeries.map (Ideal.Quotient.mk I)) f) = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: ⊢ X * hermite 0 - derivative (hermite 0) = X

Tactic:
hermite_zero

Goal state after:
⊢ X * C 1 - derivative (C 1) = X
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

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

Tactic:
norm_cast

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

Goal state before:
pp: case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1)) =
    ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + k).choose k) +
      ↑(2 * n - 1)‼ * (↑((2 * n + (k + 2)).choose (k + 2)) * (↑k + 2))

Tactic:
norm_cast

Goal state after:
case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * (n + 1) - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * (n + 1) - 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ↑d ! ≠ 0

Tactic:
norm_cast

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ¬d ! = 0
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ ↑d ! ≠ 0

Tactic:
norm_cast

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ ¬d ! = 0
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: case inr
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
this : ∀ (a b : R[X]), f = a * b → IsUnit (Polynomial.map ι b) → IsUnit a ∨ IsUnit b
hb : ¬IsUnit (Polynomial.map ι b)
⊢ IsUnit a ∨ IsUnit b

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)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
· exact (this b a (mul_comm a b ▸ h)
      (hi.2 (by rw [h, Polynomial.map_mul]) |>.resolve_right hb)).symm

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
hb : IsUnit (Polynomial.map ι b)
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: 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
i : ↥p.support
⊢ ↑((n - ↑i + d).choose d) = ↑((n + d - ↑i).choose d)

Tactic:
Nat.sub_add_comm (h_le i)

Goal state after:
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
i : ↥p.support
⊢ ↑((n - ↑i + d).choose d) = ↑((n - ↑i + d).choose d)
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
⊢ p.hilbertPoly d = 0

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : p = 0
⊢ p.hilbertPoly d = 0

case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
⊢ p.hilbertPoly d = 0
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
hp_natDegree : p.natDegree = 2
⊢ p.roots.card = p.natDegree

Tactic:
rw [hp_natDegree, hroots, Multiset.card_pair]

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

Goal state before:
pp: case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = ↑(↑(x + n)! / (↑x ! * ↑n !)) * ↑n !

Tactic:
norm_cast

Goal state after:
case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = ↑((x + n)! / (x ! * n !) * n !)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e'_3
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
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (Algebra.algHom R R S).toLinearMap 1 ⊗ₜ[R] x

Tactic:
toLinearMap_apply,

Goal state after:
case e'_3
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
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (Algebra.algHom R R S) 1 ⊗ₜ[R] x
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: case cons
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 : IsWeaklyRegular M (x :: tail✝)
⊢ IsWeaklyRegular N (List.map (⇑(algebraMap R S)) (x :: tail✝))

Tactic:
simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢

Goal state after:
case cons
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✝
⊢ IsSMulRegular N ((algebraMap R S) x) ∧
    IsWeaklyRegular (QuotSMulTop ((algebraMap R S) x) N) (List.map (⇑(algebraMap R S)) tail✝)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ g.IsWeierstrassDivisor

Tactic:
IsWeierstrassDivisor,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ g.IsWeierstrassDivisorAt (IsLocalRing.maximalIdeal A)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ IsUnit ((coeff ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat) g)

Tactic:
← IsLocalRing.notMem_maximalIdeal

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ (coeff ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat) g ∉ IsLocalRing.maximalIdeal A
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
⊢ f.ker = x • ⊤

Tactic:
simp only [LinearEquiv.ker_comp, f]

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
⊢ (Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))).ker = x • ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
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
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)

Tactic:
intro i

Goal state after:
case succ
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
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i : ℕ
⊢ (coeff i) q ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e'_3
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
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (Algebra.ofId R S).toLinearMap 1 ⊗ₜ[R] x

Tactic:
toLinearMap_apply,

Goal state after:
case e'_3
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
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (Algebra.ofId R S) 1 ⊗ₜ[R] x
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
inst✝ : IsAdicComplete I A
f : A⟦X⟧
⊢ (Ideal.Quotient.mk (Ideal.span {g})) ↑(H.mod' ((Ideal.Quotient.mk (Ideal.span {g})) f)) =
    (Ideal.Quotient.mk (Ideal.span {g})) f

Tactic:
rw [mod'_mk_eq_mod, Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
f : A⟦X⟧
⊢ ∃ a, a * g = f - ↑(H.mod f)
Module: Mathlib.RingTheory.SimpleRing.Congr

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e : TwoSidedIdeal R ≃o { I // I.IsTwoSided } := orderIsoIsTwoSided
⊢ IsSimpleRing R ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤

Tactic:
isSimpleRing_iff,

Goal state after:
R : Type u_1
inst✝ : Ring R
e : TwoSidedIdeal R ≃o { I // I.IsTwoSided } := orderIsoIsTwoSided
⊢ IsSimpleOrder (TwoSidedIdeal R) ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
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
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (IsLocalRing.residue A) ((coeff (n, 0).1) g) * (IsLocalRing.residue A) ((coeff (n, 0).2) q)
⊢ IsUnit ((IsLocalRing.residue A) (constantCoeff q))

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
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

Tactic:
coeff_zero_eq_constantCoeff,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (IsLocalRing.residue A) ((coeff (n, 0).1) g) * (IsLocalRing.residue A) (constantCoeff q)
⊢ IsUnit ((IsLocalRing.residue A) (constantCoeff q))

A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0