indentation style

Stream: mathlib4

[Kevin Buzzard]

I just suggested this

lemma isNontrivial_iff_exists_unit {K : Type*} [Field K] {w : Valuation K Γ₀} :
    w.IsNontrivial ↔ ∃ x : Kˣ, w x ≠ 1 :=
  ⟨fun ⟨x, hx0, hx1⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 0, hx0⟩
    ⟨Units.mk0 x (w.ne_zero_iff.mp hx0), hx1⟩,
    fun ⟨x, hx⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 1, hx⟩
    ⟨x, w.ne_zero_iff.mpr (Units.ne_zero x), hx⟩⟩

in a PR and then delegated, but it occurs to me that actually I'm still not at all perfect on indentation style. Is this OK? I #printed the proof to see if that gave me any clues but it's full of mp := and match.

[Yaël Dillies]

A much more readable style is IMO:

lemma isNontrivial_iff_exists_unit {K : Type*} [Field K] {w : Valuation K Γ₀} :
    w.IsNontrivial ↔ ∃ x : Kˣ, w x ≠ 1 where
  mp := fun ⟨x, hx0, hx1⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 0, hx0⟩
    ⟨Units.mk0 x (w.ne_zero_iff.mp hx0), hx1⟩
  mpr := fun ⟨x, hx⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 1, hx⟩
    ⟨x, w.ne_zero_iff.mpr (Units.ne_zero x), hx⟩

or even

lemma isNontrivial_iff_exists_unit {K : Type*} [Field K] {w : Valuation K Γ₀} :
    w.IsNontrivial ↔ ∃ x : Kˣ, w x ≠ 1 where
  mp := fun ⟨x, hx0, hx1⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 0, hx0⟩; ⟨.mk0 x (w.ne_zero_iff.mp hx0), hx1⟩
  mpr := fun ⟨x, hx⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 1, hx⟩; ⟨x, w.ne_zero_iff.mpr x.ne_zero, hx⟩

[Junyan Xu]

In this case I think it's nicer as (removed, same as Yaël's suggestion (I didn't realize this can/should be applied to Iff before reading some of their PRs))
If I write this in your style I'd unindent fun ⟨x, hx⟩ ↦ by two spaces.

[Ruben Van de Velde]

Or

lemma isNontrivial_iff_exists_unit {K : Type*} [Field K] {w : Valuation K Γ₀} :
    w.IsNontrivial ↔ ∃ x : Kˣ, w x ≠ 1 where
  mp | ⟨x, hx0, hx1⟩ =>
    have : Nontrivial Γ₀ := ⟨w x, 0, hx0⟩; ⟨Units.mk0 x (w.ne_zero_iff.mp hx0), hx1⟩
  mpr | ⟨x, hx⟩ =>
    have : Nontrivial Γ₀ := ⟨w x, 1, hx⟩; ⟨x, w.ne_zero_iff.mpr x.ne_zero, hx⟩

[Yaël Dillies]

Ooh, I knew you couldn't pattern-match left to a := and I also knew about this field | constructor => proof syntax, but I didn't put one and one together to deduce that you could use the latter to circumvent the former. Thanks Ruben!

[Junyan Xu]

But can't we make mp ⟨x, hx0, hx1⟩ := work?

[Yaël Dillies]

I wish!

[Ruben Van de Velde]

Same

[Junyan Xu]

I think the { mp := ... } syntax recently gained the ability to take arguments before :=. (Which PR is it?) Has where also become more powerful lately? I'm only recently starting to see syntax like algebraMap.toFun := ... when constructing an Algebra.

[Eric Wieser]

where has always had this power, as far as I'm aware

[Yaël Dillies]

algebraMap.toFun has been there for at least a year

[Junyan Xu]

Here is a case where where is not as convenient as { }: I can't introduce instances beforehand that apply to all the fields with where.

[Filippo A. E. Nuccio]

I understand all these suggestions, but it seems that the problem that @Kevin Buzzard was facing is not solved. With all the suggested solutions, the infoview for #print outputs the same thing.

[Ruben Van de Velde]

The question was what the source should look like, and the #print was just because that sometimes helps with deciding that, as far as I can tell