mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective ⇑(esymmAlgHom σ R n)

Tactic:
← rename_esymmAlgHom (Fintype.equivFin σ).symm,

Goal state after:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective
    ⇑((↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm)).comp (esymmAlgHom (Fin (Fintype.card σ)) R n))
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective ⇑(esymmAlgHom σ R n)

Tactic:
← rename_esymmAlgHom (Fintype.equivFin σ).symm,

Goal state after:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective
    ⇑((↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm)).comp (esymmAlgHom (Fin (Fintype.card σ)) R n))
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
d : σ →₀ ℕ
hd : d ≠ m
⊢ ((coeff d) φ * if p • m = p • d then 1 else 0) = 0

Tactic:
if_neg _,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
d : σ →₀ ℕ
hd : d ≠ m
⊢ (coeff d) φ * 0 = 0

σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
d : σ →₀ ℕ
hd : d ≠ m
⊢ ¬p • m = p • d
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ (trunc' R (p • n)) ((expand p hp) φ) = (MvPolynomial.expand p) ((trunc' R n) φ)

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ (map f) (W_ R n) = W_ S n

Tactic:
by
  rw [wittPolynomial, map_sum, wittPolynomial]
  refine sum_congr rfl fun i _ => ?_
  rw [map_monomial, map_pow, map_natCast]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((T f) (MvPolynomial.C (MvPolynomial.coeff v f) * ∏ i, MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

pp: case h
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), MvPolynomial.X i ^ 0 = 1

Tactic:
· simp only [map_mul, map_prod, leadingCoeff_mul, leadingCoeff_prod]
    rw [AlgEquiv.ofAlgHom_apply, algHom_C, algebraMap_eq, finSuccEquiv_apply,
      eval₂Hom_C, coe_comp]
    simp only [AlgEquiv.ofAlgHom_apply, Function.comp_apply, leadingCoeff_C, map_pow,
      leadingCoeff_pow, algebraMap_eq]
    have : ∀ j, ((finSuccEquiv k n) ((T1 f) 1 (X j))).leadingCoeff = 1 := fun j ↦ by
      by_cases h : j = 0
      · simp [h, finSuccEquiv_apply]
      · simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]
        obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h
        simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]
    simp only [this, one_pow, Finset.prod_const_one, mul_one]

Goal state after:
case h
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), MvPolynomial.X i ^ 0 = 1
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
this : (T f).symm.toRingEquiv.toRingHom.comp ↑(T f) = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ I = Ideal.map ((T f).symm.toRingEquiv.toRingHom.comp ↑(T f)) I

Tactic:
rw [this, Ideal.map_id]

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

Goal state before:

Tactic:
wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
    _ = _ := by rw [wittStructureRat_rec_aux]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n))
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : (aeval x) ((bind₁ (xInTermsOfW p R)) (W_ R n)) = (aeval x) (X n)
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x).ghostFun n = x n

Tactic:
simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial]

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

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ∑ x ∈ Finset.range (n + 1),
      (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ x * (expand p) (wittStructureInt p Φ x) ^ p ^ (n - x)) =
    ∑ x ∈ Finset.range (n + 1),
      (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))

Tactic:
Finset.sum_congr rfl

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (Finset.range (n + 1)).sum ?m.282 =
    ∑ x ∈ Finset.range (n + 1),
      (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))

case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ x * (expand p) (wittStructureInt p Φ x) ^ p ^ (n - x)) = ?m.282 x

p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ℕ → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1)))
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)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)

Tactic:
apply Finset.sum_congr rfl

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)) =
      C (↑p ^ x) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) x ^ p ^ (n - x)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∑ k ∈ Finset.range (n + 1), ↑p ^ (k + 1) * x.verschiebungFun.coeff (k + 1) ^ p ^ (n + 1 - (k + 1)) =
    ∑ i ∈ Finset.range (n + 1), ↑p * (↑p ^ i * x.coeff i ^ p ^ (n - i))

Tactic:
Finset.sum_congr rfl

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ (Finset.range (n + 1)).sum ?m.78 = ∑ i ∈ Finset.range (n + 1), ↑p * (↑p ^ i * x.coeff i ^ p ^ (n - i))

p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∀ x_1 ∈ Finset.range (n + 1), ↑p ^ (x_1 + 1) * x.verschiebungFun.coeff (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) = ?m.78 x_1

p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ℕ → R
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ w.coeff n = coeff 0 n

Tactic:
rw [← verschiebung_coeff_succ, h]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ coeff 0 n.succ = coeff 0 n
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ C (↑p ^ i) * (X i ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux 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))))

Tactic:
add_comm (X i ^ p),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ C (↑p ^ i) * (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) + X i ^ p) ^ 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.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : v ((algebraMap O K) r) ≤ v ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) r = 0

Tactic:
← map_natCast (algebraMap O K) p,

Goal state after:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : v ((algebraMap O K) r) ≤ v ((algebraMap O K) ↑p)
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
⊢ v ((algebraMap O K) x) ≤ v ↑p ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x = 0

Tactic:
← map_natCast (algebraMap O K) p,

Goal state after:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
⊢ v ((algebraMap O K) x) ≤ v ((algebraMap O K) ↑p) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x = 0
Module: Mathlib.RingTheory.WittVector.Identities

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

