awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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 : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
hC :
  ∀ (x : R),
    Eq (α := MvPolynomial σ T) ((((bind₂ g).comp (bind₂ f)).comp C : (a : R) → MvPolynomial σ T) x : MvPolynomial σ T)
      (((bind₂ ((bind₂ g).comp f)).comp C : (a : R) → MvPolynomial σ T) x : MvPolynomial σ T)
⊢ (bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f)
have hX : ∀ (i : σ) (m : σ →₀ ℕ),
  Eq.{u_5 + 1} (α := T) (coeff m (((bind₂ g).comp (bind₂ f) : (a : MvPolynomial σ R) → MvPolynomial σ T) (X i)))
    (coeff m ((bind₂ ((bind₂ g).comp f) : (a : MvPolynomial σ R) → MvPolynomial σ T) (X i)))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
⊢ AlgHom.comp (rename g) (bind₁ f) = bind₁ fun (i : σ) ↦ (rename g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i)
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial υ R)
    ((AlgHom.comp (rename g) (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
    ((bind₁ fun (i : σ) ↦ (rename g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial υ R)
        (X i) :
      MvPolynomial υ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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 : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ T)
    ((map g : (a : MvPolynomial σ S) → MvPolynomial σ T) ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
      MvPolynomial σ T)
    ((bind₂ (RingHom.comp (map g) f) : (a : MvPolynomial σ R) → MvPolynomial σ T) φ : MvPolynomial σ T)
have simp : eval₂ (RingHom.comp (map g) f)
    (Function.comp (β := MvPolynomial σ S) (⇑(map g) : (a : MvPolynomial σ S) → MvPolynomial σ T) X) φ =
  eval₂ (RingHom.comp (map g) f) X φ
Tactic: simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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 : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (map g) f)
      (Function.comp (β := MvPolynomial σ S) (⇑(map g) : (a : MvPolynomial σ S) → MvPolynomial σ T) X) φ =
    eval₂ (RingHom.comp (map g) f) X φ
have e_g : ∀ (x : σ),
  Eq (α := MvPolynomial σ T)
    (Function.comp (β := MvPolynomial σ S) (⇑(map g) : (a : MvPolynomial σ S) → MvPolynomial σ T) X x) (X x)
Tactic: congr 1 with : 1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
⊢ (bind₁ f).comp (rename g) = bind₁ (f ∘ g)
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial υ R)
    (((bind₁ f).comp (rename g) : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
    ((bind₁ (f ∘ g) : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
⊢ Eq (α := R →+* MvPolynomial σ S) (RingHom.comp (map f) C) (RingHom.comp C f)
have a : ∀ (x : R),
  Eq (α := MvPolynomial σ S) ((RingHom.comp (map f) C : (a : R) → MvPolynomial σ S) x : MvPolynomial σ S)
    ((RingHom.comp C f : (a : R) → MvPolynomial σ S) x : MvPolynomial σ S)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ Eq.{u_4 + 1} (α := S)
    ((f : (a : MvPolynomial τ R) → S) ((bind₁ g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) : S)
    ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
have rw : Eq.{u_4 + 1} (α := S)
  ((f : (a : MvPolynomial τ R) → S) ((aeval g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) : S)
  ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
Tactic: rw [bind₁, map_aeval, algebraMap_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
rw :
  Eq.{u_4 + 1} (α := S)
    ((f : (a : MvPolynomial τ R) → S) ((aeval g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) : S)
    ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
⊢ Eq.{u_4 + 1} (α := S)
    ((f : (a : MvPolynomial τ R) → S) ((bind₁ g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) : S)
    ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
have rw₁ : Eq.{u_4 + 1} (α := S)
  ((eval₂Hom (f.comp (algebraMap R (MvPolynomial τ R))) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) :
        (a : MvPolynomial σ R) → S)
      φ :
    S)
  ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
Tactic: rw [bind₁, map_aeval, algebraMap_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
rw :
  Eq.{u_4 + 1} (α := S)
    ((f : (a : MvPolynomial τ R) → S) ((aeval g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) : S)
    ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
rw₁ :
  Eq.{u_4 + 1} (α := S)
    ((eval₂Hom (f.comp (algebraMap R (MvPolynomial τ R))) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) :
          (a : MvPolynomial σ R) → S)
        φ :
      S)
    ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
⊢ Eq.{u_4 + 1} (α := S)
    ((f : (a : MvPolynomial τ R) → S) ((bind₁ g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) : S)
    ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
have rw₂ : Eq.{u_4 + 1} (α := S)
  ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
  ((eval₂Hom (f.comp C) fun (i : σ) ↦ (f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)
Tactic: rw [bind₁, map_aeval, algebraMap_eq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ S)
    ((map f : (a : MvPolynomial τ R) → MvPolynomial τ S) ((bind₁ g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial τ S)
    ((bind₁ fun (i : σ) ↦ (map f : (a : MvPolynomial τ R) → MvPolynomial τ S) (g i) :
          (a : MvPolynomial σ S) → MvPolynomial τ S)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
      MvPolynomial τ S)
have rw : Eq (α := MvPolynomial τ S)
  ((eval₂Hom C fun (i : σ) ↦ (map f : (a : MvPolynomial τ R) → MvPolynomial τ S) (g i) :
        (a : MvPolynomial σ S) → MvPolynomial τ S)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
    MvPolynomial τ S)
  ((bind₁ fun (i : σ) ↦ (map f : (a : MvPolynomial τ R) → MvPolynomial τ S) (g i) :
        (a : MvPolynomial σ S) → MvPolynomial τ S)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
    MvPolynomial τ S)
Tactic: rw [hom_bind₁, map_comp_C, ← eval₂Hom_map_hom]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
⊢ (eval₂Hom f g).comp C = f
have a : ∀ (r : R), Eq.{u_4 + 1} (α := S) (((eval₂Hom f g).comp C : (a : R) → S) r : S) ((f : (a : R) → S) r : S)
Tactic: ext1 r
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : τ → S
h : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ Eq.{u_4 + 1} (α := S)
    ((eval₂Hom f g : (a : MvPolynomial τ R) → S)
        ((bind₁ h : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) :
      S)
    ((eval₂Hom f fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) : (a : MvPolynomial σ R) → S) φ : S)
have rw : Eq.{u_4 + 1} (α := S)
  ((eval₂Hom ((eval₂Hom f g).comp C) fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) :
        (a : MvPolynomial σ R) → S)
      φ :
    S)
  ((eval₂Hom f fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) : (a : MvPolynomial σ R) → S) φ : S)
Tactic: rw [hom_bind₁, eval₂Hom_comp_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : τ → S
h : σ → MvPolynomial τ R
φ : MvPolynomial σ R
rw :
  Eq.{u_4 + 1} (α := S)
    ((eval₂Hom ((eval₂Hom f g).comp C) fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) :
          (a : MvPolynomial σ R) → S)
        φ :
      S)
    ((eval₂Hom f fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) : (a : MvPolynomial σ R) → S) φ : S)
⊢ Eq.{u_4 + 1} (α := S)
    ((eval₂Hom f g : (a : MvPolynomial τ R) → S)
        ((bind₁ h : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) :
      S)
    ((eval₂Hom f fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) : (a : MvPolynomial σ R) → S) φ : S)
have rw₁ : Eq.{u_4 + 1} (α := S)
  ((eval₂Hom f fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) : (a : MvPolynomial σ R) → S) φ : S)
  ((eval₂Hom f fun (i : σ) ↦ (eval₂Hom f g : (a : MvPolynomial τ R) → S) (h i) : (a : MvPolynomial σ R) → S) φ : S)
Tactic: rw [hom_bind₁, eval₂Hom_comp_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
⊢ Eq (α := MvPolynomial σ R →ₐ[R] S) (AlgHom.comp (aeval f) (bind₁ g))
    (aeval fun (i : σ) ↦ (aeval f : (a : MvPolynomial τ R) → S) (g i))
have hf : ∀ (i : σ),
  Eq.{u_4 + 1} (α := S) ((AlgHom.comp (aeval f) (bind₁ g) : (a : MvPolynomial σ R) → S) (X i) : S)
    ((aeval fun (i : σ) ↦ (aeval f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) (X i) : S)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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
⊢ (eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g
have 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)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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)
⊢ (eval₂Hom f g).comp (bind₂ h) = eval₂Hom ((eval₂Hom f g).comp h) g
have 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)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ S)
    ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial d : (a : R) → MvPolynomial σ R) 1))
    ((monomial d : (a : S) → MvPolynomial σ S) 1)
have 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
Tactic: rw [bind₂_monomial, f.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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
⊢ Eq (α := MvPolynomial σ S)
    ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial d : (a : R) → MvPolynomial σ R) 1))
    ((monomial d : (a : S) → MvPolynomial σ S) 1)
have rw₁ : HMul.hMul (α := MvPolynomial σ S) 1 ((monomial d : (a : S) → MvPolynomial σ S) 1) =
  (monomial d : (a : S) → MvPolynomial σ S) 1
Tactic: rw [bind₂_monomial, f.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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
⊢ Eq (α := MvPolynomial σ S)
    ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial d : (a : R) → MvPolynomial σ R) 1))
    ((monomial d : (a : S) → MvPolynomial σ S) 1)
have rw₂ : Eq (α := MvPolynomial σ S) ((monomial d : (a : S) → MvPolynomial σ S) 1) ((monomial d : (a : S) → MvPolynomial σ S) 1)
Tactic: rw [bind₂_monomial, f.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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 τ) (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 φ))))
have 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 φ))))
Tactic: rw [← map_sum, ← φ.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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 φ))))
⊢ 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 φ))))
have 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) φ))
Tactic: rw [← map_sum, ← φ.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ 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)
have 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)
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) := ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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)
⊢ 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)
have 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)
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) := ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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)
have 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
Tactic: apply Finset.biUnion_mono
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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 ⊆
    d.support.biUnion fun (i : σ) ↦ (f i).vars
have 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)
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 := ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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)
have calc_1 : ∀ a ∈ d.support, (HPow.hPow (β := ℕ) (f a) ((d : (a : σ) → ℕ) a : ℕ)).vars ⊆ (f a).vars
Tactic: apply Finset.biUnion_mono
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ 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
have calc_2 : (∃ a ∈ φ.support, ∃ a_1 ∈ a.support, j ∈ (f a_1).vars) → ∃ a ∈ φ.vars, j ∈ (f a).vars
Tactic: simp_rw [Finset.mem_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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) (x <* y : MvPolynomial α R)
    (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (Function.const β) x <*> y : MvPolynomial α R)
have 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)
Tactic: simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
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) (x *> y : MvPolynomial β R)
    (Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) (β := β → β) (Function.const α id) x <*> y :
      MvPolynomial β R)
have 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)
Tactic: simp [SeqRight.seqRight, Seq.seq, (· <$> ·), bind₁_rename]