avoid expansion of class fields

Stream: mathlib4

[Filippo A. E. Nuccio]

What is the lean4 equivalent of the .. when defining a term of a certain class? Consider the following

import Mathlib.RingTheory.DiscreteValuationRing.Basic

example (A : Type) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] [LocalRing A]
  (h : LocalRing.maximalIdeal A ≠ ⊥) : DiscreteValuationRing A :=

If I put a _ and hover on the bulb and ask to generate skeleton for the structure under construction I get

example (A : Type) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] [LocalRing A]
  (h : LocalRing.maximalIdeal A ≠ ⊥) : DiscreteValuationRing A where
    principal := _
    exists_pair_ne := _
    isUnit_or_isUnit_of_add_one := _
    not_a_field' := _

Now, DiscreteValuationRing is defined as

class DiscreteValuationRing (R : Type u) [CommRing R] [IsDomain R]
    extends IsPrincipalIdealRing R, LocalRing R : Prop where
  not_a_field' : maximalIdeal R ≠ ⊥

and principal is the name of the constructor for IsPrincipalIdealRing, hence the first field. Now, LocalRing in itself extends Nontrivial (whose constructor is exists_pair_ne) and has isUnit_or_isUnit_of_add_one as the other constructor: of course I can find them by destructuring my term LocalRing A, but I would like to be able to remove the two constructors

    exists_pair_ne := _
    isUnit_or_isUnit_of_add_one := _

and simply pass a term of type LocalRing A (found by infer_instance). What is the syntax?

[Eric Wieser]

Are you asking what the equivalent of Lean 3's {foo := _, ..bar} is? It's { bar with foo := _ }, or if using where, __ := bar

[Filippo A. E. Nuccio]

So this should be like this?

example (A : Type) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] [LocalRing A]
  (h : LocalRing.maximalIdeal A ≠ ⊥) : DiscreteValuationRing A where
    principal := sorry
    not_a_field' := sorry
   _ _ := by infer_instance

[Floris van Doorn]

I expect you want to remove the space between the two _

[Filippo A. E. Nuccio]

Ah! Let me try.

[Filippo A. E. Nuccio]

Ok, thanks @Eric Wieser and @Floris van Doorn ! It basically works, in the sense (but this was probably the same in Lean3) that it cannot really guess what __ is (and understandably so), so

example (A : Type) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] [LocalRing A]
  (h : LocalRing.maximalIdeal A ≠ ⊥) : DiscreteValuationRing A where
    principal := by infer_instance
    not_a_field' := h
    __  := by infer_instance

gives a problem in the last line (it has no clue of what to look for), but

example (A : Type) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] [LocalRing A]
  (h : LocalRing.maximalIdeal A ≠ ⊥) : DiscreteValuationRing A where
    principal := by infer_instance
    not_a_field' := h
    __ : LocalRing A := by infer_instance

is OK. The other option is to explicitly name the term LocalRing A:

example (A : Type) [CommRing A] [IsDomain A] [IsPrincipalIdealRing A] [hA : LocalRing A]
  (h : LocalRing.maximalIdeal A ≠ ⊥) : DiscreteValuationRing A where
    principal := by infer_instance
    not_a_field' := h
    __ := hA

Is there a mathlib preference between the previous two solutions?

[Eric Wieser]

Huh, I didn't even know that __ : LocalRing A := by infer_instance was legal!

[Eric Wieser]

I'm used to seeing __ := inferInstanceAs <| LocalRing A, but I think __ : LocalRing A := inferInstance is probably best

[Eric Wieser]

__ : LocalRing A := ‹_› would also work here, but that doesn't work in general

[Filippo A. E. Nuccio]

Right! But at any rate you discourage naming the term LocalRing A to call it explicitely, right?