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

Goal state before:
pp: case inl
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : ↑i + 1 < m
⊢ t i = s i

Tactic:
have := accumulate_rec i.2 h s

Goal state after:
case inl
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : ↑i + 1 < m
this : (accumulate n m) s ⟨↑i, ⋯⟩ = s ⟨↑i, ⋯⟩ + (accumulate n m) s ⟨↑i + 1, h⟩
⊢ t i = s i
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case isPrimitive
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
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
r : R
hr : ∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)
⊢ IsUnit r

Tactic:
apply h_dvd

Goal state after:
case isPrimitive
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
ι : n ↪ n ⊕ n →₀ ℕ := ⋯
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
r : R
hr : ∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)
⊢ ∀ (i : n), r ∣ c i
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
| (f ^ p ^ k) ^ p

Tactic:
← n_ih

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
| (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) ^ p
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ X i ^ 0 = 1

Tactic:
pow_zero

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ 1 = 1
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p n : ℕ
⊢ ∑ i ∈ range (n + 1 + 1), C (↑p ^ i) * X i ^ p ^ (n + 1 - i) =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))

Tactic:
sum_range_succ,

Goal state after:
p n : ℕ
⊢ ∑ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) + C (↑p ^ (n + 1)) * X (n + 1) ^ p ^ (n + 1 - (n + 1)) =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X 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 : ℕ
⊢ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (X n) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ

Tactic:
bind₁_X_right

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = (bind₁ φ) (X n)

Tactic:
bind₁_X_right

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = φ n
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ n) = 0

Tactic:
xInTermsOfW_eq

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) ((X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ b ∈ Finset.range n, b ≠ 0 → C ↑p ^ b * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0

Tactic:
intro i hin hi0
    rw [Finset.mem_range] at hin
    rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
⊢ (m • x).ghostFun = m • x.ghostFun

Tactic:
by
  ghost_fun_tac m • (X 0), ![x.coeff]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
⊢ (m • x).ghostFun = m • x.ghostFun

Tactic:
by
  ghost_fun_tac m • (X 0), ![x.coeff]

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)
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)

Tactic:
xInTermsOfW_eq

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

Tactic:
sum_range_succ,

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

Tactic:
sum_range_succ,

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

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n ≤ m
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

Tactic:
have h1' : n ≤ m + 1 := by lia
      simp only [h1', ↓reduceDIte, h1, Nat.leRec_succ, ← frobenius_def]
      exact Classical.choose_spec (h _)

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) = ((2 * Chebyshev.T ℚ ↑m).comp (C ⅟2 * X)).comp (2 * Chebyshev.T ℚ ↑n)

Tactic:
rw [comp_assoc]

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.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
⊢ {y | x = y + y⁻¹ ∨ y = 0}.Finite

Tactic:
convert! (φ.roots ∪ {0}).toFinset.finite_toSet using 1
        ext1 y
        simp only [φ, Multiset.mem_toFinset, Set.mem_ofPred_eq, Finset.mem_coe, Multiset.mem_union,
          mem_roots hφ, IsRoot, eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one,
          Multiset.mem_singleton]
        by_cases hy : y = 0
        · simp only [hy, or_true]
        apply or_congr _ Iff.rfl
        rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel₀ hy]
        apply eq_iff_eq_cancel_right.mpr
        ring

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

Goal state before:
pp: case pn
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ (match d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * (-1) ^ rootMultiplicity 1 p).support,
          (q * (-1) ^ rootMultiplicity 1 p).coeff i • preHilbertPoly F d i).natDegree ≤
    d - rootMultiplicity 1 p - 1

Tactic:
apply natDegree_sum_le_of_forall_le _ _ <| fun _ _ => ?_
    apply le_trans (natDegree_smul_le _ _)
    rw [natDegree_preHilbertPoly]

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

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0

Tactic:
by rwa [key, left_eq_add] at h1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this : C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2)
h1 : C a * (X - C x1) ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}

Tactic:
have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this : C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2)
h1 : C a * (X - C x1) ≠ 0
h2 : C a * (X - C x1) * (X - C x2) ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = f.toFun' S (1 ⊗ₜ[R] x)

Tactic:
by
  rw [ground_apply]
  convert! f.isCompat_apply' (Algebra.algHom R R S) (1 ⊗ₜ[R] x)
  · simp only [includeRight_lid]
  · rw [rTensor_tmul, toLinearMap_apply, map_one]

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
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
⊢ H.mod f = H.mod f'

Tactic:
obtain ⟨hf'1, hf'2⟩ := H.isWeierstrassDivisionAt_div_mod f'

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
hf'1 : (H.mod f').degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf'2 : f' = g * H.div f' + ↑(H.mod f')
⊢ H.mod f = H.mod f'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f = g * (f /ʷ g) + ↑(f %ʷ g)

Tactic:
simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]
  exact ((IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f).2

Goal state after:
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
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
e : Shrink.{v, u} (R ⧸ Ideal.ofList rs) ≃ₗ[R] Shrink.{v, u} R ⧸ Ideal.ofList rs • ⊤ :=
  Shrink.linearEquiv R (R ⧸ Ideal.ofList rs) ≪≫ₗ
    Submodule.Quotient.equiv (Ideal.ofList rs) (Ideal.ofList rs • ⊤) (Shrink.linearEquiv R R).symm ⋯
⊢ projectiveDimension (of R (Shrink.{v, u} R)) + ↑rs.length = ↑rs.length

Tactic:
ModuleCat.projectiveDimension_eq_zero_of_projective,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
e : Shrink.{v, u} (R ⧸ Ideal.ofList rs) ≃ₗ[R] Shrink.{v, u} R ⧸ Ideal.ofList rs • ⊤ :=
  Shrink.linearEquiv R (R ⧸ Ideal.ofList rs) ≪≫ₗ
    Submodule.Quotient.equiv (Ideal.ofList rs) (Ideal.ofList rs • ⊤) (Shrink.linearEquiv R R).symm ⋯
⊢ 0 + ↑rs.length = ↑rs.length
Module: Mathlib.RingTheory.SimpleRing.Congr

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

Tactic:
orderIsoRingCon.toEquiv.nontrivial_congr,

Goal state after:
R : Type u_1
inst✝ : Ring R
e : TwoSidedIdeal R ≃o { I // I.IsTwoSided } := orderIsoIsTwoSided
⊢ (Nontrivial (RingCon R) ∧ ∀ (a : TwoSidedIdeal R), a = ⊥ ∨ a = ⊤) ↔
    Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
h : m ∈ isotypicComponents R M
⊢ ⊥ < m

Tactic:
by
  obtain ⟨_, _, rfl⟩ := h; exact bot_lt_isotypicComponent ..

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯

Tactic:
by
  have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [Algebra.smul_def, h]))
  have H' := (a • g).isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
  have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])
  exact (H'.elim (H.smul (by simpa using ha))).2

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | IsClosed {x}}

Tactic:
simp only [isClosed_singleton_iff_isMaximal]

Goal state after:
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | x.asIdeal.IsMaximal}
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
x✝ : S
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((↑e.symm).comp ↑e2.symm).comp (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
simp [e, e2]

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

Goal state before:
pp: K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
heq :
  Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
    ((↑e.symm).comp ↑e2.symm).comp (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))
⊢ IsHomeomorph (comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)

Tactic:
rw [heq]

Goal state after:
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
heq :
  Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
    ((↑e.symm).comp ↑e2.symm).comp (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))
⊢ IsHomeomorph
    (comap (((↑e.symm).comp ↑e2.symm).comp (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))).toRingHom)
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I ^ 2 = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker

Tactic:
by
  rw [pow_two] at sq
  have {x : R} (h : x ∈ I * J) : f (J.toCotangent ⟨x, Ideal.mul_le_right h⟩) = 0 := by
    induction h using Submodule.mul_induction_on' with
    | mem_mul_mem y hy z hz =>
      rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_right (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
    | add y ymem z zmem hy hz =>
      have : (⟨y + z, Ideal.mul_le_right (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_right ymem⟩ + ⟨z, Ideal.mul_le_right zmem⟩ := rfl
      rw [this, map_add, map_add, hy, hz, add_zero]
  intro x hx
  rcases Submodule.mem_map.mp hx with ⟨x', hx', eq⟩
  simpa [← eq] using this hx'

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬coeff ⟨i, hin⟩ ((WittVector.truncate n) (↑p ^ i)) = coeff ⟨i, hin⟩ 0

Tactic:
rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬1 = 0
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp (truncate n) =
    (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m)

Tactic:
RingHom.comp_assoc,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (zmodEquivTrunc p m).symm.toRingHom.comp ((TruncatedWittVector.truncate h).comp (truncate n)) =
    (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m)
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ ((zmodEquivTrunc p k₁).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k₁)))).comp (PadicInt.toZModPow k₂) =
    (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)

Tactic:
RingHom.comp_assoc,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ (zmodEquivTrunc p k₁).toRingHom.comp ((ZMod.castHom ⋯ (ZMod (p ^ k₁))).comp (PadicInt.toZModPow k₂)) =
    (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)).comp
      (lift (fun k ↦ (zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) ⋯) =
    PadicInt.toZModPow n

Tactic:
RingHom.comp_assoc,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (zmodEquivTrunc p n).symm.toRingHom.comp
      ((truncate n).comp (lift (fun k ↦ (zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) ⋯)) =
    PadicInt.toZModPow n
Module: Mathlib.RingTheory.WittVector.MulCoeff

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

Tactic:
sum_range_succ,

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