awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R) ((bind₁ X : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
x : R
⊢ Eq (α := MvPolynomial τ R)
    ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) x) : MvPolynomial τ R)
    ((C : (a : R) → MvPolynomial τ R) x : MvPolynomial τ R)

Tactic:
algHom_C _ _

Premises used: MvPolynomial.algHom_C
-- 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
r : R
⊢ Eq (α := MvPolynomial σ S)
    ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) r) : MvPolynomial σ S)
    ((f : (a : R) → MvPolynomial σ S) r : MvPolynomial σ S)

Tactic:
eval₂Hom_C f X r

Premises used: MvPolynomial.X, MvPolynomial.eval₂Hom_C
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
hC :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R) ((RingHom.comp (bind₂ C) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
      ((RingHom.comp (RingHom.id (MvPolynomial σ R)) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
hX :
  ∀ (i : σ) (m : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) (coeff m ((bind₂ C : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))
      (coeff m ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ R) (bind₂ C) (RingHom.id (MvPolynomial σ R))

Tactic:
ext : 2
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
x : R
⊢ Eq (α := MvPolynomial σ R) ((RingHom.comp (bind₂ C) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((RingHom.comp (RingHom.id (MvPolynomial σ R)) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
i : σ
m : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R) (coeff m ((bind₂ C : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))
    (coeff m ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))

Tactic:
simp
-- 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
⊢ (bind₂ f).comp C = f

Tactic:
RingHom.ext <| bind₂_C_right _

Premises used: RingHom.ext, MvPolynomial.bind₂_C_right
-- 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
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ S)
    ((join₂ : (a : MvPolynomial σ (MvPolynomial σ S)) → MvPolynomial σ S)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ (MvPolynomial σ S)) φ) :
      MvPolynomial σ S)
    ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S)

Tactic:
simp only [join₂, bind₂, eval₂Hom_map_hom, RingHom.id_comp]

Premises used: MvPolynomial.bind₂, MvPolynomial.eval₂Hom_map_hom, MvPolynomial.join₂, RingHom.id_comp
-- 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
⊢ RingHom.comp join₂ (map f) = bind₂ f

Tactic:
RingHom.ext <| join₂_map _

Premises used: RingHom.ext, MvPolynomial.join₂_map
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
p : MvPolynomial σ R
rw :
  Eq (α := MvPolynomial τ R) ((aeval (id ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
    ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
rw₁ rw₂ :
  Eq (α := MvPolynomial τ R) ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
    ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((aeval id : (a : MvPolynomial (MvPolynomial τ R) R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial (MvPolynomial τ R) R) p) :
      MvPolynomial τ R)
    ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)

Tactic:
rw [aeval_rename, Function.id_comp]

Premises used: MvPolynomial.aeval_rename, Function.id_comp
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ R)
    ((join₁ : (a : MvPolynomial (MvPolynomial τ R) R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial (MvPolynomial τ R) R) φ) :
      MvPolynomial τ R)
    ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R)

Tactic:
aeval_id_rename _ _

Premises used: MvPolynomial.aeval_id_rename
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial (MvPolynomial σ R) R →ₐ[R] MvPolynomial σ R) (bind₁ id) join₁

Tactic:
rfl

Premises used: MvPolynomial.join₁, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ (MvPolynomial σ R) →+* MvPolynomial σ R) (bind₂ (RingHom.id (MvPolynomial σ R))) join₂

Tactic:
rfl

Premises used: MvPolynomial.join₂, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial υ R)
    ((bind₁ g : (a : MvPolynomial τ R) → MvPolynomial υ R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial υ R)
    ((bind₁ fun (i : σ) ↦ (bind₁ g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial υ R)
        φ :
      MvPolynomial υ R)

Tactic:
simp [bind₁, ← comp_aeval]

Premises used: MvPolynomial.bind₁, MvPolynomial.comp_aeval
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
hf :
  ∀ (i : σ),
    Eq (α := MvPolynomial υ R)
      (((bind₁ g).comp (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
      ((bind₁ fun (i : σ) ↦ (bind₁ g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i) :
            (a : MvPolynomial σ R) → MvPolynomial υ R)
          (X i) :
        MvPolynomial υ R)
⊢ (bind₁ g).comp (bind₁ f) = bind₁ fun (i : σ) ↦ (bind₁ g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i)

Tactic:
ext1
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i : σ
⊢ Eq (α := MvPolynomial υ R)
    (((bind₁ g).comp (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
    ((bind₁ fun (i : σ) ↦ (bind₁ g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial υ R)
        (X i) :
      MvPolynomial υ R)

Tactic:
apply bind₁_bind₁

Premises used: MvPolynomial.bind₁_bind₁
-- 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 : 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)
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)))
⊢ (bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f)

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 : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
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)

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 : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
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:
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 : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ T)
    ((bind₂ g : (a : MvPolynomial σ S) → MvPolynomial σ T) ((bind₂ f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
      MvPolynomial σ T)
    ((bind₂ ((bind₂ g).comp f) : (a : MvPolynomial σ R) → MvPolynomial σ T) φ : MvPolynomial σ T)

Tactic:
RingHom.congr_fun (bind₂_comp_bind₂ f g) φ

Premises used: Multiset.sum, Multiset.foldr, RingHom.congr_fun, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.bind₂_comp_bind₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
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)
⊢ AlgHom.comp (rename g) (bind₁ f) = bind₁ fun (i : σ) ↦ (rename g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i)

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial υ R)
    ((rename g : (a : MvPolynomial τ R) → MvPolynomial υ R) ((bind₁ f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial υ R)
    ((bind₁ fun (i : σ) ↦ (rename g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial υ R)
        φ :
      MvPolynomial υ R)

Tactic:
AlgHom.congr_fun (rename_comp_bind₁ f g) φ

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, AlgHom.congr_fun, MvPolynomial.rename_comp_bind₁, 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
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
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 φ
⊢ 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)

Tactic:
simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]

Premises used: MvPolynomial.eval₂_map, MvPolynomial.coe_eval₂Hom, MvPolynomial.bind₂, MvPolynomial.eval₂_comp_right
-- 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 : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
e_g :
  ∀ (x : σ),
    Eq (α := MvPolynomial σ T)
      (Function.comp (β := MvPolynomial σ S) (⇑(map g) : (a : MvPolynomial σ S) → MvPolynomial σ T) X x) (X x)
⊢ 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:
congr 1 with : 1
-- 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 : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x : σ
⊢ Eq (α := MvPolynomial σ T)
    (Function.comp (β := MvPolynomial σ S) (⇑(map g) : (a : MvPolynomial σ S) → MvPolynomial σ T) X x) (X x)

Tactic:
simp only [Function.comp_apply, map_X]

Premises used: Function.comp_apply, MvPolynomial.map_X
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
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)
⊢ (bind₁ f).comp (rename g) = bind₁ (f ∘ g)

Tactic:
ext1 i
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial υ R)
    ((bind₁ f : (a : MvPolynomial τ R) → MvPolynomial υ R) ((rename g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial υ R)
    ((bind₁ (f ∘ g) : (a : MvPolynomial σ R) → MvPolynomial υ R) φ : MvPolynomial υ R)

Tactic:
AlgHom.congr_fun (bind₁_comp_rename f g) φ

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.bind₁_comp_rename, AlgHom.congr_fun, 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
f : S →+* MvPolynomial σ T
g : R →+* S
φ : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ T)
    ((bind₂ f : (a : MvPolynomial σ S) → MvPolynomial σ T) ((map g : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
      MvPolynomial σ T)
    ((bind₂ (f.comp g) : (a : MvPolynomial σ R) → MvPolynomial σ T) φ : MvPolynomial σ T)

Tactic:
simp [bind₂]

Premises used: MvPolynomial.bind₂
-- 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 →+* S
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)
⊢ Eq (α := R →+* MvPolynomial σ S) (RingHom.comp (map f) C) (RingHom.comp C f)

Tactic:
ext1
-- 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 →+* S
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:
apply map_C

Premises used: MvPolynomial.map_C
-- Module: Mathlib.Algebra.MvPolynomial.Monad
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [bind₁, map_aeval, algebraMap_eq]

Premises used: MvPolynomial.map_aeval, MvPolynomial.bind₁, MvPolynomial.algebraMap_eq
-- Module: Mathlib.Algebra.MvPolynomial.Monad
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
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)
⊢ 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)

Tactic:
rw [hom_bind₁, map_comp_C, ← eval₂Hom_map_hom]

Premises used: MvPolynomial.map_comp_C, MvPolynomial.eval₂Hom_map_hom, MvPolynomial.hom_bind₁
-- Module: Mathlib.Algebra.MvPolynomial.Monad
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)
    ((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:
rfl
-- 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 →+* S
g : σ → S
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)
⊢ (eval₂Hom f g).comp C = f

Tactic:
ext1 r
-- 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 →+* S
g : σ → S
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:
eval₂_C f g r

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂_C, MvPolynomial.eval₂, Finset.sum
-- 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 →+* S
g : σ → S
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:
exact eval₂_C f g r

Premises used: MvPolynomial.eval₂_C
-- Module: Mathlib.Algebra.MvPolynomial.Monad
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [hom_bind₁, eval₂Hom_comp_C]

Premises used: MvPolynomial.hom_bind₁, MvPolynomial.eval₂Hom_comp_C
-- Module: Mathlib.Algebra.MvPolynomial.Monad
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
φ : MvPolynomial σ R
⊢ Eq.{u_4 + 1} (α := S)
    ((aeval f : (a : MvPolynomial τ R) → S)
        ((bind₁ g : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) :
      S)
    ((aeval fun (i : σ) ↦ (aeval f : (a : MvPolynomial τ R) → S) (g i) : (a : MvPolynomial σ R) → S) φ : S)

Tactic:
eval₂Hom_bind₁ _ _ _ _

Premises used: MvPolynomial.eval₂Hom_bind₁
-- Module: Mathlib.Algebra.MvPolynomial.Monad
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
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)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] S) (AlgHom.comp (aeval f) (bind₁ g))
    (aeval fun (i : σ) ↦ (aeval f : (a : MvPolynomial τ R) → S) (g i))

Tactic:
ext1
-- Module: Mathlib.Algebra.MvPolynomial.Monad
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
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:
apply aeval_bind₁

Premises used: MvPolynomial.aeval_bind₁