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

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • v₀ = v

Tactic:
obtain ⟨r, hr⟩ := h ⟨v, hv⟩
    exact ⟨r, by rwa [Subtype.ext_iff, coe_smul] at hr⟩

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

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : finrank K ↥S = 1
T : Submodule K V
hT : T < S
this✝ : FiniteDimensional K ↥S
this : FiniteDimensional K ↥T
h : ¬finrank K ↥T = 0
⊢ False

Tactic:
exact hT.ne <| eq_of_le_of_finrank_le hT.le <| by lia

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
n : ℕ
⊢ eval x ↑n = ↑n

Tactic:
by simp only [← C_eq_natCast, eval_C]

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

Goal state before:
pp: n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
⊢ Prime n

Tactic:
refine prime_def_lt.mpr ⟨h1, fun m mlt mdvd => ?_⟩

Goal state after:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ ringExpChar R = q

Tactic:
rw [ringExpChar, ringChar.eq R q]

Goal state after:
case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ max q 1 = q
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 g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : x ∈ f.graph
⊢ x ∈ g.graph

Tactic:
rw [mem_graph_iff] at hx ⊢

Goal state after:
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 g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : ∃ y, ↑y = x.1 ∧ ↑f y = x.2
⊢ ∃ y, ↑y = x.1 ∧ ↑g y = x.2
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
h : IsMaxOn f s a
⊢ f a ∈ upperBounds (f '' s)

Tactic:
simpa [mem_upperBounds] using! h

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
inst✝ : Subsingleton M
a : A
⊢ (uniqueAlgEquiv R M).symm a = single 1 a

Tactic:
ext; simp [uniqueAlgEquiv]

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 ∈ g, x.1 = 0 → x.2 = 0
⊢ g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g

Tactic:
by
  rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]

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
f : R[M]
⊢ ((lift R A M) F) f = f.coeff.sum fun a b ↦ b • F a

Tactic:
by simp only [lift_apply', Algebra.smul_def]

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 (Ioc a b)
h₁ : AntitoneOn f (Ici b)
⊢ IsMaxOn f (Ioi a) b

Tactic:
by
  intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ ⟨hx, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx)) g₀
  · exact h₁ self_mem_Ici g₀.le g₀.le

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

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

Tactic:
simpa only [pow_one] using coeff_mul_X_pow p 1 n

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ degree 1 ≤ 0

Tactic:
rw [← C_1]

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ (C 1).degree ≤ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ q.coeff.support
hne : a ≠ aq
he : ap + a = ap + aq
⊢ False

Tactic:
apply_fun D at he

Goal state after:
case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ q.coeff.support
hne : a ≠ aq
he : D (ap + a) = D (ap + aq)
⊢ False
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ p.coeff.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.coeff.support
he : a + a' = ap + aq
⊢ False

Tactic:
apply_fun D at he

Goal state after:
case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ p.coeff.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.coeff.support
he : D (a + a') = D (ap + aq)
⊢ False
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 0 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 0

Tactic:
simp [← WithBot.coe_add]

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

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

Tactic:
by
    have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ', ← ih h₁] at h
    rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]

Goal state after:
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
h✝ : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
apply supDegree_mul hD hadd ?_ hp hq.ne_zero

Goal state after:
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
h✝ : Nontrivial R
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
h : X ^ n + C a = 1
⊢ n = 0

Tactic:
by simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h

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
⊢ ↑d.succ * (y + 1) ^ d - ↑d.succ * y ^ d = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
add_pow

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ m ∈ range (d + 1), y ^ m * 1 ^ (d - m) * ↑(d.choose m) - ↑d.succ * y ^ d =
    ∑ 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
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * ↑(d.choose y) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ (y + 1 - 1)

Tactic:
← Nat.cast_mul,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑(d.succ * d.choose y) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ (y + 1 - 1)
Module: Mathlib.Data.Finsupp.Antidiagonal

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

Tactic:
simp [add_comm]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
k : ℕ
sn : S ⊗[R] N
⊢ X ^ k • (rTensor N (↑R (monomial 0))) sn = (rTensor N (↑R (monomial k))) sn

Tactic:
induction sn using TensorProduct.induction_on with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | tmul s n =>
    simp only [rTensor_tmul, coe_restrictScalars, monomial_zero_left]
    rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]

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
i j : ℕ
⊢ i + j = l + m → (i = l → ¬j = m) → P.coeff i * Q.coeff j = 0

Tactic:
hij

Goal state after:
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
⊢ (i = l → ¬j = m) → P.coeff i * Q.coeff j = 0
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₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), k (eval₂ f g (C a)) = eval₂ k (⇑k ∘ g) ((map f) (C a))

