tip for filling in holes

Stream: general

[Kevin Buzzard]

Sometimes in Lean you sit down to write a definition or a theorem, knowing that it will be really easy and fun. I was just in that situation. I need to write down some maps between localized rings and prove that they have some properties, but now I know that the localization interface is excellent and that pretty much every single one of my proofs will look like name_of_function _ _ _ _ _.

[Kevin Buzzard]

However, I have run into an unexpected annoyance.

[Kevin Buzzard]

Here is my skeleton set-up.

[Kevin Buzzard]

definition localization.loc_loc_is_loc {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g ⊆ Spec.D' f) :
(localization.away g) ≃ᵣ localization.away (localization.of_comm_ring R (powers f) g) :=
{ to_fun := _,
  inv_fun := _,
  left_inv := _,
  right_inv := _,
  is_ring_hom := _
}

[Kevin Buzzard]

The idea now is that I just fill in all the holes one by one.

[Kevin Buzzard]

But I want the holes to have red squiggles under them!

[Kevin Buzzard]

And for some reason, only the last one does

[Kevin Buzzard]

and the associated complaint is full of metavariables

[Kevin Buzzard]

because it depends on some earlier holes

[Kenny Lau]

begin end

[Kevin Buzzard]

and then remove it later?

[Kevin Buzzard]

because it's a def

[Kenny Lau]

i just fill in stuff in front of begin end

[Kenny Lau]

I mean, replace your _ with begin end

[Kenny Lau]

I can show you that in person next week ^^

[Kevin Buzzard]

begin exact _ end

[Kevin Buzzard]

:-)

[Kevin Buzzard]

Many thanks Kenny!

[Kevin Buzzard]

I feel like there are so many little tips like this, and it's unclear to me where they should be put.

[Kenny Lau]

you don’t need exact _