mathlib-initiative/mathlib-tactics huggingface dataset:
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 g : E →ₛₗ.[σ] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y

Tactic:
have hy : y = 0 := Subtype.ext (h y (hxy ▸ x.2) y.2)

Goal state after:
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 g : E →ₛₗ.[σ] F
h : ∀ x ∈ f.domain, x ∈ g.domain → x = 0
x : ↥f.domain
y : ↥g.domain
hxy : ↑x = ↑y
hy : y = 0
⊢ ↑f x = ↑g y
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
of : X → ↥s := Subtype.coind (ι R) grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
this : a = ↑(((lift R) of) a)
⊢ motive a

Tactic:
rw [this]
    exact Subtype.prop (lift R of a)

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

Goal state before:
pp: p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = m * 1

Tactic:
mul_one

Goal state after:
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = m
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
hab : a = a * b
⊢ a = a * 1

Tactic:
mul_one

Goal state after:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
hab : a = a * b
⊢ a = a
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac * 1
⊢ n.minFac ≤ n / n.minFac

Tactic:
mul_one

Goal state after:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ q = 1

Tactic:
· exact False.elim <| hq_prime.ne_zero <| ‹CharP R q›.eq R hp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hq : ExpChar R 1
⊢ CharZero R

Tactic:
cases hq
  · assumption
  · exact False.elim (CharP.char_ne_one R 1 rfl)

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 : A →ₐ[R] B
g : M →* B
h_comm : ∀ (x : A) (y : M), Commute (f x) (g y)
⊢ ∀ (r : R), (↑↑(liftNCRingHom (↑f) g h_comm)).toFun ((algebraMap R A[M]) r) = (algebraMap R B) r

Tactic:
simp [liftNCRingHom]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ p.coeff (d, n).1 * 1 = p.coeff d

pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ p.coeff (d, n).1 = p.coeff d

case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0
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✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
g : Multiplicative M →* B
h_comm : ∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)
⊢ ∀ (r : R), (↑↑(liftNCRingHom (↑f) g h_comm)).toFun ((algebraMap R A[M]) r) = (algebraMap R B) r

Tactic:
simp [liftNCRingHom]

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

Goal state before:
pp: case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)

Tactic:
intro i s his ih

Goal state after:
case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s✝ : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
his : i ∉ s
ih : supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
⊢ supDegree D (∏ i ∈ insert i s, f i) ≤ ∑ i ∈ insert i s, supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
exact h₁.trans h₂.symm

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
· rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * 1 = p.leadingCoeff

pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff = p.leadingCoeff

R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * 1 ≠ 0

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hmem
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).coeff.support

Tactic:
Finsupp.mem_support_iff,

Goal state after:
case hmem
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hmax
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q

Tactic:
· have := addLeftMono_of_addLeftStrictMono B
    have := addRightMono_of_addRightStrictMono B
    exact fun a ha => (Finset.le_sup ha).trans (supDegree_mul_le hadd)

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

Goal state before:
pp: case inr.inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q

Tactic:
← coeff_supDegree_add_supDegree hD hadd,

Goal state after:
case inr.inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D (p * q) = (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q))
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
⊢ leadingCoeff D p * 1 = leadingCoeff D p

Tactic:
mul_one

Goal state after:
case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
⊢ leadingCoeff D p = leadingCoeff D p
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support

Tactic:
exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ eval (1 + y) ((monomial d) ↑d.succ) - eval y ((monomial d) ↑d.succ) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
eval_monomial,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * (1 + y) ^ d - eval y ((monomial d) ↑d.succ) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * (1 + y) ^ d - eval y ((monomial d) ↑d.succ) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
eval_monomial,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * (1 + y) ^ d - ↑d.succ * y ^ d = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
y : A := ↑a
this : y ∈ R[x]
h : y = ↑a
⊢ ∃ p, (aeval x) p = y

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval] at this

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
y : A := ↑a
this : y ∈ (aeval x).range
h : y = ↑a
⊢ ∃ p, (aeval x) p = y
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ p.coeff n * r ^ n = p.coeff n * r ^ n

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)
⊢ eval₂ f t (p.comp^[k + 1] q) = (fun x ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)

Tactic:
rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ f (eval r p) = f 0

Tactic:
rw [← eval₂_hom, h, f.map_zero]

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

Goal state before:
pp: case inl
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
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ P.coeff i * Q.coeff j = 0

Tactic:
have hj : m < j := by lia
    rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]

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₁
a : R
⊢ f a * 1 = f a

Tactic:
mul_one

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ f a = f a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = C a * 1

Tactic:
mul_one

Goal state after:
R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = C a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (s + Finsupp.single n e)) a = (monomial (s + Finsupp.single n e)) (a * 1)

Tactic:
mul_one

Goal state after:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (s + Finsupp.single n e)) a = (monomial (s + Finsupp.single n e)) a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
⊢ (monomial (∑ i ∈ s, f i)) a = (monomial (∑ i ∈ s, f i)) (a * 1)

Tactic:
mul_one

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
⊢ (monomial (∑ i ∈ s, f i)) a = (monomial (∑ i ∈ s, f i)) a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ ∏ x ∈ s, (monomial (f x)) (g x * 1) = ∏ i ∈ s, (monomial (f i)) (g i)

Tactic:
mul_one

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : i ∉ (Finsupp.indicator t fun i x_1 ↦ x i).support
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1

Tactic:
Finsupp.mem_support_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : ¬(Finsupp.indicator t fun i x_1 ↦ x i) i ≠ 0
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ C X (C a) = C a

Tactic:
simp +contextual [eval₂_add, eval₂_mul]

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

Goal state before:
pp: case add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R), eval₂ C X p = p → eval₂ C X q = q → eval₂ C X (p + q) = p + q

Tactic:
simp +contextual [eval₂_add, eval₂_mul]

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

Goal state before:
pp: case mul_X
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), eval₂ C X p = p → eval₂ C X (p * X n) = p * X n

Tactic:
simp +contextual [eval₂_add, eval₂_mul]

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

Goal state before:
pp: case e_a.e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ coeff C p ≠ 0

Tactic:
rwa [Finsupp.mem_support_iff] at hc

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
Finsupp.mem_support_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if m s ≠ 0 then coeff (m - Finsupp.single s 1) p else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if m s ≠ 0 then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if m s ≠ 0 then coeff (m - Finsupp.single s 1) p else 0

Tactic:
mul_one

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
Finsupp.mem_support_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if m s ≠ 0 then coeff (m - Finsupp.single s 1) p else 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ s q, p = (rename Subtype.val) q

Tactic:
apply induction_on p
  · intro r
    exact ⟨∅, C r, by rw [rename_C]⟩
  · rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
    refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q <;>
        simp +contextual only [id, true_or, or_true,
          Finset.mem_union, forall_true_iff]
    · simp only [rename_rename, map_add]
      rfl
  · rintro p n ⟨s, p, rfl⟩
    refine ⟨insert n s, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
      simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]
    · simp only [rename_rename, rename_X, map_mul]
      rfl

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q, p = (rename f) q

Tactic:
by
  obtain ⟨s, q, rfl⟩ := exists_finset_rename p
  let n := Fintype.card { x // x ∈ s }
  let e := Fintype.equivFin { x // x ∈ s }
  refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩
  rw [← rename_rename, rename_rename e]
  simp only [Function.comp_def, Equiv.symm_apply_apply, rename_rename]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (∑ i ∈ t, φ i).vars ⊆ t.biUnion fun i ↦ (φ i).vars

Tactic:
by
  classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ coeff s p * 1 ≠ 0

Tactic:
mul_one

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ coeff s p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
⊢ degreeOf i (p * 1) = degreeOf i p

Tactic:
mul_one

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
⊢ degreeOf i p = degreeOf i p
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ f (coeff 0 p) * 1 = f (constantCoeff p)

Tactic:
mul_one

Goal state after:
case neg
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ f (coeff 0 p) = f (constantCoeff p)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty

Tactic:
rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ ¬d = 0