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

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : ¬f = 0
x✝ : K⸨X⸩
hg : Valued.v (x✝ - f) ≤ 1
n : ℤ
hn : n < min (⋯.min ⋯) 0 - 1
⊢ x✝.coeff n = 0

Tactic:
eq_coeff_of_valuation_sub_lt K hg (d := 0)

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : ¬f = 0
x✝ : K⸨X⸩
hg : Valued.v (x✝ - f) ≤ 1
n : ℤ
hn : n < min (⋯.min ⋯) 0 - 1
⊢ f.coeff n = 0

case neg
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : ¬f = 0
x✝ : K⸨X⸩
hg : Valued.v (x✝ - f) ≤ 1
n : ℤ
hn : n < min (⋯.min ⋯) 0 - 1
⊢ n < 0
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
this : ∀ (x : n →₀ ℕ), d ≠ x → x ∈ f.support → i ∉ x.support
⊢ i ∉ ψ.vars

Tactic:
by
      simpa [mem_vars_iff_mem_support, hdψ] using this

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

Goal state before:
pp: case hp.a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ (∑ x ∈ c.support, c x • X x).totalDegree ≤ 1

Tactic:
apply totalDegree_finsetSum_le

Goal state after:
case hp.a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ∀ i ∈ c.support, (c i • X i).totalDegree ≤ 1
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
i j : n
⊢ (fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1) i =
      (fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1) j →
    i = j

Tactic:
simp +contextual [Finsupp.ext_iff, Finsupp.single_apply, ite_eq_iff']

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
rw [hs, ← F_mul, PowerSeries.coe_pow, PowerSeries.coe_X, map_mul, zpow_neg,
        zpow_natCast, inv_eq_one_div (RatFunc.X ^ s), map_div₀, map_pow,
        RatFunc.coe_X]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v
      (((single 1) 1 ^ s)⁻¹ * (ofPowerSeries ℤ K) F -
        (algebraMap K⟮X⟯ K⸨X⸩) 1 / (single 1) 1 ^ s * (algebraMap K⟮X⟯ K⸨X⸩) ↑P) <
    ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ pairMap σ t ∈ pairs σ k

Tactic:
rw [mem_pairs] at h ⊢

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

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2
this : {a ∈ antidiagonal k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2

Tactic:
simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] at sub_both_sides

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ antidiagonal k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 =
    psum σ R k
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f : MvPowerSeries σ R
hf : IsRestricted c f
⊢ IsRestricted c (-f)

Tactic:
rw [← isRestricted_abs_iff, IsRestricted] at *
  simpa [IsRestricted] using hf

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
⊢ (x * y).teichmullerFun = x.teichmullerFun * y.teichmullerFun

Tactic:
refine teichmullerFun_spec fun n ↦ ?_

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ ∃ z,
    (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) (x * y) ∧
      z ^ p ^ n ≡ x.teichmullerFun * y.teichmullerFun [SMOD I ^ (n + 1)]
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ Disjoint (X n).vars (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars

Tactic:
rw [vars_X, disjoint_singleton_left]

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∉ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ (bind₁ (xInTermsOfW p R)) (∑ i ∈ range (k + 1), C (↑p ^ i) * X i ^ p ^ (k - i)) = X k

Tactic:
map_sum

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x ∈ range (k + 1), (bind₁ (xInTermsOfW p R)) (C (↑p ^ x) * X x ^ p ^ (k - x)) = X k
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:
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.Verschiebung

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) = (MvPolynomial.eval x) 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n - 1))

Tactic:
· simp only [hn, wittPolynomial_zero, bind₁_X_right, verschiebungPoly_zero, map_zero]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n - 1))
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
x y : 𝕎 R
⊢ x * y = 0 → x = 0 ∨ y = 0

Tactic:
by
    contrapose!
    rintro ⟨ha, hb⟩
    rcases verschiebung_nonzero ha with ⟨na, wa, hwa0, rfl⟩
    rcases verschiebung_nonzero hb with ⟨nb, wb, hwb0, rfl⟩
    refine ne_of_apply_ne (fun x => x.coeff (na + nb)) ?_
    rw [iterate_verschiebung_mul_coeff, zero_coeff]
    exact mul_ne_zero (pow_ne_zero _ hwa0) (pow_ne_zero _ hwb0)

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

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ∀ i < m, x.coeff i = 0
⊢ ∀ i < n, x.coeff i = 0

Tactic:
i

Goal state after:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ∀ i < m, x.coeff i = 0
i : ℕ
⊢ i < n → x.coeff i = 0
Module: Mathlib.RingTheory.Polynomial.Dickson

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

Tactic:
have h : (1 : R) = Int.castRingHom R 1 := by simp only [eq_intCast, Int.cast_one]
  rw [h]
  simp only [← map_dickson (Int.castRingHom R), ← map_comp]
  congr 1
  apply map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [map_dickson, map_comp, eq_intCast, Int.cast_one, dickson_one_one_eq_chebyshev_T,
    Nat.cast_mul, Chebyshev.T_mul, two_mul, ← add_comp]
  simp only [← two_mul, ← comp_assoc]
  apply eval₂_congr rfl rfl
  rw [comp_assoc]
  apply eval₂_congr rfl _ rfl
  rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]

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

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

pp: case e_a.e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)

Tactic:
· rw [coeff_hermite_explicit (n + 1) k]

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)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)
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)
⊢ Free R M

Tactic:
let b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := b.1.restrictScalars R

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
⊢ Free R M
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f f' g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (f + f') %ʷ g = f %ʷ g + f' %ʷ g

Tactic:
simp_rw [weierstrassMod]

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f f' g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ (f + f') else 0) =
    (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ f else 0) +
      if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ f' else 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
a : A
f g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ a • f %ʷ g = a • (f %ʷ g)

Tactic:
simp_rw [weierstrassMod]

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
a : A
f g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ (a • f) else 0) =
    a • if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ f else 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ 0 %ʷ g = 0

Tactic:
simp_rw [weierstrassMod]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : constantCoeff h ∈ I
⊢ I = ⊤

Tactic:
exact Ideal.eq_top_of_isUnit_mem _ hI (isUnit_iff_constantCoeff.1 H.isUnit)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
val✝ : Multiset ι
nodup✝ : val✝.Nodup
hs : ∃ x ∈ { val := val✝, nodup := nodup✝ }, f x ∈ I
⊢ { val := val✝, nodup := nodup✝ }.prod f ∈ I

Tactic:
simpa using multiSetProd_mem (hs := hs)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ s.prod f ∈ I

Tactic:
rcases s
  simpa using multiSetProd_mem (hs := hs)

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

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

Tactic:
rw [← commutes' _ _ hm]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) =
    (truncate hm) ((zmodEquivTrunc p m) ((zmodEquivTrunc p m).symm x))
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
n : ℕ
b : (𝕎 k)ˣ
hb : x = ↑p ^ n * ↑b
⊢ ∃ n, Associated (↑p ^ n) x

Tactic:
exact ⟨n, b, hb.symm⟩

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

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) (∑ i ∈ range (n + 1), (monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
map_sum

Goal state after:
case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    ∑ x ∈ range (n + 1), (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single x (p ^ (n - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
      (rename (Prod.mk 1)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            (rename (Prod.mk 1)) (∑ i ∈ range (n + 1 + 1), (monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n

Tactic:
map_sum

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 1 < ↑p

Tactic:
exact mod_cast hp.out.one_lt

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p (n + 1)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
apply wittPolyProdRemainder_vars

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
s : Set (Set α)
inst✝ : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)

Tactic:
by
  refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩
  rw [isCofinal_iff_top_mem, mem_sInter]
  exact fun x hx ↦ (hs x hx).isCofinal.top_mem

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂ i, f i)

Tactic:
rw [← sInter_range]
  refine IsClub.sInter hα ?_ (by simpa)
  rw [← Cardinal.lift_lt]
  exact mk_range_le_lift.trans_lt hι

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
hs : ¬IsCofinal sᶜ
t : Set α
ht : IsClub t
a : α
ha : ∀ y ∈ sᶜ, y < a
b : α
hb : b ∈ t
hb' : a ≤ b
⊢ (s ∩ t).Nonempty

Tactic:
refine ⟨b, ?_, hb⟩

Goal state after:
α : Type v
s : Set α
inst✝ : LinearOrder α
hs : ¬IsCofinal sᶜ
t : Set α
ht : IsClub t
a : α
ha : ∀ y ∈ sᶜ, y < a
b : α
hb : b ∈ t
hb' : a ≤ b
⊢ b ∈ s
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False

Tactic:
mk_initialSeg_subtype,

Goal state after:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} (lift.{u + 1, u} (succ #α)) ≤ lift.{u + 1, u} #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil

Tactic:
← of_toList l

Goal state after:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ nil → ofList l.toList = nil