mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker

pp: case insert.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Commute (f i) (s.noncommProd f ⋯)

pp: case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Disjoint (f i).ker (s.noncommProd f ⋯).ker

Tactic:
· simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]

Goal state after:
case insert.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Commute (f i) (s.noncommProd f ⋯)

case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Disjoint (f i).ker (s.noncommProd f ⋯).ker
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ finrank F ↥S = 1 ↔ S = ⊥

Tactic:
by
  rw [← Subalgebra.rank_eq_one_iff]
  exact toNat_eq_iff one_ne_zero

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ 0 • Quot.mk (Rel R X) a✝ = 0

Tactic:
change Quot.mk _ (_ * _) = _

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) 0) * a✝) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case zero
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x ↑0 = ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (p * X ^ 0) = eval x p * x ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (X ^ 0).comp p = p ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p r : R[X]
⊢ (p * X ^ 0).comp r = p.comp r * r ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ eval₂ (algebraMap R S) x (p ^ 0) = eval₂ (algebraMap R S) x p ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1

pp: case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

pp: case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
· omega

Goal state after:
case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ Nat.Prime 1 ∨ 1 = 1

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : ExpChar R q
⊢ 0 < q

Tactic:
rcases expChar_is_prime_or_one R q with h | rfl

Goal state after:
case inl
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
inst✝ : ExpChar R q
h : Nat.Prime q
⊢ 0 < q

case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : ExpChar R 1
⊢ 0 < 1
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case zero
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
⊢ φ₁ 0 = φ₂ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Monoid M
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : M →* A
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) 0) = ((lift R A M) f) 0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
⊢ (r • p).support ⊆ p.support

Tactic:
by
  intro i hi
  rw [mem_support_iff] at hi ⊢
  contrapose hi
  simp [hi]

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

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddMonoid M
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f : Multiplicative M →* A
⊢ ((lift S A M) f) ((mapRingHom M (algebraMap R S)) 0) = ((lift R A M) f) 0

Tactic:
| zero =>

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

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

Tactic:
simpa only [degree, ← support_toFinsupp, toFinsupp_add]
    using! AddMonoidAlgebra.sup_support_coeff_add_le _ _ _

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

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

Tactic:
rw [leadingCoeff_eq_zero, degree_eq_bot]

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

Goal state before:
pp: case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

Tactic:
intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h

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

Goal state before:
pp: case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

Tactic:
intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h

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
⊢ AddMonoidAlgebra.supDegree (WithBot.some ∘ id) p.toFinsupp = ↑p.natDegree

pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.coeff.support.Nonempty

Tactic:
Function.comp_id,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ AddMonoidAlgebra.supDegree WithBot.some p.toFinsupp = ↑p.natDegree

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.coeff.support.Nonempty
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
⊢ (p ^ 0).degree ≤ ↑0 * a

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
by_cases H : natDegree p < i

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p ^ 0).natDegree ≤ 0 * p.natDegree

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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✝⁶ : 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
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
obtain rfl | hp := eq_or_ne p 0
  · simp
  obtain rfl | hq := eq_or_ne q 0
  · simp
  obtain ⟨ap, -, hp⟩ := exists_supDegree_mem_support D hp
  obtain ⟨aq, -, hq⟩ := exists_supDegree_mem_support D hq
  simp_rw [leadingCoeff, hp, hq, ← hadd, Function.leftInverse_invFun hD _]
  exact coeff_add_of_supDegree_le hadd hD hp.le hq.le

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

Tactic:
rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]
  · rw [mem_antidiagonal]
  rintro ⟨df', dg'⟩ hmem hne
  obtain h | hdf' := lt_or_ge df df'
  · rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]
  obtain h | hdg' := lt_or_ge dg dg'
  · rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]
  obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
  exact (hne rfl).elim

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

Goal state before:
pp: case zero
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D (p ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D (p ^ 0) = 0 • supDegree D p

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

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
x✝¹ x✝ : ↥R[x]
p : A
hp : p ∈ R[x]
q : A
hq : q ∈ R[x]
⊢ ⟨p, hp⟩ * ⟨q, hq⟩ = ⟨q, hq⟩ * ⟨p, hp⟩

Tactic:
obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp
      obtain ⟨q', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hq
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MulMemClass.mk_mul_mk, ← map_mul,
        mul_comm p' q']

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ ↑p.natDegree ≤ (map f p).degree

