mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective ⇑includeLeft

Tactic:
← Function.Bijective.of_comp_iff _ (TensorProduct.rid R S A).bijective

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective (⇑includeLeft ∘ ⇑(TensorProduct.rid R S A))
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c + 0

Tactic:
add_zero

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * c

Tactic:
nth_rewrite 2 [← hc]; exact star_right_conjugate_nonneg ha c

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : ⊤ ≤ span K t
⊢ range ⇑(extendLe hs hst ht) = hs.extend hst

Tactic:
by
  rw [coe_extendLe, Subtype.range_coe_subtype, ofPred_mem_eq]

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

Goal state before:
pp: L : Type u_1
inst✝⁵ : Field L
inst✝⁴ : LinearOrder L
inst✝³ : IsStrictOrderedRing L
W : Type v
inst✝² : AddCommGroup W
inst✝¹ : Module L W
inst✝ : FiniteDimensional L W
t : Finset W
h : finrank L W + 1 < #t
f : W → L
sum : ∑ e ∈ t, f e • e = 0
total : ∑ e ∈ t, f e = 0
nonzero : ∃ x ∈ t, f x ≠ 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x

Tactic:
exact ⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀

Tactic:
simp_rw [rank_le_one_iff, le_span_singleton_iff]
  simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + 1)) * Quot.mk (Rel R X) a =
    (Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n)) + 1) * Quot.mk (Rel R X) a

Tactic:
congr 1

Goal state after:
case mk.e_a
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + 1)) = Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n)) + 1
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x + y ∈ S

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)

Tactic:
by_cases d2 : 2 ∣ n

Goal state after:
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)

case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
Module: Mathlib.Algebra.CharP.Defs

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

Tactic:
add_zero

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

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

Tactic:
Nat.div_one

Goal state after:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ 1 ≤ 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n / n.minFac

Tactic:
by
    conv_rhs =>
      congr
      rw [hx]
    rw [Nat.mul_div_cancel_left _ (minFac_pos _)]
    exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq : ExpChar R q
⊢ q = 1

Tactic:
rcases hq with q | hq_prime

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
hp : CharP R 0
inst✝ : CharZero R
⊢ 1 = 1

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
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
⊢ p = q ↔ Nat.Prime p

Tactic:
rcases hq with q | hq_prime

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 1 ↔ Nat.Prime p

case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q ↔ Nat.Prime p
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case left
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.graph ≤ g.graph
⊢ f.domain ≤ g.domain

Tactic:
intro x hx
    rw [mem_domain_iff] at hx ⊢
    obtain ⟨y, hx⟩ := hx
    use y
    exact h hx

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
⊢ domCongr R A 1 = 1

Tactic:
MulAut.one_def,

Goal state after:
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
⊢ domCongr R A (MulEquiv.refl M) = 1
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : SemilatticeSup B
inst✝¹ : OrderBot B
inst✝ : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).coeff.support.sup degb ≤ f.coeff.support.sup degb ⊔ g.coeff.support.sup degb

Tactic:
exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ p.coeff (d - n) = p.coeff (d - n + n - n)

Tactic:
add_tsub_cancel_right

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ p.coeff (d - n) = p.coeff (d - n)
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✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ (∑ i ∈ s, (f i).coeff).support.sup D ≤ s.sup fun i ↦ (f i).coeff.support.sup D

Tactic:
grw [Finsupp.support_finsetSum, Finset.sup_biUnion]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ (C a).natDegree = 0

Tactic:
by
  by_cases ha : a = 0
  · have : C a = 0 := by rw [ha, C_0]
    rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]
  · rw [natDegree, degree_C ha, WithBot.unbotD_zero]

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

Goal state before:
pp: case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : i < d
⊢ ↑(d.choose i) - 1 = ↑(d.choose i)

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

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

Goal state before:
pp: case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 1 = 0

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

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

Goal state before:
pp: case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : i < d
⊢ ↑(d.choose i) - 0 = ↑(d.choose i)

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

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

Goal state before:
pp: case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 0 = 0

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ (↑n).natDegree = 0

Tactic:
by
  rw [← C_eq_intCast, natDegree_C]

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).natDegree ≤ max p.natDegree q.natDegree

Tactic:
rcases le_max_iff.1 (degree_add_le p q) with h | h

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
p q : R[X]
h : (p + q).degree ≤ p.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
h : (p + q).degree ≤ q.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree + 0 ≠ 0

Tactic:
add_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree ≠ 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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ leadingCoeff D p + 0 = leadingCoeff D p

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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q

Tactic:
add_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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ leadingCoeff D p = leadingCoeff D p

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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i + 0) = supDegree D (f i) ∧ leadingCoeff D (f i + 0) = leadingCoeff D (f i)

