Binary operations + linebreaks

Stream: mathlib4

[Yury G. Kudryashov]

Do we have guidelines on the position / alignment of binary operations in multiline formulas? What should I do if I want to split

example : long_term = long_term1 + long_term2 - long_term3 := by sorry

with each long_term* on a separate line?

[Eric Wieser]

What does the pretty printer say?

[Yury G. Kudryashov]

iteratedDeriv_vcomp_three.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E} {x : 𝕜}
  (hg : ContDiffAt 𝕜 3 g (f x)) (hf : ContDiffAt 𝕜 3 f x) :
  iteratedDeriv 3 (g ∘ f) x =
    ((iteratedFDeriv 𝕜 3 g (f x)) fun x_1 => deriv f x) +
          (iteratedFDeriv 𝕜 2 g (f x)) ![iteratedDeriv 2 f x, deriv f x] +
        2 • (iteratedFDeriv 𝕜 2 g (f x)) ![deriv f x, iteratedDeriv 2 f x] +
      (fderiv 𝕜 g (f x)) (iteratedDeriv 3 f x)

[Aaron Liu]

looks slightly weird but is logical

[Yury G. Kudryashov]

iteratedDerivWithin_vcomp_three.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E} {s : Set 𝕜}
  {t : Set E} {x : 𝕜} (hg : ContDiffWithinAt 𝕜 3 g t (f x)) (hf : ContDiffWithinAt 𝕜 3 f s x) (ht : UniqueDiffOn 𝕜 t)
  (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t) :
  iteratedDerivWithin 3 (g ∘ f) s x =
    ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun x_1 => derivWithin f s x) +
          (iteratedFDerivWithin 𝕜 2 g t (f x)) ![iteratedDerivWithin 2 f s x, derivWithin f s x] +
        2 • (iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
      (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x)

[Yury G. Kudryashov]

Part of the weirdness comes from the fact that the pretty printer adds parentheses to deal with inline lambdas, and the opening parentheses go far away.

[Yury G. Kudryashov]

I'm going to use this style, but with all terms after = indented at the same level.

[Eric Wieser]

Ideally that would be how the pretty printer worked too

[Eric Wieser]

That is, don't increase indentation for wrapped subterms unless there are also parentheses