mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ ⊤.IsPrincipal

Tactic:
by
  rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
v : V
n : f v ≠ 0 v
c : K
⊢ (↑K f) (c • v) = c • f v

Tactic:
by simp

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

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + 0))

Tactic:
by simp

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

Goal state before:
pp: case neg
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
hk : ¬k = 0
⊢ Commute (f ((C a).coeff k)) x

Tactic:
simp only [coeff_C_of_ne_zero hk, map_zero, Commute.zero_left]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
k : ℕ
ih : eval x (p * X ^ k) = eval x p * x ^ k
⊢ eval x (p * X ^ (k + 1)) = eval x p * x ^ (k + 1)

Tactic:
| succ k ih =>

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

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

Tactic:
| succ k ih =>

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

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

Tactic:
| succ k ih =>

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * X + p * ↑n).comp q = p.comp q * (q + ↑n)

Tactic:
add_comp,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * X).comp q + (p * ↑n).comp q = p.comp q * (q + ↑n)
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
⊢ (single x r * f).coeff.support = image (fun x_1 ↦ x * x_1) f.coeff.support

Tactic:
refine subset_antisymm (support_coeff_single_mul_subset f _ _) fun y hy => ?_
  obtain ⟨y, yf, rfl⟩ : ∃ a ∈ f.coeff.support, x * a = y := by grind
  simp [coeff_mul, mem_support_iff.mp yf, hr, lx.eq_iff]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (a : R), map f ((C a).comp q) = (map f (C a)).comp (map f q)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S✝
inst✝⁶ : Ring T
σ : R →+* S✝
τ : S✝ →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S✝ F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
S : Submodule R E
⊢ S ⊓ f.domain ≤ f.domain

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S✝
σ : R →+* S✝
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S✝ F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ S ⊓ f.domain ≤ f.domain

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S✝
σ : R →+* S✝
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S✝ F
f : E →ₛₗ.[σ] F
S : Submodule R E
⊢ (f.domRestrict S).domain ≤ f.domain

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : ↥f.domain
⊢ (↑x, ↑f x) ∈ f.graph

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n m✝ : ℕ
n1 : n = 1
m2 : 2 ≤ m✝
x✝ : m✝ ∣ n
⊢ minFac 1 ≤ 2

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : Nat.find ⋯ ∣ x
⊢ ↑x = 0

Tactic:
← Nat.mul_div_cancel' H1,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : Nat.find ⋯ ∣ x
⊢ ↑(Nat.find ⋯ * (x / Nat.find ⋯)) = 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ r = 1 * r

Tactic:
rw [one_mul]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
⊢ n.minFac = 2

Tactic:
have lb := minFac_pos n

Goal state after:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
⊢ n.minFac = 2
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
k : ℕ
h : NeZero ↑k
⊢ ¬p ∣ k

Tactic:
by
  rwa [← CharP.cast_eq_zero_iff R p k, ← Ne, ← neZero_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ (0, y₁ - y₂).1 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Monoid M
m : M
r : R
⊢ single m r = (algebraMap R R[M]) r * (of R M) m

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
m : M
r : R
⊢ single m ((algebraMap R A) r) = (algebraMap R A[M]) r * (of A M) m

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Subsingleton M
r : R
⊢ (uniqueRingEquiv M).toFun ((algebraMap R A[M]) r) = (algebraMap R A) r

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
F : M →* A
m : M
⊢ ((lift R A M) F) ((of R M) m) = F m

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : M →* N
⊢ ∀ (r : R), (↑↑(mapDomainRingHom A f)).toFun ((algebraMap R A[M]) r) = (algebraMap R A[N]) r

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra R C
inst✝¹ : Monoid M
inst✝ : Monoid N
f : A →ₐ[R] B
⊢ ∀ (r : R), (↑↑(mapRingHom M ↑f)).toFun ((algebraMap R A[M]) r) = (algebraMap R B[M]) r

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
⊢ constantCoeff (C x) = x

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).coeff n = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
v v' : V
⊢ f (v + v') = f v + f v'

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (f ^ n).coeff.support.sup degb ≤ n • f.coeff.support.sup degb

Tactic:
rw [← List.prod_replicate, ← List.sum_replicate]

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.replicate n f).prod.coeff.support.sup degb ≤ (List.replicate n (f.coeff.support.sup degb)).sum
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (↑n).natDegree ≤ Zero.zero

Tactic:
by simp

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ ((monomial n) a).degree = ↑n

Tactic:
degree_monomial n ha

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ (↑n).natDegree ≤ Zero.zero

Tactic:
by simp

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n

Tactic:
rwa [degree_eq_natDegree hp, Nat.cast_lt]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s : Finset ι
f : ι → R[X]
⊢ (∑ i ∈ ∅, f i).degree ≤ ∅.sup fun b ↦ (f b).degree

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a b : ℕ), ↑(a + b) ≤ ↑a + ↑b

Tactic:
by simp

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.leadingCoeff ^ Nat.zero ≠ 0 → (p ^ Nat.zero).leadingCoeff = p.leadingCoeff ^ Nat.zero

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = X + C (p.coeff 0)