Tactic:
intro r
    rw [eval₂_C, map_C, eval₂_C]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

Tactic:
constructor
  · rintro ⟨φ, rfl⟩ c
    rw [coeff_C_mul]
    apply dvd_mul_right
  · intro h
    choose C hc using h
    classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]

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

Goal state before:
pp: case pos
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
h : i ∈ range f
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))

Tactic:
simp [killCompl, h]

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

Goal state before:
pp: case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
h : i ∉ range f
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))

Tactic:
simp [killCompl, h]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
⊢ (∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q

Tactic:
have hor (n) (h : ¬coeff n p + coeff n q = 0) : coeff n p ≠ 0 ∨ coeff n q ≠ 0 := by
    by_cases hp : coeff n p = 0 <;> simp_all

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ (∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p + q).degrees ≤ p.degrees ⊔ q.degrees

Tactic:
by
  simp_rw [degrees_def]; exact supDegree_add_le

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₁
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m ((map f) (C a)) = f (coeff m (C a))

Tactic:
intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]

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

Goal state before:
pp: case refine_2.inr
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ∃ n_1, ¬coeff n_1 p + coeff n_1 q = 0 ∧ coeff n q = coeff n_1 p + coeff n_1 q

Tactic:
exact ⟨n, by simp [hr n hn, hn]⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : R
⊢ (constantCoeff.comp C) x = (RingHom.id R) x

Tactic:
exact constantCoeff_C σ x

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ p.degrees ≤ (p + q).degrees

Tactic:
apply Finset.sup_le

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ ∀ b ∈ p.support, toMultiset b ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Rename

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

Tactic:
by
  obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
  obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
  classical
    use s₁ ∪ s₂
    use rename (fun x ↦ ⟨x, Finset.subset_union_left x.2⟩) q₁
    use rename (fun x ↦ ⟨x, Finset.subset_union_right x.2⟩) q₂
    constructor <;> simp [Function.comp_def]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m ↦ m j) + 1 = f.support.sup fun m ↦ m j + 1
⊢ (f.support.sup fun m ↦ m j + 1) ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m ↦ m j

Tactic:
apply Finset.sup_le

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m ↦ m j) + 1 = f.support.sup fun m ↦ m j + 1
⊢ ∀ b ∈ f.support, b j + 1 ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m ↦ m j
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h✝ : degreeOf i p ≠ degreeOf i q
h : degreeOf i p < degreeOf i q
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)

Tactic:
simp [add_comm p q, degreeOf_add_eq_of_degreeOf_lt h, max_eq_right_of_lt h]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
classical
  rw [totalDegree_eq]
  exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
⊢ Multiset.toFinsupp.symm (a + b) = Multiset.toFinsupp.symm i

Tactic:
simp [a, b, Multiset.sub_add_inter]

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → τ
φ : MvPolynomial σ R
i : τ
hi : i ∈ ((rename f) φ).degrees
⊢ ∃ a ∈ φ.degrees, f a = i

Tactic:
simpa only [Multiset.mem_map] using degrees_rename _ _ hi

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.natTrailingDegree = q.natTrailingDegree

Tactic:
unfold natTrailingDegree
  rw [h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ 0 ≤ trailingDegree 1

Tactic:
rw [← C_1]

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ 0 ≤ (C 1).trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ', mul_assoc]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hq : q.natDegree ≠ 0
⊢ (p.comp q).leadingCoeff = (p.comp q).coeff (p.natDegree * q.natDegree)

Tactic:
← natDegree_comp,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hq : q.natDegree ≠ 0
⊢ (p.comp q).leadingCoeff = (p.comp q).coeff (p.comp q).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p.natDegree * q.natDegree = 0

Tactic:
← natDegree_comp,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ (p.comp q).natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = ↑p.natDegree * ↑q.natDegree

Tactic:
← Nat.cast_mul,

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = ↑(p.natDegree * q.natDegree)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse = 0 ↔ f = 0

Tactic:
by simp [reverse]

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

Goal state before:
pp: case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0

Tactic:
rw [← C_1]

Goal state after:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (C 1).nextCoeff = 0
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 : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a * (Multiset.map f t).prod).nextCoeff = (f a).nextCoeff + (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum

Tactic:
Monic.nextCoeff_mul,

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a).nextCoeff + (Multiset.map f t).prod.nextCoeff = (f a).nextCoeff + (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum

case refine_2.hp
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a).Monic

case refine_2.hq
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin (n + 1)
⊢ i < j →
    Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j

Tactic:
hij

Goal state after:
case succ.refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin (n + 1)
hij : i < j
⊢ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j