mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ⇑f '' ↑p.coeffs ⊆ range ⇑f

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hx : ↑(C 0).coeffs ⊆ range ⇑f
⊢ (map f) 0 = C 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
b : R
h : ¬f b = 0
⊢ (map f) (C b) = C (f b)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
n : σ
q : MvPolynomial σ R
ih : ↑((map f) q).coeffs ⊆ range ⇑f → (map f) q ∈ range ⇑(map f)
hx : ↑((map f) q).coeffs ⊆ range ⇑f
⊢ (map f) (q * X n) = (map f) q * X n

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
inst✝ : Algebra R S₁
g : σ → S₁
r : R
⊢ (↑↑(eval₂Hom (algebraMap R S₁) g)).toFun ((algebraMap R (MvPolynomial σ R)) r) = (algebraMap R S₁) r

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ (a1 a2 : σ →₀ ℕ), (a1 + a2) i = a1 i + a2 i

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: n : Fin 2 →₀ ℕ
⊢ ofSupportFinite ![n 0, n 1] ⋯ = n

Tactic:
by
  rw [Finsupp.ext_iff, Fin.forall_fin_two]
  exact ⟨rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c = 0
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x ↦ id

Tactic:
simp only [hc, map_zero, totalDegree_zero, zero_le]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))

Tactic:
rw [coeff_C]

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = if 0 = m then coeff 0 p else 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ ≃ τ
p : MvPolynomial σ R
⊢ p.totalDegree ≤ ((rename ⇑f.symm) ((rename ⇑f) p)).totalDegree

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
⊢ 0 ∈ {p | p.degrees ≤ s}

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ 1 ≤ degreesLE R σ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset σ
⊢ degreesLE R σ (0 • s) = degreesLE R σ s ^ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N : ℕ
⊢ (revAt N) 0 = N

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) (Polynomial.C n) * Polynomial.eval₂ C (X default) (Polynomial.X ^ (p + 1))) =
    Polynomial.C n * Polynomial.X ^ (p + 1)

