awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
m : σ →₀ ℕ
p_1 q : MvPolynomial σ R
h : coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) p_1) = coeff m p_1
h_1 : coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) q) = coeff m q
⊢ coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (p_1 + q)) = coeff m (p_1 + q)

Tactic:
simp [*, nsmul_right_inj hp]

Premises used: nsmul_right_inj
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
m : σ →₀ ℕ
monomial :
  ∀ (u : σ →₀ ℕ) (a : R),
    Eq.{u_3 + 1} (α := R)
      (coeff (p • m)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)))
      (coeff m ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a))
add :
  ∀ (p_1 q : MvPolynomial σ R),
    coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) p_1) = coeff m p_1 →
      coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) q) = coeff m q →
        coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (p_1 + q)) = coeff m (p_1 + q)
monomial₁ :
  ∀ (u : σ →₀ ℕ) (a : R),
    Eq.{u_3 + 1} (α := R)
      (coeff (p • m)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)))
      (coeff m ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a))
add₁ :
  ∀ (p_1 q : MvPolynomial σ R),
    coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) p_1) = coeff m p_1 →
      coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) q) = coeff m q →
        coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (p_1 + q)) = coeff m (p_1 + q)
monomial₂ :
  ∀ (u : σ →₀ ℕ) (a : R),
    Eq.{u_3 + 1} (α := R)
      (coeff (p • m)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)))
      (coeff m ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a))
add₂ :
  ∀ (p_1 q : MvPolynomial σ R),
    coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) p_1) = coeff m p_1 →
      coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) q) = coeff m q →
        coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (p_1 + q)) = coeff m (p_1 + q)
monomial₃ :
  ∀ (u : σ →₀ ℕ) (a : R),
    Eq.{u_3 + 1} (α := R)
      (coeff (p • m)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)))
      (coeff m ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a))
add₃ :
  ∀ (p_1 q : MvPolynomial σ R),
    coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) p_1) = coeff m p_1 →
      coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) q) = coeff m q →
        coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (p_1 + q)) = coeff m (p_1 + q)
⊢ coeff (p • m) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff m φ

Tactic:
classical
  induction φ using induction_on' <;> simp [*, nsmul_right_inj hp]

Premises used: nsmul_right_inj
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
rw rw₁ :
  Eq.{u_3 + 1} (α := R) (coeff.{u_3, u_1} (σ := σ) 0 ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff.{u_3, u_1} (σ := σ) 0 ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
⊢ Eq.{u_3 + 1} (α := R) (coeff.{u_3, u_1} (σ := σ) 0 ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (coeff (HSMul.hSMul (β := σ →₀ ℕ) p 0) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
rw rw₁ : coeff 0 φ = coeff 0 φ
⊢ coeff (HSMul.hSMul (β := σ →₀ ℕ) p 0) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = coeff 0 φ

Tactic:
rw [coeff_expand_smul p hp]

Premises used: MvPolynomial.coeff_expand_smul
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H :
  Eq (α := MvPolynomial σ R) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
    ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g' : MvPolynomial σ R)
a : ∀ (d : σ →₀ ℕ), coeff d g = coeff d g'
⊢ g = g'

Tactic:
ext d
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H :
  Eq (α := MvPolynomial σ R) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
    ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g' : MvPolynomial σ R)
d : σ →₀ ℕ
a : coeff (n • d) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g) = coeff d g'
a₁ : coeff (n • d) ((expand n : (a : MvPolynomial σ R) → MvPolynomial σ R) g') = coeff d g'
a₂ a₃ : coeff d g' = coeff d g'
⊢ coeff d g = coeff d g'

Tactic:
rw [← coeff_expand_smul _ (n.ne_zero_iff_zero_lt.mpr hn), H, coeff_expand_smul _
      (n.ne_zero_iff_zero_lt.mpr hn)]

Premises used: Iff.mpr, Nat.ne_zero_iff_zero_lt, MvPolynomial.coeff_expand_smul
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : 0 < p
f g : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) g : MvPolynomial σ R) ↔
    f = g

Tactic:
(expand_injective hp).eq_iff

Premises used: Function.Injective.eq_iff, MvPolynomial.expand_injective
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      (0 : MvPolynomial σ R) ↔
    f = 0

Tactic:
(expand_injective hp).eq_iff' (map_zero _)

Premises used: map_zero, Function.Injective.eq_iff', MvPolynomial.expand_injective
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
⊢ Ne (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      (0 : MvPolynomial σ R) ↔
    f ≠ 0

Tactic:
(expand_eq_zero hp).not

Premises used: MvPolynomial.expand_eq_zero, Iff.not
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
r : R
rw :
  Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial σ R) ↔
    f = (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)
p₁ : ℕ
rw₁ :
  f = (C : (a : R) → MvPolynomial σ R) r ↔
    f = (expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r)
rw₂ rw₃ : f = (C : (a : R) → MvPolynomial σ R) r ↔ f = (C : (a : R) → MvPolynomial σ R) r
⊢ Eq (α := MvPolynomial σ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    f = (C : (a : R) → MvPolynomial σ R) r

Tactic:
rw [← expand_C, expand_inj hp, expand_C]

Premises used: MvPolynomial.expand_C, MvPolynomial.expand_inj
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
hf :
  ∀ (i : σ),
    Eq (α := MvPolynomial τ R)
      ((AlgHom.comp (expand p) (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
      ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
            (a : MvPolynomial σ R) → MvPolynomial τ R)
          (X i) :
        MvPolynomial τ R)
⊢ AlgHom.comp (expand p) (bind₁ f) = bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i)

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ Eq (α := MvPolynomial τ R)
    ((AlgHom.comp (expand p) (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        (X i) :
      MvPolynomial τ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
rw :
  Eq (α := MvPolynomial τ R)
    ((AlgHom.comp (expand p) (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        φ :
      MvPolynomial τ R)
rw₁ rw₂ :
  Eq (α := MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        φ :
      MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        φ :
      MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial τ R)
    ((bind₁ fun (i : σ) ↦ (expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial τ R)
        φ :
      MvPolynomial τ R)

Tactic:
rw [← AlgHom.comp_apply, expand_comp_bind₁]

Premises used: AlgHom.comp_apply, MvPolynomial.expand_comp_bind₁
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ S)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) :
      MvPolynomial σ S)
    ((expand p : (a : MvPolynomial σ S) → MvPolynomial σ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
      MvPolynomial σ S)

Tactic:
simp [expand, map_bind₁]

Premises used: MvPolynomial.map_bind₁, MvPolynomial.expand
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → τ
hf :
  ∀ (i : σ),
    Eq (α := MvPolynomial τ R)
      ((AlgHom.comp (rename f) (expand p) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
      ((AlgHom.comp (expand p) (rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (AlgHom.comp (rename f) (expand p))
    (AlgHom.comp (expand p) (rename f))

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → τ
i : σ
⊢ Eq (α := MvPolynomial τ R)
    ((AlgHom.comp (rename f) (expand p) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)
    ((AlgHom.comp (expand p) (rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i) : MvPolynomial τ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → τ
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) :
      MvPolynomial τ R)
    ((expand p : (a : MvPolynomial τ R) → MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial τ R)

Tactic:
DFunLike.congr_fun (rename_comp_expand p f) φ

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.rename_comp_expand, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
hC :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := S)
      ((RingHom.comp ((eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R)) C : (a : R) → S) x : S)
      (((eval₂Hom f (g ^ p)).comp C : (a : R) → S) x : S)
hX :
  ∀ (i : σ),
    Eq.{u_4 + 1} (α := S)
      (((eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R) : (a : MvPolynomial σ R) → S) (X i) :
        S)
      ((eval₂Hom f (g ^ p) : (a : MvPolynomial σ R) → S) (X i) : S)
⊢ (eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R) = eval₂Hom f (g ^ p)

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
x : R
⊢ Eq.{u_4 + 1} (α := S)
    ((RingHom.comp ((eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R)) C : (a : R) → S) x : S)
    (((eval₂Hom f (g ^ p)).comp C : (a : R) → S) x : S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
i : σ
⊢ Eq.{u_4 + 1} (α := S)
    (((eval₂Hom f g).comp (↑(expand p) : MvPolynomial σ R →+* MvPolynomial σ R) : (a : MvPolynomial σ R) → S) (X i) : S)
    ((eval₂Hom f (g ^ p) : (a : MvPolynomial σ R) → S) (X i) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
φ : MvPolynomial σ R
⊢ eval₂ f g ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) = eval₂ f (g ^ p) φ

Tactic:
DFunLike.congr_fun (eval₂Hom_comp_expand p f g) φ

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, MvPolynomial.eval₂Hom_comp_expand
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
f : σ → A
hf :
  ∀ (i : σ),
    Eq.{u_5 + 1} (α := A) ((AlgHom.comp (aeval f) (expand p) : (a : MvPolynomial σ R) → A) (X i) : A)
      ((aeval (f ^ p) : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] A) (AlgHom.comp (aeval f) (expand p)) (aeval (f ^ p))

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
f : σ → A
i : σ
⊢ Eq.{u_5 + 1} (α := A) ((AlgHom.comp (aeval f) (expand p) : (a : MvPolynomial σ R) → A) (X i) : A)
    ((aeval (f ^ p) : (a : MvPolynomial σ R) → A) (X i) : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
f : σ → A
φ : MvPolynomial σ R
⊢ Eq.{u_5 + 1} (α := A)
    ((aeval f : (a : MvPolynomial σ R) → A)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R) :
      A)
    ((aeval (f ^ p) : (a : MvPolynomial σ R) → A) φ : A)

Tactic:
eval₂_expand ..

Premises used: Multiset.sum, MvPolynomial.eval₂_expand, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
f : σ → R
φ : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := R)
    ((eval f : (a : MvPolynomial σ R) → R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R) :
      R)
    ((eval (f ^ p) : (a : MvPolynomial σ R) → R) φ : R)

Tactic:
eval₂_expand ..

Premises used: Multiset.sum, MvPolynomial.eval₂_expand, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
rw :
  support.{u_3, u_1} (R := R)
    ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (∑ v ∈ φ.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v φ)))
| support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)

Tactic:
rw [φ.as_sum]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
conv_lhs :
  Subset (α := Finset (σ →₀ ℕ))
    (support.{u_3, u_1} (R := R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (∑ v ∈ φ.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v φ))))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
⊢ Subset (α := Finset (σ →₀ ℕ)) (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)

Tactic:
conv_lhs => rw [φ.as_sum]

Premises used: MvPolynomial.as_sum
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
simp :
  Subset (α := Finset (σ →₀ ℕ))
    (support.{u_3, u_1} (R := R) (∑ x ∈ φ.support, (monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
⊢ Subset (α := Finset (σ →₀ ℕ))
    (support.{u_3, u_1} (R := R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        (∑ v ∈ φ.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v φ))))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)

Tactic:
simp only [map_sum, expand_monomial]

Premises used: MvPolynomial.expand_monomial, map_sum
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset (α := Finset (σ →₀ ℕ))
    (support.{u_3, u_1} (R := R) (∑ x ∈ φ.support, (monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)

Tactic:
MvPolynomial.support_sum.trans ?_

Premises used: MvPolynomial.support_sum, Set.Mem, setOf, HasSubset.Subset.trans
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
refine :
  Subset (α := Finset (σ →₀ ℕ))
    (φ.support.biUnion fun (x : σ →₀ ℕ) ↦
      support.{u_3, u_1} (R := R) ((monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
⊢ Subset (α := Finset (σ →₀ ℕ))
    (support.{u_3, u_1} (R := R) (∑ x ∈ φ.support, (monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)

Tactic:
refine MvPolynomial.support_sum.trans ?_

Premises used: MvPolynomial.support_sum, HasSubset.Subset.trans
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset (α := Finset (σ →₀ ℕ))
    (φ.support.biUnion fun (x : σ →₀ ℕ) ↦
      support.{u_3, u_1} (R := R) ((monomial (p • x) : (a : R) → MvPolynomial σ R) (coeff x φ)))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)

Tactic:
aesop (add simp Finset.subset_iff)

Premises used: Finset.subset_iff
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! :
  ∀ (h : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0),
    p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
⊢ ∃ a ∈ φ.support, p • a = m

Tactic:
grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h

Premises used: MvPolynomial.mem_support_iff, Finset.mem_image, MvPolynomial.support_expand_subset
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ∃ a ∈ φ.support, p • a = m
rcases : ∀ (a : σ →₀ ℕ), p ∣ (p • a : (a : σ) → ℕ) i
⊢ p ∣ (m : (a : σ) → ℕ) i

Tactic:
rcases h with ⟨a, -, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
i : σ
a : σ →₀ ℕ
⊢ (p • a : (a : σ) → ℕ) i = HMul.hMul (β := ℕ) p ((a : (a : σ) → ℕ) i : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
i : σ
a : σ →₀ ℕ
⊢ p ∣ (p • a : (a : σ) → ℕ) i

Tactic:
exact ⟨a i, by simp⟩
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0
contrapose!₂ contrapose!₃ contrapose!₄ :
  ∀ (h : Ne.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₅ : ∀ (h : ∃ a ∈ φ.support, p • a = m), p ∣ (m : (a : σ) → ℕ) i
contrapose!₆ : ∀ (a : σ →₀ ℕ), p ∣ (p • a : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ)) 0

Tactic:
classical
  contrapose! h
  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
  rcases h with ⟨a, -, rfl⟩
  exact ⟨a i, by simp⟩

Premises used: MvPolynomial.mem_support_iff, Finset.mem_image, MvPolynomial.support_expand_subset, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
hp : p ≠ 0
⊢ Eq (α := Finset (σ →₀ ℕ)) (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)

Tactic:
(support_expand_subset φ).antisymm ?_

Premises used: MvPolynomial.support_expand_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
hp : p ≠ 0
refine :
  Subset (α := Finset (σ →₀ ℕ)) (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
    (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
⊢ Eq (α := Finset (σ →₀ ℕ)) (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
    (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)

Tactic:
refine (support_expand_subset φ).antisymm ?_

Premises used: MvPolynomial.support_expand_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Algebra.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst_1 : DecidableEq σ
hp : p ≠ 0
⊢ Subset (α := Finset (σ →₀ ℕ)) (Finset.image (fun (x : σ →₀ ℕ) ↦ p • x) φ.support)
    (support.{u_3, u_1} (R := R) ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))

Tactic:
simp [Finset.image_subset_iff, hp]

Premises used: Finset.image_subset_iff