Tactic:
← one_mul X,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = 1 * X + C (p.coeff 0)
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ 0 ∉ p.support → (fun e a ↦ a * 0 ^ e) 0 (p.coeff 0) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ leadingCoeff 1 = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ (fun i ↦ eval₂ f x ((monomial i) (p.coeff i))) = fun i ↦ f (p.coeff i) * x ^ i

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q p) = eval₂ f (eval₂ f x q) p

Tactic:
p.as_sum_range

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))) =
    eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ i ∈ antidiagonal n, f i.1 i.2 = f ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i).2 ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i).1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f y ∈ Set.range (embDomain f)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r : R[X]
f : A →ₐ[R] B
⊢ ∀ (r : R), (↑↑(mapRingHom f.toRingHom)).toFun ((algebraMap R A[X]) r) = (algebraMap R B[X]) r

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g₁ g₂ : ι →₀ α
h : g₁ ≤ g₂
⊢ ∀ i ∈ g₁.support ∪ g₂.support, single (f i) 0 = 0

Tactic:
by simp

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
n : ℕ
a : A
⊢ (mapAlgHom f) ((monomial n) a) = (monomial n) (f a)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r : R[X]
f : A ≃ₐ[R] B
⊢ (mapAlgHom ↑f).comp (mapAlgHom ↑f.symm) = AlgHom.id R B[X]

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r : R[X]
f : A ≃ₐ[R] B
⊢ (mapAlgHom ↑f.symm).comp (mapAlgHom ↑f) = AlgHom.id R A[X]

Tactic:
by simp

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

Goal state before:
pp: R : Type u
B : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring B
inst✝ : Algebra R B
P : R[X]
b : B
⊢ eval b (map (algebraMap R B) P) = (aeval b) P

Tactic:
rw [aeval_def, eval_map]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
i : ι
x : α
f : ι →₀ α
⊢ (∀ i_1 ∈ {i}, (single i x) i_1 ≤ f i_1) ↔ x ≤ f i

Tactic:
by simp

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
t : R
⊢ (X + C t).comp (X - C t) = X

Tactic:
by simp

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
t : R
⊢ (X - C t).comp (X + C t) = X

Tactic:
by simp

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R✝
n : ℕ
inst✝⁶ : CommSemiring R✝
inst✝⁵ : Semiring A
inst✝⁴ : CommSemiring A'
inst✝³ : Semiring B
inst✝² : Algebra R✝ A
inst✝¹ : Algebra R✝ B
p q : R✝[X]
x : A
R : Type u_3
inst✝ : CommRing R
⊢ (-X).comp (-X) = X

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ (x : ι), x ∈ {i | a i ≠ b i} → ¬x < i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ toLex a j = toLex b j

Tactic:
contrapose! hl
    exact ⟨j, hl, hj⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ (∀ i_1 ∈ {i}, (single i a) i_1 ≤ f i_1) ↔ a ≤ f i

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ (l, m) ∉ antidiagonal (l + m) → P.coeff (l, m).1 * Q.coeff (l, m).2 = 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₁
g : σ → S₁
n : σ
⊢ eval₂ f g (X n) = g n

Tactic:
simp [eval₂_monomial, f.map_one, X, prod_single_index, pow_one]

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

Goal state before:
pp: R : Type u
σ : Type u_1
a a' : R
inst✝ : CommSemiring R
⊢ C (a + a') = C a + C a'

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
a : R
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ (eval₂ f g p * f a * Finsupp.prod 0 fun n e ↦ g n ^ e) = eval₂ f g p * f a

Tactic:
by simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), y * 1 = 0 ↔ y = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), 1 * y = 0 ↔ y = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ 0 ∈ support 1 ∧ coeff 0 1 = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
r : R
⊢ (C r).coeffs = if r = 0 then ∅ else {r}

Tactic:
classical
  aesop (add simp mem_coeffs_iff)

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
⊢ ∀ (a : MvPolynomial σ R), (renameEquiv R (Equiv.refl σ)) a = AlgEquiv.refl a

Tactic:
by 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
⊢ coeff 0 1 = 1

Tactic:
by 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✝
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M N : Submodule R S
p : MvPolynomial σ S
s : σ
i : σ →₀ ℕ
x : S
n : ℕ
⊢ 0 ∈ {p | ∀ (i : σ →₀ ℕ), coeff i p ∈ M}

Tactic:
by simp

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

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : 1 ≠ 0
M : Submodule R S
⊢ coeffsIn σ (M ^ 1) = coeffsIn σ M ^ 1

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₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ Finset.image (⇑f) ((monomial a) s).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs ∪ Finset.image (⇑f) p.coeffs

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₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ Finset.image (⇑f) p.coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs ∪ Finset.image (⇑f) p.coeffs

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₁
p : MvPolynomial σ R
⊢ ↑((map f) p).coeffs ⊆ ⇑f '' ↑p.coeffs

Tactic:
by
  classical
  exact mod_cast coeffs_map f p

Goal state after: