mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) {a} x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support

Tactic:
image₂_singleton_left

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ image (fun b ↦ a * b) x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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
⊢ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } } ∈ upperBounds c

Tactic:
intro p

Goal state after:
case h
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
p : E →ₛₗ.[σ] F
⊢ p ∈ c → p ≤ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }
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:
LinearPMap.smul_apply

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

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

Tactic:
by
  rcases hp with ⟨hp⟩ | ⟨hp'⟩
  · rcases hq with hq | hq'
    exacts [rfl, False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))]
  · rcases hq with hq | hq'
    exacts [False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp')),
      CharP.eq R ‹_› ‹_›]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case refine_1
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
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃ x, (a, x) ∈ g

pp: case refine_2
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
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂

Tactic:
· convert! ha
    simp

Goal state after:
case refine_2
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
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (C x * X ^ k).coeff n = if n = k then x else 0

Tactic:
rw [C_mul_X_pow_eq_monomial, coeff_monomial]
  simp [eq_comm]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * X ^ n * C r).coeff (d + n) = p.coeff d * r

Tactic:
coeff_mul_C,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * X ^ n).coeff (d + n) * r = p.coeff d * r
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ((monomial 0) a).support.max = 0

Tactic:
support_monomial 0 ha,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ {0}.max = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
coeff_mul_C,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ p.coeff (p * C a).natDegree * a = p.leadingCoeff * a
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ s.coeff.support.inf (WithTop.some ∘ D) = ↑(s.coeff.support.inf D)

Tactic:
← Finset.coe_inf' hs,

Goal state after:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ ↑(s.coeff.support.inf' hs D) = ↑(s.coeff.support.inf D)
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
⊢ (map f p).degree = p.degree

Tactic:
refine degree_map_le.antisymm ?_

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
⊢ p.degree ≤ (map f p).degree
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
⊢ eval₂ (algebraMap R A) (f X) p = f p

Tactic:
conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]

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
⊢ eval₂ (algebraMap R A) (f X) p = f (p.sum fun n a ↦ C a * X ^ n)
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : 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 : ι →₀ α
⊢ mapDomain f (f1 - f2) = mapDomain f f1 - mapDomain f f2

Tactic:
ext y
  by_cases! hy : y ∉ Set.range f
  · simp [mapDomain_of_notMem_range _ _ hy]
  · obtain ⟨x, rfl⟩ := hy
    simp [mapDomain_apply h]

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

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

Tactic:
intro p

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

Tactic:
intro p

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

Goal state before:
pp: R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
this : AddMonoidAlgebra.single 0 a * AddMonoidAlgebra.single s a' = AddMonoidAlgebra.single s (a * a')
⊢ C a * (monomial s) a' = (monomial s) (a * a')

Tactic:
exact this

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ (C (p.coeff 0)).coeff default = p.coeff default

Tactic:
simp [C_apply, ← single_eq_monomial]

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

Goal state before:
pp: case add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q →
        (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)

Tactic:
intro p

Goal state after:
case add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q →
        (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)
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:
rw [MvPolynomial.ext_iff]
  simp only [coeff_zero]

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

Goal state before:
pp: case mul_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p * X n)

Tactic:
intro p

Goal state after:
case mul_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p : MvPolynomial σ R
⊢ ∀ (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
⊢ IsLeftRegular ((MvPolynomial.monomial m) a)

Tactic:
intro p

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p : MvPolynomial σ R
⊢ ∀ ⦃a₂ : MvPolynomial σ R⦄,
    (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) a₂ → p = a₂
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
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 : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) →
      k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q) → k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))

Tactic:
intro p

Goal state after:
case add
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
⊢ ∀ (q : MvPolynomial σ R),
    k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) →
      k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q) → k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))
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 : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) → k (eval₂ f g (p * X n)) = eval₂ k (⇑k ∘ g) ((map f) (p * X n))

Tactic:
intro p

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
⊢ ∀ (n : σ),
    k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) → k (eval₂ f g (p * X n)) = eval₂ k (⇑k ∘ g) ((map f) (p * X n))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ∀ (p q : MvPolynomial S₂ R),
    (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) →
      (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q) →
        (map f) (eval₂ C g (p + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))

Tactic:
intro p

Goal state after:
case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
⊢ ∀ (q : MvPolynomial S₂ R),
    (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) →
      (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q) →
        (map f) (eval₂ C g (p + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
⊢ ∀ (p : MvPolynomial S₂ R) (n : S₂),
    (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) →
      (map f) (eval₂ C g (p * X n)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p * X n))

Tactic:
intro p

Goal state after:
case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
⊢ ∀ (n : S₂),
    (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) →
      (map f) (eval₂ C g (p * X n)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p * X n))
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ coeff s ((killCompl hf) p) = coeff (Finsupp.mapDomain f s) p

Tactic:
apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))

Goal state after:
case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ ∀ (u : τ →₀ ℕ) (a : R), coeff s ((killCompl hf) ((monomial u) a)) = coeff (Finsupp.mapDomain f s) ((monomial u) a)

case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ ∀ (p q : MvPolynomial τ R),
    coeff s ((killCompl hf) p) = coeff (Finsupp.mapDomain f s) p →
      coeff s ((killCompl hf) q) = coeff (Finsupp.mapDomain f s) q →
        coeff s ((killCompl hf) (p + q)) = coeff (Finsupp.mapDomain f s) (p + q)
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
intro p

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))
Module: Mathlib.Algebra.MvPolynomial.Eval

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

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

Tactic:
· intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p * X n)) = f (coeff m (p * X n))
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₁
f : R →+* S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p * X n)) = f (coeff m (p * X n))

Tactic:
intro p

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p * X n)) = f (coeff m (p * X n))
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₁
hf : Injective ⇑f
⊢ Injective ⇑(map f)

Tactic:
intro p

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p : MvPolynomial σ R
⊢ ∀ ⦃a₂ : MvPolynomial σ R⦄, (map f) p = (map f) a₂ → p = a₂
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
⊢ ((map f) p).support ⊆ p.support

Tactic:
simp only [Finset.subset_iff, mem_support_iff]

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.Basic

Goal state before:
pp: case refine_1.mem_mul_mem
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
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) m * (monomial 0) n ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
apply Submodule.mul_mem_mul

Goal state after:
case refine_1.mem_mul_mem.hm
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
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) m ∈ coeffsIn σ M

case hn
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
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial 0) n ∈ coeffsIn σ N
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
⊢ p.support ⊆ ((map f) p).support

Tactic:
simp only [Finset.subset_iff, mem_support_iff]

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.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ (map q) φ = 0

Tactic:
rw [C_dvd_iff_dvd_coeff, MvPolynomial.ext_iff]

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔ ∀ (m : σ →₀ ℕ), coeff m ((map q) φ) = coeff m 0
Module: Mathlib.Algebra.MvPolynomial.Rename

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

Tactic:
intro p

Goal state after:
case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    constantCoeff ((rename f) p) = constantCoeff p →
      constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)
Module: Mathlib.Algebra.MvPolynomial.Rename

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

Tactic:
intro p

Goal state after:
case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
⊢ ∀ (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
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 ((Finset.mem_singleton.mp h1) ▸ hx) hd_not

Goal state after: