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

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ C ↑0 = ↑0

pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
a✝ : C ↑n✝ = ↑n✝
⊢ C ↑(n✝ + 1) = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ C ↑0 = ↑0

case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
a✝ : C ↑n✝ = ↑n✝
⊢ C ↑(n✝ + 1) = ↑(n✝ + 1)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
x✝ : R
⊢ ((φ.comp (eval₂Hom f g)).comp C) x✝ = ((eval₂Hom (φ.comp f) fun i ↦ φ (g i)).comp C) x✝

pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
i✝ : σ
⊢ (φ.comp (eval₂Hom f g)) (X i✝) = (eval₂Hom (φ.comp f) fun i ↦ φ (g i)) (X i✝)

Tactic:
<;>

Goal state after:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
x✝ : R
⊢ ((φ.comp (eval₂Hom f g)).comp C) x✝ = ((eval₂Hom (φ.comp f) fun i ↦ φ (g i)).comp C) x✝

case hX
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
i✝ : σ
⊢ (φ.comp (eval₂Hom f g)) (X i✝) = (eval₂Hom (φ.comp f) fun i ↦ φ (g i)) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∈ p.support ↔ coeff m p ≠ 0

Tactic:
by
  simp [support, coeff]

Goal state after:
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₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (a : R), k (eval₂ f g (C a)) = eval₂ (k.comp f) (⇑k ∘ g) (C a)

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.comp f) (⇑k ∘ g) p →
      k (eval₂ f g q) = eval₂ (k.comp f) (⇑k ∘ g) q → k (eval₂ f g (p + q)) = eval₂ (k.comp f) (⇑k ∘ g) (p + q)

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.comp f) (⇑k ∘ g) p → k (eval₂ f g (p * X n)) = eval₂ (k.comp f) (⇑k ∘ g) (p * X n)

Tactic:
<;>

Goal state after:
case C
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
⊢ ∀ (a : R), k (eval₂ f g (C a)) = eval₂ (k.comp f) (⇑k ∘ g) (C a)

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.comp f) (⇑k ∘ g) p →
      k (eval₂ f g q) = eval₂ (k.comp f) (⇑k ∘ g) q → k (eval₂ f g (p + q)) = eval₂ (k.comp f) (⇑k ∘ g) (p + q)

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

Goal state before:
pp: case C
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ C X (C a) = C a

pp: case add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R), eval₂ C X p = p → eval₂ C X q = q → eval₂ C X (p + q) = p + q

pp: case mul_X
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), eval₂ C X p = p → eval₂ C X (p * X n) = p * X n

Tactic:
<;>

Goal state after:
case C
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ C X (C a) = C a

case add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R), eval₂ C X p = p → eval₂ C X q = q → eval₂ C X (p + q) = p + q

case mul_X
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), eval₂ C X p = p → eval₂ C X (p * X n) = p * X n
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: 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
⊢ f wit < g wit → P (toLex f) (toLex g)

pp: 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
⊢ g wit < f wit → P (toLex f) (toLex g)

Tactic:
<;>

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
⊢ 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
⊢ g wit < f wit → P (toLex f) (toLex g)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
rw [coeffs, Finset.image_subset_iff]
    simp_all [coeff_one]

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

Goal state before:
pp: case isTrue
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : r = 0
⊢ ∅ ⊆ {r}

pp: case isFalse
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : ¬r = 0
⊢ {r} ⊆ {r}

Tactic:
<;>

Goal state after:
case isTrue
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : r = 0
⊢ ∅ ⊆ {r}

case isFalse
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : ¬r = 0
⊢ {r} ⊆ {r}
Module: Mathlib.Algebra.MvPolynomial.Rename

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

pp: case neg
σ : 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 : σ →₀ ℕ
h : i ∉ range f
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))

Tactic:
<;>

Goal state after:
case pos
σ : 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 : σ →₀ ℕ
h : i ∈ range f
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))

case neg
σ : 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 : σ →₀ ℕ
h : i ∉ range f
⊢ coeff n (((↑(killCompl hf)).comp (map φ)) (X i)) = coeff n (((map φ).comp ↑(killCompl hf)) (X i))
Module: Mathlib.Algebra.MvPolynomial.Basic

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

pp: case neg
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h✝ : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
hp : ¬coeff n p = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h✝ : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
hp : coeff n p = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0

case neg
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h✝ : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
hp : ¬coeff n p = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0
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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
a✝ : R
⊢ eval₂ ((map f).comp C) h (C a✝) = eval₂ C h ((map f) (C a✝))

pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p✝ q✝ : MvPolynomial ι R
a✝¹ : eval₂ ((map f).comp C) h p✝ = eval₂ C h ((map f) p✝)
a✝ : eval₂ ((map f).comp C) h q✝ = eval₂ C h ((map f) q✝)
⊢ eval₂ ((map f).comp C) h (p✝ + q✝) = eval₂ C h ((map f) (p✝ + q✝))

pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p✝ : MvPolynomial ι R
n✝ : ι
a✝ : eval₂ ((map f).comp C) h p✝ = eval₂ C h ((map f) p✝)
⊢ eval₂ ((map f).comp C) h (p✝ * X n✝) = eval₂ C h ((map f) (p✝ * X n✝))

Tactic:
<;>

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
a✝ : R
⊢ eval₂ ((map f).comp C) h (C a✝) = eval₂ C h ((map f) (C a✝))

case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p✝ q✝ : MvPolynomial ι R
a✝¹ : eval₂ ((map f).comp C) h p✝ = eval₂ C h ((map f) p✝)
a✝ : eval₂ ((map f).comp C) h q✝ = eval₂ C h ((map f) q✝)
⊢ eval₂ ((map f).comp C) h (p✝ + q✝) = eval₂ C h ((map f) (p✝ + q✝))

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p✝ : MvPolynomial ι R
n✝ : ι
a✝ : eval₂ ((map f).comp C) h p✝ = eval₂ C h ((map f) p✝)
⊢ eval₂ ((map f).comp C) h (p✝ * X n✝) = eval₂ C h ((map f) (p✝ * X n✝))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
⊢ q (eval₂ (RingHom.id S₁) g p) = eval₂ q (⇑q ∘ g) p

Tactic:
eval₂_comp_right,

Goal state after:
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
⊢ eval₂ q (⇑q ∘ g) ((map (RingHom.id S₁)) p) = eval₂ q (⇑q ∘ g) p
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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ f g ((rename k) (C a)) = eval₂ f (g ∘ k) (C a)

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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p →
      eval₂ f g ((rename k) q) = eval₂ f (g ∘ k) q → eval₂ f g ((rename k) (p + q)) = eval₂ f (g ∘ k) (p + q)

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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p → eval₂ f g ((rename k) (p * X n)) = eval₂ f (g ∘ k) (p * X n)

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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ f g ((rename k) (C a)) = eval₂ f (g ∘ k) (C a)

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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p →
      eval₂ f g ((rename k) q) = eval₂ f (g ∘ k) q → eval₂ f g ((rename k) (p + q)) = eval₂ f (g ∘ k) (p + q)

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
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p → eval₂ f g ((rename k) (p * X n)) = eval₂ f (g ∘ k) (p * X n)
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))

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))

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 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))

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))

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₁
p : MvPolynomial σ R
⊢ ∀ (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 : MvPolynomial σ R
⊢ ∀ (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
⊢ ∀ (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₁
p : MvPolynomial σ R
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m ((map f) (C a)) = f (coeff m (C a))

case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (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))

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (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 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)

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)

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 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)

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)

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

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)

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 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)

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)

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

Goal state before:
pp: case isTrue
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
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
h✝ : i = j
⊢ x ∈ M

pp: case isFalse
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
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
h✝ : ¬i = j
⊢ 0 ∈ M

Tactic:
<;>

Goal state after:
case isTrue
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
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
h✝ : i = j
⊢ x ∈ M

case isFalse
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
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
h✝ : ¬i = j
⊢ 0 ∈ M