Closed pechersky closed 1 year ago
This line should have
`match_pattern
https://github.com/leanprover-community/mathport/blob/8695123e7e09ab6fd41b16ba38f475207cfde213/Mathport/Syntax/Translate/Command.lean#L60
as needed for here https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Data/Sum/Basic.lean#L466-L476
This line should have
https://github.com/leanprover-community/mathport/blob/8695123e7e09ab6fd41b16ba38f475207cfde213/Mathport/Syntax/Translate/Command.lean#L60
as needed for here https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Data/Sum/Basic.lean#L466-L476