indentation issue in mathport

Stream: mathlib4

[Patrick Massot]

I think this kind of issues has already been reported and they are Lean 4 formatter issues instead of mathport issue but let me make sure I'm not missing something. Mathport write things like

instance [Zero α] [Mul α] [NoZeroDivisors α] :
    NoZeroDivisors
      αᵃᵒᵖ where eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
    Or.imp (fun hx => unop_injective hx) (fun hy => unop_injective hy)
      (@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _ <| op_injective H)

which doesn't work (with a super confusing error message) but changing the code layout to

instance [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ where
eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
  Or.imp (fun hx => unop_injective hx) (fun hy => unop_injective hy)
  (@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _ <| op_injective H)

fixes everything.

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/1945!