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

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f))) (f (hB b)) = hB b

Tactic:
rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ C.domRestrict (invFun ⇑f) ⟨f ↑b, ⋯⟩ = ↑b
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval₂ (RingHom.id R) x p = p.sum fun e a ↦ a * x ^ e

Tactic:
eval₂_eq_sum

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ (p.sum fun e a ↦ (RingHom.id R) a * x ^ e) = p.sum fun e a ↦ a * x ^ e
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ eval₂ C q p = p.sum fun e a ↦ C a * q ^ e

Tactic:
eval₂_eq_sum

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.sum fun e a ↦ C a * q ^ e) = p.sum fun e a ↦ C a * q ^ e
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ Algebra.adjoin R (Set.range (ι R)) = ⊤

Tactic:
set S := Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X))
  refine top_unique fun x hx => ?_; clear hx
  induction x with
  | grade0 => exact S.algebraMap_mem _
  | add x y hx hy => exact S.add_mem hx hy
  | mul x y hx hy => exact S.mul_mem hx hy
  | grade1 x => exact Algebra.subset_adjoin (Set.mem_range_self _)

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q

Tactic:
by
  rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]

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✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ f (c • v) = (RingHom.id R[M]) c • f v

Tactic:
refine induction c ?_ ?_

Goal state after:
case refine_1
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✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ f (0 • v) = (RingHom.id R[M]) 0 • f v

case refine_2
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✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        f (x • v) = (RingHom.id R[M]) x • f v → f ((single m r + x) • v) = (RingHom.id R[M]) (single m r + x) • f v
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
· grind [mem_antidiagonal]

Goal state after:
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✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
hr : r = 0
⊢ supDegree D (single a r) = ⊥

Tactic:
simp [supDegree_single_ne_zero, hr]

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

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
hr : ¬r = 0
⊢ supDegree D (single a r) = D a

Tactic:
simp [supDegree_single_ne_zero, hr]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X).degree = 1

Tactic:
simpa only [pow_one] using! degree_C_mul_X_pow 1 ha

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

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

Tactic:
Finset.sum_empty,

Goal state after:
case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D 1 ≤ 0
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.Nonempty

Tactic:
nonempty_iff_ne_empty,

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:
nonempty_iff_ne_empty,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support ≠ ∅ ↔ ¬p = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x

Tactic:
refine ⟨zero_lt_one.trans_le, fun h => ?_⟩
  cases x
  · exact (not_lt_bot h).elim
  · rwa [← WithBot.coe_zero, WithBot.coe_lt_coe, ← Nat.add_one_le_iff, zero_add,
      ← WithBot.coe_le_coe, WithBot.coe_one] at h

Goal state after:
Module: Mathlib.Algebra.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 + ∑ x ∈ ∅, f x) = supDegree D (f i) ∧ leadingCoeff D (f i + ∑ x ∈ ∅, f x) = leadingCoeff D (f i)

Tactic:
Finset.sum_empty,

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 + 0) = supDegree D (f i) ∧ leadingCoeff D (f i + 0) = leadingCoeff D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree = 3

Tactic:
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
    degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    degree_C_mul_X_pow 3 ha]

Goal state after:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑3 = 3
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: 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 ^ n) = n • supDegree D p

Tactic:
induction n with
  | zero => rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
  | succ n ih => rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₁ x) ≤ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₂ x)

Tactic:
gcongr with i hi

Goal state after:
case h
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
i : ι
hi : i ∈ f₁.support ∪ f₂.support
⊢ h i (f₁ i) ≤ h i (f₂ i)
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]
r : R
p : A[X]
⊢ (r • p).toFinsupp = ((C.comp (algebraMap R A)) r * p).toFinsupp

Tactic:
dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply]
      rw [toFinsupp_smul, toFinsupp_mul, toFinsupp_C]
      exact Algebra.smul_def' _ _

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
⊢ f s ≤ g s

Tactic:
by_cases H : s ∈ f.support

Goal state after:
case pos
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
H : s ∈ f.support
⊢ f s ≤ g s

case neg
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
H : s ∉ f.support
⊢ f s ≤ g s
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
x : ι
⊢ (mapDomain f (f1 - f2)) (f x) = (mapDomain f f1 - mapDomain f f2) (f x)

Tactic:
simp [mapDomain_apply h]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval (ψ a) (map (algebraMap T U) (map φ p))

