Problematic AddCommMonoid instance in DirectSum.Internal

Stream: mathlib4

[Richard Copley]

I noticed that the def grade₁_equiv below goes through, unless I import Mathlib. I bisected the problem to an instance in Mathlib.Algebra.DirectSum.Internal that's sufficient to cause the errors below. If the section between the two rows of dashes is commented out, the errors go away.

Should AddCommMonoid.ofSubmonoidOnSemiring only be made a local instance where needed?
What's the usual way to fix this kind of problem?

import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

noncomputable section
namespace ExteriorAlgebra

variable (V : Type*) [AddCommGroup V] [Module ℝ V]

abbrev grade₁ := LinearMap.range (ExteriorAlgebra.ι ℝ : V →ₗ[ℝ] ExteriorAlgebra ℝ V)
abbrev grade (k : ℕ) := grade₁ V ^ k
theorem grade₁_eq : grade V 1 = grade₁ V := pow_one _
def grade₁_equiv' : grade₁ V ≃ₗ[ℝ] V := .symm <| .ofLeftInverse ι_leftInverse

#synth ∀ i, AddCommMonoid (grade V i)
-- fun i => Submodule.addCommMonoid (grade V i)

--------------------------------------------------------------------------------
-- from `Mathlib.Algebra.DirectSum.Internal`:
variable {ι : Type*} {σ S R : Type*}
instance AddCommMonoid.ofSubmonoidOnSemiring [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R]
    (A : ι → σ) : ∀ i, AddCommMonoid (A i) := fun i => by infer_instance

#synth ∀ i, AddCommMonoid (grade V i)
-- fun i => AddCommMonoid.ofSubmonoidOnSemiring (grade V) i

-- The instances are propositionally equal
example (i) : Submodule.addCommMonoid (grade V i) =
    AddCommMonoid.ofSubmonoidOnSemiring (grade V) i :=
  rfl -- (succeeds, but "by with_reducible rfl" fails)
--------------------------------------------------------------------------------

def grade₁_equiv : grade V 1 ≃ₗ[ℝ] V := by
  rw [grade₁_eq]
  exact grade₁_equiv' V
-- tactic 'rewrite' failed, motive is not type correct
-- V : Type u_1
-- inst¹ : AddCommGroup V
-- inst : Module ℝ V
-- ⊢ ↥(grade V 1) ≃ₗ[ℝ] V

def grade₁_equiv_2 : grade V 1 ≃ₗ[ℝ] V := grade₁_eq V ▸ grade₁_equiv' V
-- type mismatch
--   grade₁_equiv' V
-- has type
--   @LinearEquiv ℝ ℝ Real.semiring Real.semiring (RingHom.id ℝ) (RingHom.id ℝ)
--     (_ : RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)) (_ : RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)) (↥(grade₁ V))
--     V (AddCommMonoid.ofSubmonoidOnSemiring LinearMap.range (ι ℝ)) AddCommGroup.toAddCommMonoid
--     (Submodule.module (grade₁ V)) inst : Type u_1
-- but is expected to have type
--   @LinearEquiv ℝ ℝ Real.semiring Real.semiring (RingHom.id ℝ) (RingHom.id ℝ)
--     (_ : RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)) (_ : RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)) (↥(grade₁ V))
--     V (AddCommMonoid.ofSubmonoidOnSemiring (grade V) 1) AddCommGroup.toAddCommMonoid (Submodule.module (grade₁ V))
--     inst : Type u_1

end ExteriorAlgebra
end

[Eric Wieser]

Are you aware of the grading file for ExteriorAlgebra?

[Richard Copley]

Yes.

[Eric Wieser]

I think you want

def grade₁_equiv : grade V 1 ≃ₗ[ℝ] V :=
  .ofEq _ _ (grade₁_eq _) ≪≫ₗ grade₁_equiv' V

[Eric Wieser]

Using rw for data is usually a bad idea unless you have no other option

[Richard Copley]

Great, thanks. I had found that proof. (Sorry I didn't mention it. It was in an earlier draft of my question, but I cut it for brevity.) I thought the instance "problem" was still worth asking about. Maybe it won't be an issue. I'll see how I get on.