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

Goal state before:
pp: case w.refine_1
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∀ (x y : ↥(sSup (domain '' c))), f (x + y) = f x + f y

Tactic:
intro x

Goal state after:
case w.refine_1
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x : ↥(sSup (domain '' c))
⊢ ∀ (y : ↥(sSup (domain '' c))), f (x + y) = f x + f y
Module: Mathlib.Algebra.FreeAlgebra

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

Tactic:
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
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ eval₂ (C.comp f) X ((monomial n) a) = (monomial n) (f a)

Tactic:
eval₂_monomial,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ (C.comp f) a * X ^ n = (monomial n) (f a)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

Tactic:
by
  refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩
  have h1 := Nat.one_lt_two.trans_le h.1
  refine ⟨mt Nat.isUnit_iff.mp h1.ne', ?_⟩
  rintro a b rfl
  simp only [Nat.isUnit_iff]
  refine (h.2 a <| dvd_mul_right ..).imp_right fun hab ↦ ?_
  rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]

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

Goal state before:
pp: p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e✝ : p = m * k
e : p = k * m
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ 1 * m < k * m

Tactic:
by rwa [one_mul, ← e]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : ↑y = (x_fst, x_snd).1
h : ↑(z • f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph

Tactic:
rw [LinearPMap.smul_apply] at h

Goal state after:
case mp
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
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : ↑y = (x_fst, x_snd).1
h : z • ↑f y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
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

Goal state after:
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
x : E
⊢ x ∈ f.domain → x ∈ g.domain
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
⊢ f.graph ≤ g.graph

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
⊢ x ∈ f.graph → x ∈ g.graph
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✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a₂

Tactic:
simpa [mul_def, sum_sum_index, add_smul, Finsupp.mul_sum, Finsupp.sum_mul,
        smul_mul_smul_comm] using Finsupp.sum_comm ..

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Ioo a c) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
⊢ x ∈ Ioo a c → x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Ico a c) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
⊢ x ∈ Ico a c → x ∈ {x | (fun x ↦ f x ≤ f b) x}
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
hf : f.toFun.ker = ⊥
y : E
hv : (0, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph
⊢ (0, y).2 = 0

Tactic:
simp only [Submodule.map_equiv_eq_comap_symm, Submodule.mem_comap, LinearEquiv.symm_prodComm,
    LinearEquiv.coe_coe, LinearEquiv.prodComm_apply, mem_graph_iff, Prod.swap] at hv

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
y : E
hv : ∃ y_1, ↑y_1 = y ∧ ↑f y_1 = 0
⊢ (0, y).2 = 0
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
⊢ IsMaxOn f (Ioc a c) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
⊢ x ∈ Ioc a c → x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
⊢ IsMaxOn f (Icc a c) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
⊢ x ∈ Icc a c → x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
⊢ IsMaxOn f (Ioi a) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
⊢ x ∈ Ioi a → x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
⊢ IsMaxOn f (Ici a) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
⊢ x ∈ Ici a → x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
⊢ IsMaxOn f (Iio a) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
⊢ x ∈ Iio a → x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[ℕ]
⊢ ({ toFinsupp := p } * { toFinsupp := q }).coeff n =
    ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * { toFinsupp := q }.coeff x.2

Tactic:
simp_rw [← ofFinsupp_mul, coeff]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[ℕ]
⊢ (p * q).coeff n = ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
⊢ IsMaxOn f (Iic a) b

Tactic:
intro x

Goal state after:
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
⊢ x ∈ Iic a → x ∈ {x | (fun x ↦ f x ≤ f b) x}
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 ?_ ?_
    · simp
    · intro g r c' _nm _nz w
      dsimp at *
      simp only [add_smul, f.map_add, w, single_eq_algebraMap_mul_of, ← smul_smul]
      rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]

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✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
      (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
        a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
              coeffAddEquiv.toAddMonoidHom)).toFun
        a₂

Tactic:
simpa [mul_def, sum_sum_index, add_smul, Finsupp.mul_sum, Finsupp.sum_mul,
        smul_mul_smul_comm] using Finsupp.sum_comm ..

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

Goal state before:
pp: case neg.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n

Tactic:
exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

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✝¹ : Algebra R A
inst✝ : Monoid M
r : R
⊢ (toAdditive A M).toFun ((algebraMap R A[M]) r) = (algebraMap R (AddMonoidAlgebra A (Additive M))) r

Tactic:
by simp [toAdditive]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : (C a).natDegree < p.natDegree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
exact natDegree_add_eq_left_of_natDegree_lt hpd

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
x : R
⊢ eval₂ C X ((monomial n) x) = (monomial n) x

