awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
a : R
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (X s) =
    HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X s) 1)
rw₁ rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (X s) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (X s)
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (X s) =
    (monomial (Finsupp.single s 1) : (a : R) → MvPolynomial σ R) a

Tactic:
rw [← C_mul_X_pow_eq_monomial, pow_one]

Premises used: pow_one, MvPolynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 0) 0

Tactic:
Finsupp.single_zero _

Premises used: AddMonoidAlgebra, Finsupp.single_zero, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := (a : R) → MvPolynomial σ R) (⇑(monomial 0) : (a : R) → MvPolynomial σ R) (⇑C : (a : R) → MvPolynomial σ R)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
b : R
⊢ Eq (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) (0 : MvPolynomial σ R) ↔
    b = 0

Tactic:
Finsupp.single_eq_zero

Premises used: Finsupp.single_eq_zero, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : AddCommMonoid A
u : σ →₀ ℕ
r : R
b : (σ →₀ ℕ) → R → A
w : b u 0 = 0
⊢ sum ((monomial u : (a : R) → MvPolynomial σ R) r) b = b u r

Tactic:
Finsupp.sum_single_index w

Premises used: Finsupp.sum_single_index, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
A : Type u_2
inst_1 : AddCommMonoid A
b : (σ →₀ ℕ) → R → A
w : b 0 0 = 0
⊢ sum ((C : (a : R) → MvPolynomial σ R) a) b = b 0 a

Tactic:
sum_monomial_eq w

Premises used: MvPolynomial.sum_monomial_eq, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1)
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1)

Tactic:
map_prod (monomialOneHom R σ) (fun i => Multiplicative.ofAdd (f i)) s

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, map_prod, Finset.prod, Multiplicative, Finsupp.onFinset, MvPolynomial.monomialOneHom, Finsupp.zipWith, Multiplicative.ofAdd, DFunLike.coe, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
rw :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HSMul.hSMul (β := MvPolynomial σ R) a ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1)
rw₂ :
  Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (HSMul.hSMul (β := R) a 1) : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
rw₄ rw₅ :
  Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)

Tactic:
rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]

Premises used: MvPolynomial.monomial, MvPolynomial.C_mul', LinearMap.map_smul, MvPolynomial.monomial_sum_one, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
simp_rw :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
    ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
simp_rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (∏ x ∈ s, (C : (a : R) → MvPolynomial σ R) (g x))
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
    ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
simp_rw₂ :
  Eq (α := MvPolynomial σ R)
    (∏ x ∈ s,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial σ R) (g x) : MvPolynomial σ R)
        ((monomial (f x) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
simp_rw₃ :
  Eq (α := MvPolynomial σ R) (∏ x ∈ s, (monomial (f x) : (a : R) → MvPolynomial σ R) (g x * 1))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
⊢ Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))

Tactic:
simp_rw [monomial_sum_index, map_prod, ← Finset.prod_mul_distrib, C_mul_monomial, mul_one]

Premises used: Finset.prod_mul_distrib, MvPolynomial.C_mul_monomial, map_prod, MvPolynomial.monomial_sum_index, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
β : Type u_3
inst_1 : Zero β
f : α →₀ β
g : α → β → σ →₀ ℕ
a : R
⊢ (monomial (f.sum g) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (f.prod fun (a : α) (b : β) ↦ (monomial (g a b) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)

Tactic:
monomial_sum_index _ _ _

Premises used: Finsupp.sum, MvPolynomial.monomial_sum_index, Finsupp.prod
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
α : Type u_2
a₁ a₂ : α →₀ ℕ
b₁ b₂ : R
⊢ Eq (α := MvPolynomial α R) ((monomial a₁ : (a : R) → MvPolynomial α R) b₁ : MvPolynomial α R)
      ((monomial a₂ : (a : R) → MvPolynomial α R) b₂ : MvPolynomial α R) ↔
    a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
Finsupp.single_eq_single_iff _ _ _ _

Premises used: Finsupp.single_eq_single_iff, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst : CommSemiring R
⊢ (monomial s : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e : MvPolynomial σ R)

Tactic:
simp only [X_pow_eq_monomial, ← monomial_finsupp_sum_index, Finsupp.sum_single]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.monomial_finsupp_sum_index, Finsupp.sum_single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R)
    (∏ x ∈ s.support, HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x) ((s : (a : σ) → ℕ) x : ℕ))
    ((monomial s : (a : R) → MvPolynomial σ R) 1)

Tactic:
simp only [monomial_eq, map_one, one_mul, Finsupp.prod]

Premises used: map_one, MvPolynomial.monomial_eq, Finsupp.prod, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
rw :
  Eq (α := MvPolynomial σ R) (∏ y ∈ t, HPow.hPow (α := MvPolynomial σ R) (X y) (x y))
    (∏ x_1 ∈ t,
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x_1)
        ((Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i : (a : σ) → ℕ) x_1 : ℕ))
rw₁ :
  ∀ x_1 ∈ t,
    x_1 ∉ Finsupp.support (M := ℕ) (Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i) →
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x_1)
          ((Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i : (a : σ) → ℕ) x_1 : ℕ) =
        1
⊢ Eq (α := MvPolynomial σ R) (∏ y ∈ t, HPow.hPow (α := MvPolynomial σ R) (X y) (x y))
    ((monomial (Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i) : (a : R) → MvPolynomial σ R) 1)

Tactic:
rw [monomial_eq, C_1, one_mul, Finsupp.prod, Finset.prod_subset (support_indicator_subset _ _)]

Premises used: MvPolynomial.C_1, Finset.prod_subset, MvPolynomial.monomial_eq, Finsupp.support_indicator_subset, Finsupp.prod, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
x_1 : σ
hi : x_1 ∈ t
⊢ HPow.hPow (α := MvPolynomial σ R) (X x_1) (x x_1) =
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x_1)
      ((Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i : (a : σ) → ℕ) x_1 : ℕ)

Tactic:
simp [Finsupp.indicator, hi]

Premises used: Finsupp.indicator
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ Eq (α := MvPolynomial σ R) (∏ y ∈ t, HPow.hPow (α := MvPolynomial σ R) (X y) (x y))
    (∏ x_1 ∈ t,
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x_1)
        ((Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i : (a : σ) → ℕ) x_1 : ℕ))

Tactic:
exact Finset.prod_congr rfl (fun _ hi ↦ by simp [Finsupp.indicator, hi])

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : i ∉ Finsupp.support (M := ℕ) (Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i)
⊢ Eq (α := ℕ) ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
rw [Finsupp.mem_support_iff, ne_eq, not_not] at hi'

Premises used: Finsupp.mem_support_iff, Classical.not_not, ne_eq
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : Eq (α := ℕ) ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
rw : HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1
rw₁ rw₂ : Eq (α := MvPolynomial σ R) 1 1
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i)
      ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) =
    1

Tactic:
rw [hi', pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
zero : motive ((monomial 0 : (a : R) → MvPolynomial σ R) a)
single_add :
  ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support →
      b ≠ 0 →
        motive ((monomial f : (a : R) → MvPolynomial σ R) a) →
          motive ((monomial (Finsupp.single a_1 b + f) : (a : R) → MvPolynomial σ R) a)
⊢ motive ((monomial s : (a : R) → MvPolynomial σ R) a)

Tactic:
apply @Finsupp.induction σ ℕ _ _ s

Premises used: Finsupp.induction
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
zero : motive ((monomial 0 : (a : R) → MvPolynomial σ R) a)
⊢ motive ((monomial 0 : (a : R) → MvPolynomial σ R) a)

Tactic:
change motive (monomial 0 a)

Premises used: MvPolynomial.monomial, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ motive ((monomial 0 : (a : R) → MvPolynomial σ R) a)

Tactic:
C a

Premises used: Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ motive ((monomial 0 : (a : R) → MvPolynomial σ R) a)

Tactic:
exact C a
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
⊢ motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X n) 0))

Tactic:
simp [ih]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e_1 : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e_1 ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
e : ℕ
e_ih :
  motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e))
⊢ motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) (e + 1)))

Tactic:
simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]

Premises used: pow_succ, mul_assoc, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e_1 : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e_1 ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
e : ℕ
zero :
  motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X n) 0))
succ :
  ∀ (e : ℕ)
    (e_ih :
      motive
        (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          (HPow.hPow (α := MvPolynomial σ R) (X n) e))),
    motive
      (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (HPow.hPow (α := MvPolynomial σ R) (X n) (e + 1)))
⊢ motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e))

Tactic:
induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]

Premises used: pow_succ, mul_assoc, AddMonoidAlgebra.zero, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
single_add :
  ∀
    (this :
      ∀ (e : ℕ),
        motive
          (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
            (HPow.hPow (α := MvPolynomial σ R) (X n) e))),
    motive ((monomial (Finsupp.single n e + p) : (a : R) → MvPolynomial σ R) a)
⊢ motive ((monomial (Finsupp.single n e + p) : (a : R) → MvPolynomial σ R) a)

Tactic:
have : ∀ e : ℕ, motive (monomial p a * X n ^ e) := by
      intro e
      induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
this :
  ∀ (e : ℕ),
    motive
      (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (HPow.hPow (α := MvPolynomial σ R) (X n) e))
⊢ motive ((monomial (Finsupp.single n e + p) : (a : R) → MvPolynomial σ R) a)

Tactic:
simp [add_comm, monomial_add_single, this]

Premises used: MvPolynomial.monomial_add_single, add_comm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
P : MvPolynomial σ R → Prop
p : MvPolynomial σ R
monomial : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)
add : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)
this : P ((MvPolynomial.monomial 0 : (a : R) → MvPolynomial σ R) 0)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : P 0), P 0
⊢ P 0

Tactic:
rwa [monomial_zero] at this

Premises used: MvPolynomial.monomial_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
p : MvPolynomial σ R
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
monomial_add :
  ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R),
    a ∉ f.support →
      b ≠ 0 →
        motive f →
          motive (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)
⊢ motive p

Tactic:
Finsupp.induction p (C_0.rec <| C 0) monomial_add

Premises used: Finsupp.induction
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
p : MvPolynomial σ R
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
monomial_add :
  ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R),
    a ∉ f.support →
      b ≠ 0 →
        motive f →
          motive ((monomial a : (a : R) → MvPolynomial σ R) b) →
            motive
              (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
⊢ motive p

Tactic:
monomial_add_induction_on p C fun a b f ha hb hf =>
    monomial_add a b f ha hb hf <| induction_on_monomial C mul_X a b

Premises used: MvPolynomial.monomial_add_induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
p : MvPolynomial σ R
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add : ∀ (p q : MvPolynomial σ R), motive p → motive q → motive (p + q)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
⊢ motive p

Tactic:
induction_on'' p C (fun a b f _ha _hb hf hm => add (monomial a b) f hm hf) mul_X

Premises used: MvPolynomial.induction_on'', MvPolynomial.monomial, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ f = g

Tactic:
AddMonoidAlgebra.ringHom_ext' ?_ ?_

Premises used: AddMonoidAlgebra.ringHom_ext'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
refine_1 : f.comp singleZeroRingHom = g.comp singleZeroRingHom
refine_2 :
  Eq (α := MonoidHom.{u_1, u_2} (Multiplicative (σ →₀ ℕ)) A) (MonoidHom.comp (↑f : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
    (MonoidHom.comp (↑g : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
⊢ f = g

Tactic:
refine AddMonoidAlgebra.ringHom_ext' ?_ ?_

Premises used: AddMonoidAlgebra.ringHom_ext'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
refine_1 :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := A) ((f.comp singleZeroRingHom : (a : R) → A) x : A)
      ((g.comp singleZeroRingHom : (a : R) → A) x : A)
⊢ f.comp singleZeroRingHom = g.comp singleZeroRingHom

Tactic:
ext x
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
x : R
⊢ Eq.{u_2 + 1} (α := A) ((f.comp singleZeroRingHom : (a : R) → A) x : A)
    ((g.comp singleZeroRingHom : (a : R) → A) x : A)

Tactic:
hC _

Premises used: Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
x : R
⊢ Eq.{u_2 + 1} (α := A) ((f.comp singleZeroRingHom : (a : R) → A) x : A)
    ((g.comp singleZeroRingHom : (a : R) → A) x : A)

Tactic:
exact hC _