implicit argument in mathlibport field

Stream: mathlib4

[Patrick Massot]

In https://github.com/leanprover-community/mathlib3port/blob/25aba9a00dd0c7af7df362a275829ce34ac8dd48/Mathbin/Algebra/Ring/Opposite.lean#L81-L85, we see

instance [Zero α] [Mul α] [NoZeroDivisors α] :
    NoZeroDivisors
      αᵐᵒᵖ where eq_zero_or_eq_zero_of_mul_eq_zero x y (H : op (_ * _) = op (0 : α)) :=

which has extraneous x and y on the third line because those are implicit arguments. @Mario Carneiro is this something mathport could improve?

[Mario Carneiro]

no, this is the implicit lambda change and it's hard to tell from the input syntax that it is being triggered

[Mario Carneiro]

This happens whenever lean 3 uses \lam x y, to introduce variables in \forall {x y : foo}, ...

[Patrick Massot]

Indeed this comes from \lam x y in the lean 3 code.

[Patrick Massot]

I'm trying to add an explanation to the porting wiki. Is the following accurate enough to do more good than harm?

* If you get an error message containing "the following variables have been introduced by the implicit lambda feature", it may be that the Lean 3 code contained a proof term with a lambda introducing an implicit argument and this confused mathport. For instance you could have in Lean 3 example := ∀ {n : ℕ}, ... := λ n, bar which becomes in Lean 4 example := ∀ {n : Nat}, ... := bar.