Tactic:
eval₂_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
x : R
⊢ C x * X ^ n = (monomial n) x
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).degree = q.degree

Tactic:
rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).support ⊆ p.support

Tactic:
intro x

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∈ (map f p).support → x ∈ p.support
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ eval₂ f (f x) p = 0

Tactic:
← eval_map

Goal state after:
S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ eval (f x) (Polynomial.map f p) = 0
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ ∃ n a, f = (monomial n) a

Tactic:
refine ⟨n, f.coeff n, ?_⟩

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ f = (monomial n) (f.coeff n)
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h' : ∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i
x : ι
⊢ g₁ x ≤ g₂ x

Tactic:
simpa [Finsupp.embDomain_apply] using h' (f x)

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
⊢ ∀ (x : R), ¬C ((algebraMap R A) x) = X

Tactic:
intro x

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
x : R
⊢ ¬C ((algebraMap R A) x) = X
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = f (∑ n ∈ p.support, C (p.coeff n) * X ^ n)

Tactic:
simp only [map_sum, map_mul, map_pow]

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ ∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * f X ^ n = ∑ x ∈ p.support, f (C (p.coeff x)) * f X ^ x
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case pos
ι : 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 : ι →₀ α
y : κ
hy : y ∉ Set.range f
⊢ (mapDomain f (f1 - f2)) y = (mapDomain f f1 - mapDomain f f2) y

Tactic:
simp [mapDomain_of_notMem_range _ _ hy]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ (fun {i} x1 x2 ↦ x1 < x2) (a i) (Function.update a i b i)

Tactic:
rwa [Function.update_self i b]

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₁
a : R
⊢ eval₂ f g ((monomial 0) a) = f a

Tactic:
eval₂_monomial,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ (f a * Finsupp.prod 0 fun n e ↦ g n ^ e) = f a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
⊢ ∀ (x : σ),
    ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
      ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))

Tactic:
intro x

Goal state after:
case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : σ
⊢ ((↑f).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
    ((↑g).comp (of R (σ →₀ ℕ))).comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (q + p).support

Tactic:
exact support_sdiff_support_subset_support_add q p

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → σ
hf : LeftInverse f g
⊢ LeftInverse ⇑(rename f) ⇑(rename g)

Tactic:
intro x

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → σ
hf : LeftInverse f g
x : MvPolynomial τ R
⊢ (rename f) ((rename g) x) = x
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
⊢ False

Tactic:
rcases mem_degrees.mp hi with ⟨s, hs1, hs2⟩

Goal state after:
case refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
s : σ →₀ ℕ
hs1 : coeff s p ≠ 0
hs2 : i ∈ s.support
⊢ False
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
⊢ ∀ ⦃x : σ →₀ ℕ⦄, coeff x ((map f) p) ≠ 0 → coeff x p ≠ 0

Tactic:
intro x

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x ((map f) p) ≠ 0 → coeff x p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case H₂
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ⇑f
⊢ ∀ ⦃x : σ →₀ ℕ⦄, coeff x p ≠ 0 → coeff x ((map f) p) ≠ 0

Tactic:
intro x

Goal state after:
case H₂
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ⇑f
x : σ →₀ ℕ
⊢ coeff x p ≠ 0 → coeff x ((map f) p) ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)

Tactic:
intro x

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
⊢ x ∈ coeffsIn σ M → ∀ n ∈ coeffsIn σ N, x * n ∈ coeffsIn σ (M * N)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: 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
⊢ (p - ((monomial d) c - (monomial d') c)).support ⊆ p.support.erase d ∪ {d'}

Tactic:
intro x

Goal state after:
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 : σ →₀ ℕ
⊢ x ∈ (p - ((monomial d) c - (monomial d') c)).support → x ∈ p.support.erase d ∪ {d'}
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p + q).vars ⊆ p.vars ∪ q.vars

Tactic:
intro x

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
⊢ x ∈ (p + q).vars → x ∈ p.vars ∪ q.vars
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ degreeOf i p ≠ 0 → p ≠ 0

Tactic:
by
  aesop

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

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

Tactic:
intro x

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ (X s).totalDegree = 1

Tactic:
rw [totalDegree, support_X]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ({Finsupp.single s 1}.sup fun s ↦ s.sum fun x e ↦ e) = 1
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
by
  rcases eq_or_ne o (m * n) with rfl | h
  · simpa only [ite_true] using coeff_pow_of_natDegree_le pn
  · simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt <|
      lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).eraseLead = 0

Tactic:
rw [X_pow_eq_monomial, eraseLead_monomial]

Goal state after: