chore(Algebra/Lie/Quotient): remove unused variable 'I' (#19864)

Removes an unused `variable {I}` declaration which causes the `I` to sometimes show up as a hypothesis whose type is a metavariable.

When this file was originally ported in #4822, the variable `I` was declared to have type `LieIdeal R L` and then the lower-down `variable {N I}` declaration served to modify the implicitness of that existing variable:
```lean
...
variable (N N' : LieSubmodule R L M) (I J : LieIdeal R L)

...

namespace Quotient

variable {N I}
...
```

However, in #15538, the initial (typed) declaration of `I` was removed. This had the effect of causing an `I` to appear with a metavarable in some contexts, e.g. the proof of `lieQuotientLieRing.leibniz_lie`:

```lean
I : ?m.48970
```

I noticed this problem when I tried running `exact?` in the proof of `lieQuotientLieRing.leibniz_lie`; doing so returned a nonsensical result.

Mathlib/Algebra/Lie/Quotient.lean

@@ -43,7 +43,7 @@ instance : HasQuotient M (LieSubmodule R L M) :=
 
 namespace Quotient
 
-variable {N I}
+variable {N}
 
 instance addCommGroup : AddCommGroup (M ⧸ N) :=
   Submodule.Quotient.addCommGroup _