mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
s : V
hs : s ∈ T
hz : s ≠ 0
⊢ v ∈ T

Tactic:
rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩

Goal state after:
case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
⊢ v ∈ T
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ toNat (Module.rank R M) = 0

Tactic:
rank_subsingleton',

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ toNat 0 = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_comm
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ : Pre R X
⊢ liftFun R X f (a✝ + b✝) = liftFun R X f (b✝ + a✝)

Tactic:
change _ + _ = _ + _

Goal state after:
case add_comm
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ = liftFun R X f b✝ + liftFun R X f a✝
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
⊢ p.comp (C a) = C (eval a p)

Tactic:
by simp [comp]

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

Goal state before:
pp: p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ), b < p → m * b ≠ p

Tactic:
Ne,

Goal state after:
p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ), b < p → ¬m * b = p
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
⊢ ↑(f.domRestrict S) x = ↑f y

Tactic:
have : Submodule.inclusion (by simp) x = y := by
    ext
    simp [h]

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 : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
this : (Submodule.inclusion ⋯) x = y
⊢ ↑(f.domRestrict S) x = ↑f y
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ n.sqrt + 2 - (a✝ + 2) < n.sqrt + 2 - a✝

Tactic:
simp_wf

Goal state after:
n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ n.sqrt - a✝ < n.sqrt + 2 - a✝
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 : E × F
⊢ x ∈ f.graph ↔ ∃ y, ↑y = x.1 ∧ ↑f y = x.2

Tactic:
by
  cases x
  simp_rw [mem_graph_iff', Prod.mk_inj]

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

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ↑2 ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ¬↑2 = 0
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬2 ≤ n ∨ ¬n.minFac = n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
← h1,

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
⊢ Nat.Prime q ∨ q = 1

Tactic:
cases hq with
  | zero => exact .inr rfl
  | prime hp => exact .inl hp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0 ∧ y ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ ¬x = 0 ∧ ¬y = 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ ¬x = 0 ∧ ¬y = 0 ∧ ¬z = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.leadingCoeff ≠ 0 ↔ p ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.leadingCoeff = 0 ↔ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n

Tactic:
· exact (coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
⊢ p.degree ≠ ⊥

Tactic:
Ne,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
⊢ ¬p.degree = ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
· rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.support ≠ ∅

Tactic:
Ne,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ¬p.support = ∅
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support.Nonempty ↔ ¬p = 0
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support ≠ ∅ ↔ ¬p = 0

Tactic:
Ne,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.support = ∅ ↔ ¬p = 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
hp : ¬p = 0
⊢ p.leadingCoeff ≠ 0

Tactic:
Ne,

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p ^ n).leadingCoeff ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬(p ^ n).leadingCoeff = 0
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
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n

Tactic:
ih h₁

Goal state after:
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
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ p.leadingCoeff * p.leadingCoeff ^ n = p.leadingCoeff * p.leadingCoeff ^ n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ n * p).degree = (n + 1) • p.degree

Tactic:
degree_mul' h₂,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ n).degree + p.degree = (n + 1) • p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ q.leadingCoeff ≠ 0

Tactic:
Ne,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ ¬q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a * p).degree = p.degree

Tactic:
degree_mul',

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).degree + p.degree = p.degree

R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (p * C a).degree = p.degree

Tactic:
degree_mul',

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.degree + (C a).degree = p.degree

R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C a).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ (↑u).leadingCoeff ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ ¬(↑u).leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : a ∣ p
h : a.degree ≤ 0
⊢ IsUnit a

Tactic:
Polynomial.eq_C_of_degree_le_zero h

Goal state after:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (C (a.coeff 0))
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ p = 1

Tactic:
eq_C_of_natDegree_eq_zero hfd,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ C (p.coeff 0) = 1
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: 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 ≠ 0

Tactic:
Ne,

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 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: 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
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ leadingCoeff D q ≠ 0

Tactic:
Ne,

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
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ ¬leadingCoeff D q = 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
i : ι
n : ℕ
⊢ ((RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i))
          { toFinsupp := ofCoeff (Finsupp.ofSupportFinite (fun n i ↦ (p i).coeff n) ⋯) } i).coeff
      n =
    (p i).coeff n

Tactic:
exact coeff_map _ _

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

Goal state before:
pp: case ha
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 ≠ 0

Tactic:
Ne,

Goal state after:
case ha
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 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
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 q ≠ 0

Tactic:
Ne,

Goal state after:
case hb
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 q = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Ring S
c : S
⊢ (X + -C c).nextCoeff = -c

Tactic:
← map_neg C c,

Goal state after:
S : Type v
inst✝ : Ring S
c : S
⊢ (X + C (-c)).nextCoeff = -c
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

pp: case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
· simp [hi]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i
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 * ∑ x ∈ range (d + 1), ↑(d.choose x) * y ^ x - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
rw [sum_range_succ, mul_add, Nat.choose_self, Nat.cast_one, one_mul, add_sub_cancel_right,
    mul_sum, sum_range_succ', Nat.cast_zero, zero_mul, mul_zero, add_zero]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ comapDomain (⇑f) u ⋯ + comapDomain (⇑f) v ⋯ = y

Tactic:
rw [← comapDomain_add_of_injective f.injective, h, comapDomain_embDomain]

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]
inst✝ : Nontrivial A
⊢ ⊥ ≠ ⊤

Tactic:
Ne,

Goal state after:
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]
inst✝ : Nontrivial A
⊢ ¬⊥ = ⊤
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ (single a (f a)).sum g ≤ f.sum g

Tactic:
rw [sum, support_single _ H, sum_singleton, single_eq_same]

Goal state after:
case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ g a (f a) ≤ f.sum g
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ toLex x < toLex (update x i a) ↔ x i < a

Tactic:
refine ⟨?_, fun h => toLex_strictMono <| lt_update_self_iff.2 h⟩

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ toLex x < toLex (update x i a) → x i < a
Module: Mathlib.Order.PiLex

Goal state before:
pp: case refine_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : j < i
⊢ a₂ j = Function.update a₂ i a j

Tactic:
rw [Function.update_of_ne hj.ne a]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: case refine_3
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ Function.update a₂ i a j = a₂ j

Tactic:
rw [Function.update_of_ne hj.ne a]

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₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
    eval₂ f g (C a * (monomial s) a_1) = eval₂ f g (C a) * f a_1 * s.prod fun n e ↦ g n ^ e

pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e

pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * X n) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
· intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
        ∀ {s : σ →₀ ℕ} {a : R},
          eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * X n) * f a * s.prod fun n e ↦ g n ^ e
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case hnc
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p ≠ 0 ↔ ∃ d, coeff d p ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ¬p = 0 ↔ ∃ d, coeff d p ≠ 0
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
⊢ (∃ 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 hr (n : σ →₀ ℕ) (hne : q.coeff n ≠ 0) : p.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_right_finset (mem_support_iff.mpr hne)

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
⊢ (∃ 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.Rename

Goal state before:
pp: case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : ¬↑u.support ⊆ range f
⊢ coeff s 0 = coeff (Finsupp.mapDomain f s) ((monomial u) r)

Tactic:
· simp? says simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]
      intro rfl
      contrapose! h
      apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support
      simp

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

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ coeff d q = 0

Tactic:
Ne,

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : ¬d = 0
⊢ coeff d q = 0