mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (a : R), (rename k) (eval₂ C (g ∘ k) (C a)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (C a))

Tactic:
·

Goal state after:
case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (a : R), (rename k) (eval₂ C (g ∘ k) (C a)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (C a))
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p) →
      (rename k) (eval₂ C (g ∘ k) q) = eval₂ C (⇑(rename k) ∘ g) ((rename k) q) →
        (rename k) (eval₂ C (g ∘ k) (p + q)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p + q))

Tactic:
·

Goal state after:
case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p) →
      (rename k) (eval₂ C (g ∘ k) q) = eval₂ C (⇑(rename k) ∘ g) ((rename k) q) →
        (rename k) (eval₂ C (g ∘ k) (p + q)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p) →
      (rename k) (eval₂ C (g ∘ k) (p * X n)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p * X n))

Tactic:
·

Goal state after:
case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p) →
      (rename k) (eval₂ C (g ∘ k) (p * X n)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p * X n))
Module: Mathlib.Algebra.MvPolynomial.Eval

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

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:
·

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

Goal state before:
pp: case refine_2.inr
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ∃ n_1, ¬coeff n_1 p + coeff n_1 q = 0 ∧ coeff n q = coeff n_1 p + coeff n_1 q

Tactic:
·

Goal state after:
case refine_2.inr
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ∃ n_1, ¬coeff n_1 p + coeff n_1 q = 0 ∧ coeff n q = coeff n_1 p + coeff n_1 q
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (a : R), (rename (Prod.mk j)) (eval₂ C g (C a)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (C a)

Tactic:
·

Goal state after:
case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (a : R), (rename (Prod.mk j)) (eval₂ C g (C a)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (C a)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p →
      (rename (Prod.mk j)) (eval₂ C g q) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) q →
        (rename (Prod.mk j)) (eval₂ C g (p + q)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p + q)

Tactic:
·

Goal state after:
case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p →
      (rename (Prod.mk j)) (eval₂ C g q) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) q →
        (rename (Prod.mk j)) (eval₂ C g (p + q)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p + q)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p →
      (rename (Prod.mk j)) (eval₂ C g (p * X n)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p * X n)

Tactic:
·

Goal state after:
case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p →
      (rename (Prod.mk j)) (eval₂ C g (p * X n)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p * X n)
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:
·

Goal state after:
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))
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (a : R), eval₂ f g ((rename (Prod.mk i)) (C a)) = eval₂ f (fun j ↦ g (i, j)) (C a)

Tactic:
·

Goal state after:
case C
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (a : R), eval₂ f g ((rename (Prod.mk i)) (C a)) = eval₂ f (fun j ↦ g (i, j)) (C a)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p q : MvPolynomial τ R),
    eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun j ↦ g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i)) q) = eval₂ f (fun j ↦ g (i, j)) q →
        eval₂ f g ((rename (Prod.mk i)) (p + q)) = eval₂ f (fun j ↦ g (i, j)) (p + q)

Tactic:
·

Goal state after:
case add
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p q : MvPolynomial τ R),
    eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun j ↦ g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i)) q) = eval₂ f (fun j ↦ g (i, j)) q →
        eval₂ f g ((rename (Prod.mk i)) (p + q)) = eval₂ f (fun j ↦ g (i, j)) (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₁
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:
·

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p : MvPolynomial τ R) (n : τ),
    eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun j ↦ g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i)) (p * X n)) = eval₂ f (fun j ↦ g (i, j)) (p * X n)

Tactic:
·

Goal state after:
case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p : MvPolynomial τ R) (n : τ),
    eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun j ↦ g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i)) (p * X n)) = eval₂ f (fun j ↦ g (i, j)) (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s = 0

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:
·

Goal state after:
case refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ (a : σ), a ∉ p.degrees
s : σ →₀ ℕ
hs : s ∈ p.support
⊢ s = 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, C a = (rename Subtype.val) q

pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1

pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) q

Tactic:
·

Goal state after:
case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, C a = (rename Subtype.val) q
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mp
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M

pp: case mpr
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M

Tactic:
·

Goal state after:
case mp
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1

pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) q

Tactic:
·

Goal state after:
case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ toMultiset 0 ≤ (p + q).degrees

pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ toMultiset d ≤ (p + q).degrees

Tactic:
·

Goal state after:
case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ toMultiset 0 ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mpr
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M

Tactic:
·

Goal state after:
case mpr
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ MvPolynomial (↥(s ∪ t)) R

pp: case add.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ (rename Subtype.val) p + (rename Subtype.val) q = (rename Subtype.val) ?add.refine_1

Tactic:
·

Goal state after:
case add.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ MvPolynomial (↥(s ∪ t)) R
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ toMultiset d ≤ (p + q).degrees

Tactic:
·

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ toMultiset d ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename Subtype.val) ((rename (Subtype.map id ⋯)) p + (rename (Subtype.map id ⋯)) q)

Tactic:
·

Goal state after:
case add.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename Subtype.val) ((rename (Subtype.map id ⋯)) p + (rename (Subtype.map id ⋯)) q)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M ≤ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)

Tactic:
·

Goal state after:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M ≤ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
hp : p ∈ coeffsIn σ M
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩

Goal state after:
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✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)

Tactic:
·

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) q

Tactic:
·

Goal state after:
case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) q
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), (eval g) ((map f) (C a)) = eval₂ f g (C a)

Tactic:
·

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), (eval g) ((map f) (C a)) = eval₂ f g (C a)
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ MvPolynomial (↥(insert n s)) R

pp: case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ?mul_X.refine_1

Tactic:
·

Goal state after:
case mul_X.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ MvPolynomial (↥(insert n s)) R
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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (eval g) ((map f) p) = eval₂ f g p →
      (eval g) ((map f) q) = eval₂ f g q → (eval g) ((map f) (p + q)) = eval₂ f g (p + q)

Tactic:
·

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

Goal state before:
pp: case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ((rename (Subtype.map id ⋯)) p * X ⟨n, ⋯⟩)

Tactic:
·

Goal state after:
case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ((rename (Subtype.map id ⋯)) 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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval g) ((map f) p) = eval₂ f g p → (eval g) ((map f) (p * X n)) = eval₂ f g (p * X n)

Tactic:
·

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval g) ((map f) p) = eval₂ f g p → (eval g) ((map f) (p * X n)) = eval₂ f g (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∈ p.support
⊢ coeff i p ∈ M

pp: case neg
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p ∈ M

Tactic:
·

Goal state after:
case pos
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∈ p.support
⊢ coeff i p ∈ M
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p ∈ M

Tactic:
·

Goal state after:
case neg
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p ∈ M
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
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 ∈ M * N, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ coeffsIn σ M * coeffsIn σ N

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
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)

Tactic:
·

Goal state after:
case refine_1
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 ∈ M * N, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ coeffsIn σ M * coeffsIn σ N