Tactic:
add_zero

Goal state after:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i) = supDegree D (f i) ∧ leadingCoeff D (f i) = leadingCoeff D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
by
  rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ 1 + 0 = 1

Tactic:
add_zero

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ 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
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1)) + 0

Tactic:
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.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:
Function.iterate_succ_apply',

Goal state after:
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 (p.comp^[k] q)) = (fun x ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
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 (p.comp^[k] q)) = (fun x ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)

Tactic:
Function.iterate_succ_apply',

Goal state after:
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 (p.comp^[k] q)) = eval₂ f ((fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : x i = 0 ∧ y i = 0
⊢ 0 = x i ∧ 0 = y i

Tactic:
exact h.imp Eq.symm Eq.symm

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ φ p = (φ.comp (aeval X)) p

Tactic:
aeval_X_left,

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ φ p = (φ.comp (AlgHom.id R R[X])) p
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
u : ι →₀ ℕ
i : ι
h : u i ≠ 0
⊢ u + single i 1 - single i 1 = u

Tactic:
add_tsub_cancel_right

Goal state after:
ι : Type u_1
u : ι →₀ ℕ
i : ι
h : u i ≠ 0
⊢ u = u
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ ↑y.support ⊆ ↑(y + w).support

pp: α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ ↑(y + w).support ⊆ Set.range ⇑f

Tactic:
· exact fun _ ↦ by simp; grind

Goal state after:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ ↑(y + w).support ⊆ Set.range ⇑f
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case add
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 y : S ⊗[R] N
hx : X ^ k • (rTensor N (↑R (monomial 0))) x = (rTensor N (↑R (monomial k))) x
hy : X ^ k • (rTensor N (↑R (monomial 0))) y = (rTensor N (↑R (monomial k))) y
⊢ X ^ k • (rTensor N (↑R (monomial 0))) (x + y) = (rTensor N (↑R (monomial k))) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (f + g) = (f + 0).neLocus (f + g)

Tactic:
add_zero

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (f + g) = f.neLocus (f + g)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: 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
⊢ (f (p.coeff C) * C.prod fun n e ↦ g₁ n ^ e) = f (p.coeff C) * C.prod fun n e ↦ g₂ n ^ e

Tactic:
congr 1

Goal state after:
case 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
⊢ (C.prod fun n e ↦ g₁ n ^ e) = C.prod fun n e ↦ g₂ n ^ e
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case 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
⊢ g₁ i ^ C i = g₂ i ^ C i

Tactic:
congr 1

Goal state after:
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
⊢ g₁ i = g₂ i
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:
eq_zero_iff

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
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✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ k (eval₂ f g p * eval₂ f g (X s)) = eval₂ k (⇑k ∘ g) ((map f) (p * X s))

Tactic:
k.map_mul,

Goal state after:
case mul_X
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✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ k (eval₂ f g p) * k (eval₂ f g (X s)) = eval₂ k (⇑k ∘ g) ((map f) (p * X s))
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 : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
by_cases hp : coeff n p = 0 <;> simp_all

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ degrees 0 = 0

Tactic:
rw [← C_0]
  exact degrees_C 0

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ coeff d p - (c - 0) = 0

Tactic:
sub_zero,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ coeff d p - c = 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 : σ
h : p ≠ 0
⊢ degreeOf i p = degreeOf i p + 0

Tactic:
add_zero

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
⊢ degreeOf i p = degreeOf i p
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ (cons (t 0) t.tail) a = t a

Tactic:
· rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]

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

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this✝ : p.support.Nonempty
s : σ →₀ ℕ
hs2 : degreeOf i p = s i
hs1 : ¬coeff s p = 0
this : coeff s q = 0
⊢ ¬coeff s p + 0 = 0

Tactic:
add_zero

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this✝ : p.support.Nonempty
s : σ →₀ ℕ
hs2 : degreeOf i p = s i
hs1 : ¬coeff s p = 0
this : coeff s q = 0
⊢ ¬coeff s p = 0
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₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ (f₁ (coeff d p₁) * d.prod fun i k ↦ g₁ i ^ k) = f₁ (coeff d p₁) * d.prod fun i k ↦ g₂ i ^ k

Tactic:
congr 1

Goal state after:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ (d.prod fun i k ↦ g₁ i ^ k) = d.prod fun i k ↦ g₂ i ^ k
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ ((algebraMap R (MvPolynomial σ R)) (coeff u q) * u.prod fun i k ↦ (if i ∈ s then X i else 0) ^ k) =
    C (coeff u q) * u.prod fun n e ↦ X n ^ e

Tactic:
congr 1

Goal state after:
case e_a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ (u.prod fun i k ↦ (if i ∈ s then X i else 0) ^ k) = u.prod fun n e ↦ X n ^ e