Sum Alg Equiv mem restrict Degree Var

lemma sumAlgEquiv_mem_restrictDegreeVar {R : Type*} [CommSemiring R]    {S₁ S₂ : Type*} (p : MvPolynomial (S₁ ⊕ S₂) R) {b : S₁ ⊕ S₂ → ℕ}    (hp : p ∈ restrictDegreeVar (S₁ ⊕ S₂) R b) :    (MvPolynomial.sumAlgEquiv R S₁ S₂) p ∈      restrictDegreeVar S₁ (MvPolynomial S₂ R) (b ∘ Sum.inl) := by  intro s hs  obtain ⟨m, hm, hs_eq⟩ : ∃ m : (S₁ ⊕ S₂) →₀ ℕ,      m ∈ p.support ∧ s = m.comapDomain Sum.inl Sum.inl_injective.injOn := by    have h_sum : (MvPolynomial.sumAlgEquiv R S₁ S₂) p =        ∑ m ∈ p.support,          (MvPolynomial.monomial (m.comapDomain Sum.inl Sum.inl_injective.injOn))            (MvPolynomial.monomial (m.comapDomain Sum.inr Sum.inr_injective.injOn)              (p.coeff m)) := by      conv_lhs => rw [p.as_sum]      rw [map_sum]      exact Finset.sum_congr rfl fun _ _ => sumToIter_monomial_aux _ _    contrapose! hs    simp only [h_sum, SetLike.mem_coe, Finsupp.mem_support_iff, ne_eq, not_not]    erw [Finsupp.finsetSum_apply]    refine Finset.sum_eq_zero fun x hx => ?_    erw [AddMonoidAlgebra.lsingle_apply, AddMonoidAlgebra.lsingle_apply]; aesop  intro i  subst hs_eq  rw [Finsupp.comapDomain_apply]  exact hp hm (Sum.inl i)