Tactic:
rw [mul_comm]

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

Goal state before:
pp: case calc_6
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung)^[i + j] ((⇑frobenius)^[i] y * (⇑frobenius)^[j] x) =
    (⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)

Tactic:
rw [mul_comm]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ verschiebung (x.shift k.succ) = x.shift k

Tactic:
ext ⟨j⟩

Goal state after:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ (verschiebung (x.shift k.succ)).coeff 0 = (x.shift k).coeff 0

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ (verschiebung (x.shift k.succ)).coeff (n✝ + 1) = (x.shift k).coeff (n✝ + 1)
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∑ x ∈ Finset.range (n + 1),
      C ↑p ^ x * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) =
    ∑ x ∈ Finset.range (n + 1), C ↑p ^ x * X x ^ p ^ (n - x)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    C ↑p ^ x * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) =
      C ↑p ^ x * X x ^ p ^ (n - x)
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
x : R
m n : ℕ
h : m ≠ n
⊢ ((teichmuller p) x * ↑p ^ n).coeff m = 0

Tactic:
by
  cases Nat.lt_or_lt_of_ne h with
  | inl h =>
    exact WittVector.mul_pow_charP_coeff_zero (teichmuller p x) h
  | inr h =>
    rw [← Nat.sub_add_cancel h.le, WittVector.mul_pow_charP_coeff_succ (teichmuller p x),
      WittVector.teichmuller_coeff_pos p x (m - n) (Nat.zero_lt_sub_of_lt h), zero_pow]
    simp [Nat.Prime.ne_zero Fact.out]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
⊢ dickson k a (n + 2) = X * dickson k a (n + 1) - C a * dickson k a n

Tactic:
rw [dickson]

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

Goal state before:
pp: case h.left
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (fun h ↦ ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) (p.hilbertPoly d)

Tactic:
use p.natDegree
    exact fun n => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d

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

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n * (shiftedLegendre n).comp (1 - X) = shiftedLegendre n

Tactic:
refine nat_mul_inj' ?_ (factorial_ne_zero n)
  rw [← mul_assoc, mul_comm (n ! : ℤ[X]), mul_assoc, ← natCast_mul_comp,
    factorial_mul_shiftedLegendre_eq, ← iterate_derivative_comp_one_sub_X]
  simp [mul_comm]

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⟧
m : ℕ
h : ¬p ∣ m
⊢ (coeff m) ((expand p hp) φ) = 0

Tactic:
rw [coeff, expand, MvPowerSeries.coeff_expand_of_not_dvd (i := ())]
  simpa

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 := ⋯
⊢ ↑w ⊆ ↑(s ∪ w)

Tactic:
simp only [Finset.coe_union, Set.subset_union_right]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
⊢ (coeff i) (g * q) ∈ I

Tactic:
refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal i (fun j hj ↦ ?_) i le_rfl

Goal state after:
A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
j : ℕ
hj : j ≤ i
⊢ (coeff j) g ∈ I
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
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
⊢ p = Ideal.map C (span (Submodule.generators (maximalIdeal R))) ⊔ span {y}

Tactic:
hy,

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
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
⊢ Ideal.map C (comap C p) ⊔ span {y} = Ideal.map C (span (Submodule.generators (maximalIdeal R))) ⊔ span {y}
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + (↑n + 1)

Tactic:
projectiveDimension_eq_of_iso
        (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x rs').toModuleIso,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (QuotSMulTop x ↑M ⧸ Ideal.ofList rs' • ⊤)) = projectiveDimension M + (↑n + 1)
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
have disj : Disjoint (pc : Set R[X]) (p : Set R[X]) := by
    simpa [pc, q] using! Set.disjoint_image_left.mpr
      (Set.disjoint_compl_left_iff_subset.mpr (fun _ a ↦ a))

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q))
      (comap ((algebraMap R[X] (Localization.AtPrime q)[X]).comp (algebraMap R R[X]))
        (Ideal.map (algebraMap R[X] (Localization.AtPrime q)[X]) p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))

Tactic:
← comap_comap,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q))
      (comap (algebraMap R R[X])
        (comap (algebraMap R[X] (Localization.AtPrime q)[X])
          (Ideal.map (algebraMap R[X] (Localization.AtPrime q)[X]) p))) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝³ : Ring R
inst✝² : Ring S
e : ModuleCat R ⥤ ModuleCat S
inst✝¹ : e.IsEquivalence
M : ModuleCat R
inst✝ : IsSimpleModule R ↑M
⊢ IsSimpleModule S ↑(e.obj M)

Tactic:
← simple_iff_isSimpleModule'

Goal state after:
R : Type u_3
S : Type u_4
inst✝³ : Ring R
inst✝² : Ring S
e : ModuleCat R ⥤ ModuleCat S
inst✝¹ : e.IsEquivalence
M : ModuleCat R
inst✝ : Simple M
⊢ Simple (e.obj M)
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
⊢ IsOpen (comap f '' (fun r ↦ ↑(basicOpen r)) s)

Tactic:
obtain ⟨n, hn, r, hr⟩ := H s

Goal state after:
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
⊢ IsOpen (comap f '' (fun r ↦ ↑(basicOpen r)) s)