Tactic:
map_map,

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval (ψ a) (map ((algebraMap T U).comp φ) p)
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ (eval₂ (algebraMap R (M →ₗ[R] M)) f p) v = p.sum fun n b ↦ b • (f ^ n) v

Tactic:
eval₂_eq_sum

Goal state after:
R : Type u
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ (p.sum fun e a ↦ (algebraMap R (M →ₗ[R] M)) a * f ^ e) v = p.sum fun n b ↦ b • (f ^ n) v
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 g = f.neLocus (-g)

Tactic:
by rw [← neLocus_neg_neg, neg_neg]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ j,
    (∀ d < j, (ofLex (toLex (single b 1))) d = (ofLex (toLex (single a 1))) d) ∧
      ((ofLex (toLex (single b 1))) j).lt ((ofLex (toLex (single a 1))) j)

Tactic:
simp only [ofLex_toLex, Nat.lt_eq]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ j, (∀ d < j, (single b 1) d = (single a 1) d) ∧ (single b 1) j < (single a 1) j
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
| coeff (m - s) p * r

Tactic:
← coeff_mul_monomial _ s

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
| coeff (m - s + s) (p * (monomial s) r)
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
⊢ P (toLex f) (toLex g)

Tactic:
apply (mem_neLocus.mp <| Finset.mem_of_min h).lt_or_gt.by_cases <;> intro hwit

Goal state after:
case h₁
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
hwit : f wit < g wit
⊢ P (toLex f) (toLex g)

case h₂
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3
h_lt : {f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)
h_eq : {f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)
h_gt : {f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)
f g : Π₀ (i : ι), α i
wit : ι
h : (f.neLocus g).min = ↑wit
hwit : g wit < f wit
⊢ P (toLex f) (toLex g)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case hX
σ : 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 : σ →₀ ℕ
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))

Tactic:
· by_cases h : i ∈ Set.range f <;> simp [killCompl, h]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)

Tactic:
by
  classical
  apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
  · intro p i hp m
    simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ →+* R
hf : LeftInverse ⇑f ⇑g
X : MvPolynomial σ S₁
⊢ (map f) ((map g) X) = X

Tactic:
map_map,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ →+* R
hf : LeftInverse ⇑f ⇑g
X : MvPolynomial σ S₁
⊢ (map (f.comp g)) X = X
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case refine_1
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
x : MvPolynomial σ S₁
hx : x ∈ range ⇑(map f)
⊢ ↑x.coeffs ⊆ range ⇑f

Tactic:
obtain ⟨p, rfl⟩ := hx
    exact subset_trans (coe_coeffs_map f p) (by simp)

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

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : c = 0
h1 : x ∈ ∅
⊢ x ∈ p.support.erase d ∪ {d'}

pp: case neg
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : ¬c = 0
h1 : x ∈ {d}
⊢ x ∈ p.support.erase d ∪ {d'}

Tactic:
· exact absurd h1 (Finset.notMem_empty _)

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : ¬c = 0
h1 : x ∈ {d}
⊢ x ∈ p.support.erase d ∪ {d'}
Module: Mathlib.Algebra.MvPolynomial.Variables

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

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

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

Goal state before:
pp: case a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ Algebra.adjoin R (range f) ≤ (aeval f).range

Tactic:
· rw [Algebra.adjoin_le_iff]
    rintro x ⟨i, rfl⟩
    use X i, by aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support < #f.support

Tactic:
rw [eraseLead_support]
  exact card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)

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

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
a : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ (Polynomial.eval₂ C (X default) (Polynomial.C a)) = coeff m✝ (C a)

Tactic:
Polynomial.eval₂_C

Goal state after:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
a : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ (C a) = coeff m✝ (C a)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q

Tactic:
rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree = 1 ↔ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p

Tactic:
refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff 1 = 0
⊢ False

case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = p

case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) ((monomial j) r)).coeff i) = coeff (cons i m) ((monomial j) r)

Tactic:
simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
      Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
      Fin.cases_succ, ← _root_.map_prod, ← map_pow, Function.comp_apply]

Goal state after:
case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m ((Polynomial.X ^ j 0 * Polynomial.C (∏ x, X x ^ j x.succ)).coeff i) = if j = cons i m then r else 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ #(range n) • x ^ (n - 1) = ↑n * x ^ (n - 1)

Tactic:
by rw [Finset.card_range, nsmul_eq_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (-p).degree < ↑n

Tactic:
rwa [← degree_neg p] at H

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
by_cases hp₀ : p = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r