Tactic:
Polynomial.eval₂_pow,

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) (Polynomial.C n) * Polynomial.eval₂ C (X default) Polynomial.X ^ (p + 1)) =
    Polynomial.C n * Polynomial.X ^ (p + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree

Tactic:
rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
by
  rw [natDegree_mul']
  simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
a : ι
⊢ ∀ (s : Multiset ι),
    ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) →
      (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic

Tactic:
t

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
⊢ ((∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic) →
    (∀ i ∈ a ::ₘ t, (f i).Monic) → (Multiset.map f (a ::ₘ t)).prod.Monic
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ (Multiset.map leadingCoeff t).prod ≠ 0

Tactic:
simp only [ne_eq]

Goal state after:
case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ ¬(Multiset.map leadingCoeff t).prod = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : (Multiset.map leadingCoeff t).prod ≠ 0
⊢ t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod

Tactic:
induction t using Multiset.induction_on with | empty => simp | cons a t ih => ?_
  simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢
  rw [Polynomial.leadingCoeff_mul']
  · rw [ih]
    simp only [ne_eq]
    apply right_ne_zero_of_mul h
  · rw [ih]
    · exact h
    simp only [ne_eq]
    apply right_ne_zero_of_mul h

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ x j ≠ 0

Tactic:
exact hx j

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
⊢ ∑ i ∈ range 1, x ^ i = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ∑ i ∈ range 0, 0 ^ i = if 0 = 0 then 0 else 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ∑ i ∈ range 1, 0 ^ i = if 1 = 0 then 0 else 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ ∑ i ∈ range n, 1 ^ i = ↑n

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Tactic:
have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n

Tactic:
pow_succ' y,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).natDegree = P.natDegree

Tactic:
refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = (X ^ n - C 1).natDegree

Tactic:
natDegree_X_pow_sub_C

Goal state after:
case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
this : k ≤ ↑n
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
rw [← C_mul_X_pow_eq_monomial, C_mul']

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
this : k ≤ ↑n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
i : Fin n
a : R
⊢ ↑↑i < ↑n

Tactic:
by simp

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
rw [← C_mul_X_pow_eq_monomial, C_mul']

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
x✝ : ↥(degreeLT R n)
p : R[X]
hp : p ∈ degreeLT R n
⊢ ∀ (i : ℕ), (monomial i) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ (degreeLTEquiv R n) ⟨p, hp⟩ = 0 ↔ p = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inl.inr
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ 1 * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
rw [one_mul]

Goal state after:
case inl.inr
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
x : A
⊢ ∀ (s : Finset A), x ∉ s → P (Algebra.adjoin R ↑s) → P (Algebra.adjoin R ↑(insert x s))

Tactic:
t

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
⊢ x ∉ t → P (Algebra.adjoin R ↑t) → P (Algebra.adjoin R ↑(insert x t))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
⊢ ∏ i ∈ ∅, (f i).leadingCoeff ≤ (∅.prod f).leadingCoeff

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: ι : Sort u_1
R : Type u_2
inst✝ : NonAssocRing R
S : Subring R
⊢ ∀ {x : Rᵐᵒᵖ}, x ∈ S.op.carrier → -x ∈ S.op.carrier

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: ι : Sort u_1
R : Type u_2
inst✝ : NonAssocRing R
S : Subring Rᵐᵒᵖ
⊢ ∀ {x : R}, x ∈ S.unop.carrier → -x ∈ S.unop.carrier

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x✝ : R
⊢ MulOpposite.op ((algebraMap R A) x✝) = MulOpposite.op (MulOpposite.unop x) ↔ MulOpposite.op ((algebraMap R A) x✝) = x

Tactic:
MulOpposite.op_unop

Goal state after:
case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x✝ : R
⊢ MulOpposite.op ((algebraMap R A) x✝) = x ↔ MulOpposite.op ((algebraMap R A) x✝) = x
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
t : Set A
h : t.Finite
⊢ adjoin R ↑h.toFinset = adjoin R t

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
⊢ n ∈ {n} ∪ Set.range nj

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule S * toSubmodule T ≤ toSubmodule (S ⊔ T)

Tactic:
by
  rw [Submodule.mul_le]
  intro y hy z hz
  simp only [mem_toSubmodule]
  exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝⁴ : AddCommMonoid M
x✝³ : Module R M
x✝² : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝¹ x : ↥N
hx : x = n
j : Fin k
x✝ : j ∈ Finset.univ
⊢ b j ∈ Set.range b ∪ Set.range (Function.uncurry c)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝⁴ : AddCommMonoid M
x✝³ : Module R M
x✝² : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝¹ x : ↥N
hx : x = n
j : Fin k
x✝ : j ∈ Finset.univ
b' : ↥A := ⟨b j, ⋯⟩
⊢ mj j ∈ Set.range mj

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j j' : Fin k
x✝ : j' ∈ Finset.univ
c' : ↥A := ⟨c j j', ⋯⟩
⊢ mj j' ∈ Set.range mj

Tactic:
by simp

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

Goal state before:
pp: case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ (∑ v ∈ p.support, (monomial v) (coeff v p)) = eval₂ (ϕ.comp C) (fun s ↦ ϕ (X s)) p

Tactic:
MvPolynomial.eval₂_eq',

Goal state after:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ (∑ v ∈ p.support, (monomial v) (coeff v p)) = ∑ d ∈ p.support, (ϕ.comp C) (coeff d p) * ∏ i, ϕ (X i) ^ d i
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ p.support
this : C (coeff m p) ∈ I
⊢ C (coeff m p) * (monomial m) 1 ∈ I

Tactic:
exact I.mul_mem_right (monomial m 1) this

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

Goal state before:
pp: case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
⊢ f ∈ Ideal.map C I

Tactic:
rw [as_sum f]

Goal state after:
case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
⊢ ∑ v ∈ f.support, (monomial v) (coeff v f) ∈ Ideal.map C I
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
⊢ (n • x + x) * y = n • x * y + x * y

Tactic:
add_mul

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ -((n + 1) • x) * y = -((n + 1) • (x * y))

Tactic:
neg_mul,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ -((n + 1) • x * y) = -((n + 1) • (x * y))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ : ↥M'
x : M
j : Fin k
⊢ nj j ∈ {n} ∪ Set.range nj

Tactic:
by simp

Goal state after: