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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑((algebraMap S L).comp (algebraMap R S))

Tactic:
← IsScalarTower.algebraMap_eq,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑(algebraMap R L)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ (liftBaseChange A l).range ≤ Submodule.span A ↑l.range

pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ Submodule.span A ↑l.range ≤ (liftBaseChange A l).range

Tactic:
· rintro _ ⟨x, rfl⟩
    induction x using TensorProduct.induction_on
    · simp
    · rw [LinearMap.liftBaseChange_tmul]
      exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)
    · rw [map_add]
      exact add_mem ‹_› ‹_›

Goal state after:
case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ Submodule.span A ↑l.range ≤ (liftBaseChange A l).range
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
⊢ spectrum R (↑u * a * ↑u⁻¹) ⊆ spectrum R a

Tactic:
μ

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
⊢ μ ∈ spectrum R (↑u * a * ↑u⁻¹) → μ ∈ spectrum R a
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
this : Algebra R C := restrictScalars R S C
⊢ (LinearMap.mul S (A ⊗[R] B)).compr₂ f = (LinearMap.mul S C ∘ₗ f).compl₂ f

Tactic:
let : IsScalarTower R S C := .restrictScalars R S C

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
this✝ : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := IsScalarTower.restrictScalars R S C
⊢ (LinearMap.mul S (A ⊗[R] B)).compr₂ f = (LinearMap.mul S C ∘ₗ f).compl₂ f
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Field S
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : Module S A
inst✝ : Algebra R S
a : A
f : S → R
h : QuasispectrumRestricts a f
⊢ f 0 = 0

Tactic:
rw [← h.left_inv 0, map_zero (algebraMap R S)]

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr.inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
r✝¹ : R
a✝¹ : A
r✝ : R
a✝ : A
⊢ (algebraMap R C) r✝¹ + (algebraMap R C) r✝ + (φ a✝¹ + φ a✝) =
    (algebraMap R C) r✝¹ + φ a✝¹ + ((algebraMap R C) r✝ + φ a✝)

Tactic:
add_add_add_comm

Goal state after:
case inl_add_inr.inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
r✝¹ : R
a✝¹ : A
r✝ : R
a✝ : A
⊢ (algebraMap R C) r✝¹ + φ a✝¹ + ((algebraMap R C) r✝ + φ a✝) =
    (algebraMap R C) r✝¹ + φ a✝¹ + ((algebraMap R C) r✝ + φ a✝)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
x : M
hx : ∀ (a : R), a ≠ 0 → a • x ≠ 0
this : LinearIndependent R fun x_1 ↦ x
⊢ 1 ≤ Module.rank R M

Tactic:
simpa using this.cardinal_lift_le_rank

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : Module.rank R M = 0
⊢ Module.Finite R M

Tactic:
nontriviality R
  rw [rank_zero_iff] at h
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
this : ∀ (t : Set A), NonUnitalAlgebra.adjoin R (star t) ≤ star (NonUnitalAlgebra.adjoin R t)
⊢ star (NonUnitalAlgebra.adjoin R s) ≤ NonUnitalAlgebra.adjoin R (star s)

Tactic:
by simpa only [star_star] using NonUnitalSubalgebra.star_mono (this (star s))

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ⊆ ↑S

Tactic:
rw [← toNonUnitalSubalgebra_le_iff, adjoin_toNonUnitalSubalgebra,
    NonUnitalAlgebra.adjoin_le_iff, coe_toNonUnitalSubalgebra]

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ⊆ ↑S
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
⊢ (∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v) → Module.rank K V ≤ 1

Tactic:
rintro ⟨v₀, hv₀⟩
    have h : K ∙ v₀ = ⊤ := by
      ext
      simp [mem_span_singleton, hv₀]
    rw [← rank_top, ← h]
    refine (rank_span_le _).trans_eq ?_
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ↑⟨v, ⋯⟩ ≠ ↑0

Tactic:
simp [hv]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ liftAux R ((fun F ↦ ⇑F ∘ ι R) F) = F

Tactic:
ext t

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) t = F t
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a b : R
inst✝ : Ring R
⊢ eval b X - eval b (C a) = 0 ↔ a = b

Tactic:
eval_X,

Goal state after:
R : Type u
a b : R
inst✝ : Ring R
⊢ b - eval b (C a) = 0 ↔ a = b
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
by_cases h : n < k * k

Goal state after:
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n / n.minFac

Tactic:
congr
      rw [hx]

Goal state after:
case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n.minFac * (x + 2)

case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n.minFac
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).coeff 0 = p.coeff 0 * q.coeff 0

Tactic:
simp [coeff_mul]

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
⊢ IsMaxOn f (Iic a) b

Tactic:
intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ g₀ self_mem_Iic g₀
  · exact h₁ (left_mem_Icc.2 (g₀.le.trans hx)) ⟨g₀.le, hx⟩ g₀.le

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
⊢ p.degree ≤ q.degree

Tactic:
by
  by_cases hp : p = 0
  · rw [hp, degree_zero]
    exact bot_le
  · rw [degree_eq_natDegree hp]
    exact le_degree_of_ne_zero h

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = (C (p.coeff 0)).coeff (n + 1)

Tactic:
coeff_C,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = if n + 1 = 0 then p.coeff 0 else 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
⊢ max p.degree q.degree ≤ (p + q).degree

Tactic:
degree_add_eq_right_of_degree_lt hlt,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
⊢ max p.degree q.degree ≤ q.degree
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).degree = 2

Tactic:
by
  rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    degree_C_mul_X_pow 2 ha]
  rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ 1 + (C r).coeff n = 1

Tactic:
coeff_C,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (1 + if n = 0 then r else 0) = 1
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
j : ι
⊢ (single j (a - b)) j = (single j a - single j b) j

Tactic:
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
⊢ (aeval (f x)) X = (f.comp (aeval x)) X

Tactic:
simp only [aeval_X, AlgHom.comp_apply]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
| (aeval (ψ a)) (map φ p)

Tactic:
← eval_map_algebraMap

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
| eval (ψ a) (map (algebraMap T U) (map φ p))
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
⊢ aevalTower (Algebra.ofId S A') = aeval

Tactic:
by
  ext
  simp only [aeval_X, aevalTower_X]

Goal state after:
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
inst✝ : DecidableEq ι
j : ι
a b : α j
⊢ (single j (a - b)) j = (single j a - single j b) j

Tactic:
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ X.coeff 1 ∈ R⁰

Tactic:
simp [one_mem]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
h : m ≠ 0
a : R
⊢ coeff m (C a) = 0

Tactic:
coeff_C,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
h : m ≠ 0
a : R
⊢ (if 0 = m then a else 0) = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ coeffs 1 = {1}

Tactic:
by
  apply Finset.Subset.antisymm coeffs_one
  simp only [coeffs, Finset.singleton_subset_iff, Finset.mem_image]
  exact ⟨0, by simp⟩

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

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ f g ((rename k) (C a)) = eval₂ f (g ∘ k) (C a)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p →
      eval₂ f g ((rename k) q) = eval₂ f (g ∘ k) q → eval₂ f g ((rename k) (p + q)) = eval₂ f (g ∘ k) (p + q)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p → eval₂ f g ((rename k) (p * X n)) = eval₂ f (g ∘ k) (p * X n)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (a : R), (rename k) (eval₂ C (g ∘ k) (C a)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (C a))

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p) →
      (rename k) (eval₂ C (g ∘ k) q) = eval₂ C (⇑(rename k) ∘ g) ((rename k) q) →
        (rename k) (eval₂ C (g ∘ k) (p + q)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p + q))

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p) →
      (rename k) (eval₂ C (g ∘ k) (p * X n)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p * X n))

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ coeff m (C (f r)) = f (coeff m (C r))

Tactic:
coeff_C,

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ (if 0 = m then f r else 0) = f (if 0 = m then r else 0)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (a : R), (rename (Prod.mk j)) (eval₂ C g (C a)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (C a)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p →
      (rename (Prod.mk j)) (eval₂ C g q) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) q →
        (rename (Prod.mk j)) (eval₂ C g (p + q)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p + q)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p →
      (rename (Prod.mk j)) (eval₂ C g (p * X n)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p * X n)

Tactic:
· intros
      simp [*]

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

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
⊢ ∀ (x y : MvPolynomial σ R), coeff 0 (x * y) = coeff 0 x * coeff 0 y

Tactic:
simp [coeff_mul]

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

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (a : R), eval₂ f g ((rename (Prod.mk i)) (C a)) = eval₂ f (fun j ↦ g (i, j)) (C a)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p q : MvPolynomial τ R),
    eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun j ↦ g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i)) q) = eval₂ f (fun j ↦ g (i, j)) q →
        eval₂ f g ((rename (Prod.mk i)) (p + q)) = eval₂ f (fun j ↦ g (i, j)) (p + q)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p : MvPolynomial τ R) (n : τ),
    eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun j ↦ g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i)) (p * X n)) = eval₂ f (fun j ↦ g (i, j)) (p * X n)

Tactic:
· intros
      simp [*]

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

Goal state before:
pp: case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ((rename (Subtype.map id ⋯)) p * X ⟨n, ⋯⟩)

Tactic:
simp only [rename_rename, rename_X, map_mul]
      rfl

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

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p ∈ M

Tactic:
convert! M.zero_mem

Goal state after:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ (map q) φ = 0

Tactic:
C_dvd_iff_dvd_coeff,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔ (map q) φ = 0