broken

Author: YaelDillies

Mathlib/Algebra/MvPolynomial/Monad.lean

@@ -338,8 +338,10 @@ instance lawfulFunctor : LawfulFunctor fun σ => MvPolynomial σ R where
   id_map := by intros; simp [(· <$> ·)]
   comp_map := by intros; simp [(· <$> ·)]
 
+set_option allowUnsafeReducibility true in
+attribute [local reducible] MvPolynomial in
 instance lawfulMonad : LawfulMonad fun σ => MvPolynomial σ R where
-  pure_bind := by intros; simp [pure, bind]
+  pure_bind a p := by intros; simp [pure, bind, bind₁, MvPolynomial.aeval_X]
   bind_assoc := by intros; simp [bind, ← bind₁_comp_bind₁]
   seqLeft_eq _ _ := by
     simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]; simp [rename_eq]; rfl

Mathlib/RepresentationTheory/Equiv.lean

@@ -35,8 +35,8 @@ variable (k G) in
   on `k[H]` is equivalent to the trivial representation. -/
 def ofMulActionSubsingletonEquivTrivial : (ofMulAction k G H).Equiv (trivial k G k) :=
   letI : Unique H := uniqueOfSubsingleton 1
-  .mk (Finsupp.LinearEquiv.finsuppUnique _ _ _) fun g ↦ by
-    ext a; simp [Subsingleton.elim (g • a) a]
+  .mk (MonoidAlgebra.uniqueLinearEquiv k G).toLinearEquiv fun g ↦ _
+    -- ext a; simp [Subsingleton.elim (g • a) a]
 
 @[simp]
 lemma ofMulActionSubsingletonEquivTrivial_apply (f : H →₀ k) :