Tactic:
refine le_degree_of_ne_zero ?_

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ (map f p).coeff p.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
⊢ image (Prod.map (embDomain f) (embDomain f)) (antidiagonal y) = antidiagonal (embDomain f y)

Tactic:
by
  ext ⟨u, v⟩
  simp only [mem_image, mem_antidiagonal, Prod.exists, Prod.map_apply,
    Prod.mk.injEq]
  refine ⟨fun ⟨w, z, h, hw, hz⟩ ↦ ?_, fun h ↦ ⟨u.comapDomain f f.injective.injOn,
    ⟨v.comapDomain f f.injective.injOn, ?_, ?_, ?_⟩⟩⟩
  · rw [← hw, ← hz, ← embDomain_add, h]
  · rw [← comapDomain_add_of_injective f.injective, h, comapDomain_embDomain]
  · rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add.mpr ⟨v, h.symm⟩) (by simp)))]
  · rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add'.mpr ⟨u, h.symm⟩) (by simp)))]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ single i a ≤ 0 ↔ a ≤ 0

Tactic:
classical exact Pi.single_nonpos

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

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

Tactic:
tsub_apply,

Goal state after:
case inl
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
j : ι
⊢ (single j (a - b)) j = (single j a) j - (single j b) j
Module: Mathlib.Data.Finsupp.Order

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

Tactic:
tsub_apply,

Goal state after:
case inr
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
⊢ (single i (a - b)) j = (single i a) j - (single i b) j
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case zero
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 : ℕ
⊢ X ^ k • (rTensor N (↑R (monomial 0))) 0 = (rTensor N (↑R (monomial k))) 0

Tactic:
| zero =>

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

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

Tactic:
tsub_apply,

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

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

Tactic:
tsub_apply,

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : j ≠ i
⊢ (single i (a - b)) j = (single i a) j - (single i b) j
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p) a)
⊢ motive ((monomial p) a * X n ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e✝ : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e✝ ≠ 0
ih : motive ((monomial p) a)
e : ℕ
⊢ motive ((monomial p) a * X n ^ e)

Tactic:
induction e with

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
hp : p ∈ ⊤
⊢ p ∈ S

Tactic:
clear hp

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
⊢ p ∈ S
Module: Mathlib.Data.Finsupp.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ StrictAnti fun a ↦ toLex (single a 1)

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ ∀ ⦃b : α⦄, a < b → (fun a ↦ toLex (single a 1)) b < (fun a ↦ toLex (single a 1)) a
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ Monotone ⇑toLex

Tactic:
intro a

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a : Π₀ (i : ι), α i
⊢ ∀ ⦃b : Π₀ (i : ι), α i⦄, a ≤ b → toLex a ≤ toLex b
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d ((rename f) φ) ≠ 0 ∧ i ∈ d.support) → i ∈ Multiset.map f φ.degrees

Tactic:
Multiset.mem_map

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d ((rename f) φ) ≠ 0 ∧ i ∈ d.support) → ∃ a ∈ φ.degrees, f a = i
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), constantCoeff ((rename f) (C a)) = constantCoeff (C a)

Tactic:
intro a

Goal state after:
case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ constantCoeff ((rename f) (C a)) = constantCoeff (C a)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.totalDegree = 0

Tactic:
suffices p.degrees.card = 0 by grind [totalDegree_le_degrees_card p]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.degrees.card = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ (φ ^ 0).vars ⊆ φ.vars

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2.monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
ih : ↑((monomial a) s).coeffs ⊆ range ⇑f → (monomial a) s ∈ range ⇑(map f)
hx : ↑((monomial a) s + p).coeffs ⊆ range ⇑f
⊢ (monomial a) s + p ∈ range ⇑(map f)

Tactic:
rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩

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

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
h : i ≠ j
⊢ degreeOf i (X j ^ 0) = 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ (eval₂Hom f g) φ = 0

Tactic:
φ.as_sum,

Goal state after:
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ (eval₂Hom f g) (∑ v ∈ φ.support, (monomial v) (coeff v φ)) = 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 * X j ^ 0) = degreeOf i p

Tactic:
| zero =>

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
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ p.totalDegree ≤ q.totalDegree

Tactic:
totalDegree_eq p,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ (p.support.sup fun m ↦ (toMultiset m).card) ≤ q.totalDegree
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

Tactic:
by_cases ha : a = 0 <;> simp [ha]

Goal state after: