awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
hC :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := T) ((((eval₂Hom f g).comp (bind₂ h)).comp C : (a : R) → T) x : T)
      (((eval₂Hom ((eval₂Hom f g).comp h) g).comp C : (a : R) → T) x : T)
hX :
  ∀ (i : σ),
    Eq.{u_5 + 1} (α := T) (((eval₂Hom f g).comp (bind₂ h) : (a : MvPolynomial σ R) → T) (X i) : T)
      ((eval₂Hom ((eval₂Hom f g).comp h) g : (a : MvPolynomial σ R) → T) (X i) : T)
⊢ (eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g

Tactic:
ext : 2
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
x : R
⊢ Eq.{u_5 + 1} (α := T) ((((eval₂Hom f g).comp (bind₂ h)).comp C : (a : R) → T) x : T)
    (((eval₂Hom ((eval₂Hom f g).comp h) g).comp C : (a : R) → T) x : T)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
i : σ
⊢ Eq.{u_5 + 1} (α := T) (((eval₂Hom f g).comp (bind₂ h) : (a : MvPolynomial σ R) → T) (X i) : T)
    ((eval₂Hom ((eval₂Hom f g).comp h) g : (a : MvPolynomial σ R) → T) (X i) : T)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
φ : MvPolynomial σ R
⊢ Eq.{u_5 + 1} (α := T)
    ((eval₂Hom f g : (a : MvPolynomial σ S) → T)
        ((bind₂ h : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S) :
      T)
    ((eval₂Hom ((eval₂Hom f g).comp h) g : (a : MvPolynomial σ R) → T) φ : T)

Tactic:
RingHom.congr_fun (eval₂Hom_comp_bind₂ f g h) φ

Premises used: Multiset.sum, Multiset.foldr, MvPolynomial.eval₂Hom_comp_bind₂, RingHom.congr_fun, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra S T
f : σ → T
g : R →+* MvPolynomial σ S
φ : MvPolynomial σ R
⊢ Eq.{u_5 + 1} (α := T)
    ((aeval f : (a : MvPolynomial σ S) → T)
        ((bind₂ g : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S) :
      T)
    ((eval₂Hom (RingHom.comp (↑(aeval f) : MvPolynomial σ S →+* T) g) f : (a : MvPolynomial σ R) → T) φ : T)

Tactic:
eval₂Hom_bind₂ _ _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂Hom, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, MvPolynomial.eval₂Hom_bind₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
d : σ →₀ ℕ
r : R
⊢ (bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial d : (a : R) → MvPolynomial σ R) r) =
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)

Tactic:
simp only [monomial_eq, map_mul, bind₁_C_right, Finsupp.prod, map_prod,
    map_pow, bind₁_X_right]

Premises used: MvPolynomial.bind₁_C_right, map_pow, map_prod, map_mul, MvPolynomial.monomial_eq, MvPolynomial.bind₁_X_right, Finsupp.prod
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
r : R
⊢ (bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial d : (a : R) → MvPolynomial σ R) r) =
    HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S) ((f : (a : R) → MvPolynomial σ S) r : MvPolynomial σ S)
      ((monomial d : (a : S) → MvPolynomial σ S) 1 : MvPolynomial σ S)

Tactic:
simp only [monomial_eq, map_mul, bind₂_C_right, Finsupp.prod, map_prod,
    map_pow, bind₂_X_right, C_1, one_mul]

Premises used: MvPolynomial.C_1, map_pow, map_prod, MvPolynomial.bind₂_X_right, map_mul, MvPolynomial.bind₂_C_right, MvPolynomial.monomial_eq, Finsupp.prod, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
rw :
  HMul.hMul (α := MvPolynomial σ S) ((f : (a : R) → MvPolynomial σ S) 1) ((monomial d : (a : S) → MvPolynomial σ S) 1) =
    (monomial d : (a : S) → MvPolynomial σ S) 1
rw₁ :
  HMul.hMul (α := MvPolynomial σ S) 1 ((monomial d : (a : S) → MvPolynomial σ S) 1) =
    (monomial d : (a : S) → MvPolynomial σ S) 1
rw₂ rw₃ :
  Eq (α := MvPolynomial σ S) ((monomial d : (a : S) → MvPolynomial σ S) 1) ((monomial d : (a : S) → MvPolynomial σ S) 1)
⊢ Eq (α := MvPolynomial σ S)
    ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial d : (a : R) → MvPolynomial σ R) 1))
    ((monomial d : (a : S) → MvPolynomial σ S) 1)

Tactic:
rw [bind₂_monomial, f.map_one, one_mul]

Premises used: MvPolynomial.bind₂_monomial, RingHom.map_one, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
rw :
  Eq.{u_2 + 1} (α := Finset τ) (vars.{u_3, u_2} (R := R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ))
    (vars.{u_3, u_2} (R := R)
      ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        (∑ x ∈ φ.support, (monomial x : (a : R) → MvPolynomial σ R) (coeff x φ))))
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Finset τ) (vars.{u_3, u_2} (R := R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ))
    (vars.{u_3, u_2} (R := R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ))
⊢ Eq.{u_2 + 1} (α := Finset τ) (vars.{u_3, u_2} (R := R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ))
    (vars.{u_3, u_2} (R := R)
      (∑ x ∈ φ.support,
        (bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ))))

Tactic:
rw [← map_sum, ← φ.as_sum]

Premises used: MvPolynomial.as_sum, map_sum
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ LE.le.{u_2} (α := Finset τ)
    (vars.{u_3, u_2} (R := R)
      (∑ x ∈ φ.support,
        (bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ))))
    (φ.support.biUnion fun (i : σ →₀ ℕ) ↦
      vars.{u_3, u_2} (R := R)
        ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial i : (a : R) → MvPolynomial σ R) (coeff i φ))))

Tactic:
(vars_sum_subset _ _)

Premises used: Set.Mem, setOf, MvPolynomial.vars_sum_subset
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ Eq.{u_2 + 1} (α := Finset τ)
    (φ.support.biUnion fun (i : σ →₀ ℕ) ↦
      vars.{u_3, u_2} (R := R)
        ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial i : (a : R) → MvPolynomial σ R) (coeff i φ))))
    (φ.support.biUnion fun (d : σ →₀ ℕ) ↦
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
          ((C : (a : R) → MvPolynomial τ R) (coeff d φ) : MvPolynomial τ R)
          (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)).vars)

Tactic:
simp only [bind₁_monomial]

Premises used: MvPolynomial.bind₁_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ LE.le.{u_2} (α := Finset τ)
    (φ.support.biUnion fun (d : σ →₀ ℕ) ↦
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
          ((C : (a : R) → MvPolynomial τ R) (coeff d φ) : MvPolynomial τ R)
          (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)).vars)
    (φ.support.biUnion fun (d : σ →₀ ℕ) ↦ d.support.biUnion fun (i : σ) ↦ (f i).vars)

Tactic:
?_
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ LE.le.{u_2} (α := Finset τ) (φ.support.biUnion fun (d : σ →₀ ℕ) ↦ d.support.biUnion fun (i : σ) ↦ (f i).vars)
    (φ.vars.biUnion fun (i : σ) ↦ (f i).vars)

Tactic:
?_
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
calc_1 :
  LE.le.{u_2} (α := Finset τ)
    (φ.support.biUnion fun (d : σ →₀ ℕ) ↦
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
          ((C : (a : R) → MvPolynomial τ R) (coeff d φ) : MvPolynomial τ R)
          (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)).vars)
    (φ.support.biUnion fun (d : σ →₀ ℕ) ↦ d.support.biUnion fun (i : σ) ↦ (f i).vars)
calc_2 :
  LE.le.{u_2} (α := Finset τ) (φ.support.biUnion fun (d : σ →₀ ℕ) ↦ d.support.biUnion fun (i : σ) ↦ (f i).vars)
    (φ.vars.biUnion fun (i : σ) ↦ (f i).vars)
⊢ Subset.{u_2} (α := Finset τ) (vars.{u_3, u_2} (R := R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ))
    (φ.vars.biUnion fun (i : σ) ↦ (f i).vars)

Tactic:
calc (bind₁ f φ).vars
    _ = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by
      rw [← map_sum, ← φ.as_sum]
    _ ≤ φ.support.biUnion fun i : σ →₀ ℕ => ((bind₁ f) (monomial i (coeff i φ))).vars :=
      (vars_sum_subset _ _)
    _ = φ.support.biUnion fun d : σ →₀ ℕ => vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) := by
      simp only [bind₁_monomial]
    _ ≤ φ.support.biUnion fun d : σ →₀ ℕ => d.support.biUnion fun i => vars (f i) := ?_
    -- proof below
    _ ≤ φ.vars.biUnion fun i : σ => vars (f i) := ?_

Premises used: HMul.hMul, MvPolynomial.monomial, Finsupp.support, MvPolynomial.vars, Finset.biUnion, MvPolynomial.support, MvPolynomial.coeff, Finset.prod, MvPolynomial.bind₁, HPow.hPow, MvPolynomial.C, DFunLike.coe, Finset.sum, MvPolynomial.vars_sum_subset
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
calc_1 :
  ∀ a ∈ φ.support,
    (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
          ((C : (a : R) → MvPolynomial τ R) (coeff a φ) : MvPolynomial τ R)
          (∏ i ∈ a.support, HPow.hPow (β := ℕ) (f i) ((a : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)).vars ⊆
      a.support.biUnion fun (i : σ) ↦ (f i).vars
⊢ LE.le.{u_2} (α := Finset τ)
    (φ.support.biUnion fun (d : σ →₀ ℕ) ↦
      (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
          ((C : (a : R) → MvPolynomial τ R) (coeff d φ) : MvPolynomial τ R)
          (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)).vars)
    (φ.support.biUnion fun (d : σ →₀ ℕ) ↦ d.support.biUnion fun (i : σ) ↦ (f i).vars)

Tactic:
apply Finset.biUnion_mono

Premises used: Finset.biUnion_mono
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((C : (a : R) → MvPolynomial τ R) (coeff d φ) : MvPolynomial τ R)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)).vars ≤
    vars.{u_3, u_2} (R := R) ((C : (a : R) → MvPolynomial τ R) (coeff d φ)) ∪
      vars.{u_3, u_2} (R := R) (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ))

Tactic:
vars_mul _ _

Premises used: Set.Mem, setOf, MvPolynomial.vars_mul
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ LE.le.{u_2} (α := Finset τ)
    (vars.{u_3, u_2} (R := R) ((C : (a : R) → MvPolynomial τ R) (coeff d φ)) ∪
      vars.{u_3, u_2} (R := R) (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)))
    (vars.{u_3, u_2} (R := R) (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)))

Tactic:
simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]

Premises used: Finset.empty_union, Finset.Subset.refl, MvPolynomial.vars_C, Finset.le_iff_subset
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ LE.le.{u_2} (α := Finset τ)
    (vars.{u_3, u_2} (R := R) (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)))
    (d.support.biUnion fun (i : σ) ↦ (HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)).vars)

Tactic:
vars_prod _

Premises used: Set.Mem, setOf, MvPolynomial.vars_prod
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ LE.le.{u_2} (α := Finset τ)
    (d.support.biUnion fun (i : σ) ↦ (HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)).vars)
    (d.support.biUnion fun (i : σ) ↦ (f i).vars)

Tactic:
?_
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
calc_1 :
  LE.le.{u_2} (α := Finset τ)
    (d.support.biUnion fun (i : σ) ↦ (HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)).vars)
    (d.support.biUnion fun (i : σ) ↦ (f i).vars)
⊢ (HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((C : (a : R) → MvPolynomial τ R) (coeff d φ) : MvPolynomial τ R)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ) : MvPolynomial τ R)).vars ⊆
    d.support.biUnion fun (i : σ) ↦ (f i).vars

Tactic:
calc
      vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) ≤
          (C (coeff d φ)).vars ∪ (∏ i ∈ d.support, f i ^ d i).vars :=
        vars_mul _ _
      _ ≤ (∏ i ∈ d.support, f i ^ d i).vars := by
        simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]
      _ ≤ d.support.biUnion fun i : σ => vars (f i ^ d i) := vars_prod _
      _ ≤ d.support.biUnion fun i : σ => (f i).vars := ?_

Premises used: HMul.hMul, Finsupp.support, MvPolynomial.vars, Finset.biUnion, MvPolynomial.coeff, Finset.prod, MvPolynomial.vars_prod, HPow.hPow, MvPolynomial.vars_mul, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
calc_1 : ∀ a ∈ d.support, (HPow.hPow (β := ℕ) (f a) ((d : (a : σ) → ℕ) a : ℕ)).vars ⊆ (f a).vars
⊢ LE.le.{u_2} (α := Finset τ)
    (d.support.biUnion fun (i : σ) ↦ (HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)).vars)
    (d.support.biUnion fun (i : σ) ↦ (f i).vars)

Tactic:
apply Finset.biUnion_mono

Premises used: Finset.biUnion_mono
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
i : σ
_hi : i ∈ d.support
⊢ (HPow.hPow (β := ℕ) (f i) ((d : (a : σ) → ℕ) i : ℕ)).vars ⊆ (f i).vars

Tactic:
apply vars_pow

Premises used: MvPolynomial.vars_pow
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
calc_2 : (∃ a ∈ φ.support, ∃ a_1 ∈ a.support, j ∈ (f a_1).vars) → ∃ a ∈ φ.vars, j ∈ (f a).vars
⊢ Membership.mem (γ := Finset τ) (φ.support.biUnion fun (d : σ →₀ ℕ) ↦ d.support.biUnion fun (i : σ) ↦ (f i).vars) j →
    Membership.mem (γ := Finset τ) (φ.vars.biUnion fun (i : σ) ↦ (f i).vars) j

Tactic:
simp_rw [Finset.mem_biUnion]

Premises used: Finset.mem_biUnion
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hj : j ∈ (f i).vars
⊢ ∃ a ∈ φ.vars, j ∈ (f a).vars

Tactic:
⟨i, (mem_vars_iff_mem_support _).mpr ⟨d, hd, hi⟩, hj⟩

Premises used: Iff.mpr, And.intro, Exists.intro, MvPolynomial.mem_vars_iff_mem_support
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hj : j ∈ (f i).vars
⊢ ∃ a ∈ φ.vars, j ∈ (f a).vars

Tactic:
exact ⟨i, (mem_vars_iff_mem_support _).mpr ⟨d, hd, hi⟩, hj⟩
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h :
  Membership.mem (γ := Finset τ) (vars.{u_3, u_2} (R := R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) j
⊢ ∃ i ∈ φ.vars, j ∈ (f i).vars

Tactic:
simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne] using vars_bind₁ f φ h

Premises used: MvPolynomial.mem_support_iff, Ne, exists_prop, MvPolynomial.vars_bind₁, Finset.mem_biUnion
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h :
  Membership.mem (γ := Finset τ) (vars.{u_3, u_2} (R := R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) j
⊢ ∃ i ∈ φ.vars, j ∈ (f i).vars

Tactic:
classical
  simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne] using vars_bind₁ f φ h

Premises used: MvPolynomial.mem_support_iff, Ne, exists_prop, Finset.mem_biUnion
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β : Type u_6
⊢ Eq (α := α → MvPolynomial β R → MvPolynomial α R)
    (Functor.mapConst (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (α := α) (β := β) :
      α → MvPolynomial β R → MvPolynomial α R)
    (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (α := β) (β := α) ∘ Function.const β :
      α → MvPolynomial β R → MvPolynomial α R)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α : Type u_6
x : MvPolynomial α R
⊢ Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) id x = x

Tactic:
simp [(· <$> ·)]

Premises used: Functor.map
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β γ : Type u_6
g : α → β
h : β → γ
x : MvPolynomial α R
⊢ Eq (α := MvPolynomial γ R) (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (h ∘ g) x : MvPolynomial γ R)
    (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) h
        (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) g x) :
      MvPolynomial γ R)

Tactic:
simp [(· <$> ·)]

Premises used: Functor.map
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β : Type u_6
x : MvPolynomial α R
y : MvPolynomial β R
simp :
  Eq (α := MvPolynomial α R)
    ((bind₁ fun (a : α) ↦ (bind₁ fun (x : β) ↦ X a : (a : MvPolynomial β R) → MvPolynomial α R) y :
          (a : MvPolynomial α R) → MvPolynomial α R)
        x :
      MvPolynomial α R)
    ((bind₁ ((fun (y_1 : β → α) ↦ (rename y_1 : (a : MvPolynomial β R) → MvPolynomial α R) y) ∘ Function.const β) :
          (a : MvPolynomial α R) → MvPolynomial α R)
        x :
      MvPolynomial α R)
⊢ Eq (α := MvPolynomial α R) (x <* y : MvPolynomial α R)
    (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (Function.const β) x <*> y : MvPolynomial α R)

Tactic:
simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]

Premises used: MvPolynomial.bind₁_rename, Seq.seq, SeqLeft.seqLeft, Functor.map
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β : Type u_6
x : MvPolynomial α R
y : MvPolynomial β R
⊢ Eq (α := MvPolynomial α R)
    ((bind₁ fun (a : α) ↦ (bind₁ fun (x : β) ↦ X a : (a : MvPolynomial β R) → MvPolynomial α R) y :
          (a : MvPolynomial α R) → MvPolynomial α R)
        x :
      MvPolynomial α R)
    ((bind₁ ((fun (y_1 : β → α) ↦ (rename y_1 : (a : MvPolynomial β R) → MvPolynomial α R) y) ∘ Function.const β) :
          (a : MvPolynomial α R) → MvPolynomial α R)
        x :
      MvPolynomial α R)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β : Type u_6
x : MvPolynomial α R
y : MvPolynomial β R
simp :
  Eq (α := MvPolynomial β R) ((bind₁ fun (x : α) ↦ y : (a : MvPolynomial α R) → MvPolynomial β R) x : MvPolynomial β R)
    ((bind₁ (Function.const α y) : (a : MvPolynomial α R) → MvPolynomial β R) x : MvPolynomial β R)
⊢ Eq (α := MvPolynomial β R) (x *> y : MvPolynomial β R)
    (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (β := β → β) (Function.const α id) x <*> y :
      MvPolynomial β R)

Tactic:
simp [SeqRight.seqRight, Seq.seq, (· <$> ·), bind₁_rename]

Premises used: MvPolynomial.bind₁_rename, Seq.seq, SeqRight.seqRight, Functor.map
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β : Type u_6
x : MvPolynomial α R
y : MvPolynomial β R
⊢ Eq (α := MvPolynomial β R) ((bind₁ fun (x : α) ↦ y : (a : MvPolynomial α R) → MvPolynomial β R) x : MvPolynomial β R)
    ((bind₁ (Function.const α y) : (a : MvPolynomial α R) → MvPolynomial β R) x : MvPolynomial β R)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β : Type u_6
g : α → β
x : MvPolynomial α R
⊢ Eq (α := MvPolynomial β R) (pure (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) g <*> x : MvPolynomial β R)
    (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) g x : MvPolynomial β R)

Tactic:
simp [(· <$> ·), pure, Seq.seq]

Premises used: Pure.pure, Seq.seq, Functor.map
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type u_6} (f : α → β) (x : MvPolynomial α R),
    Eq (α := MvPolynomial β R)
      (do
        let a ← x
        pure (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (f a) : MvPolynomial β R)
      (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) f x : MvPolynomial β R)

Tactic:
aesop