## Stream: general

### Topic: tip for filling in holes

#### Kevin Buzzard (Apr 20 2018 at 10:11):

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 (Apr 20 2018 at 10:12):

However, I have run into an unexpected annoyance.

#### Kevin Buzzard (Apr 20 2018 at 10:12):

Here is my skeleton set-up.

#### Kevin Buzzard (Apr 20 2018 at 10:12):

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 (Apr 20 2018 at 10:12):

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

#### Kevin Buzzard (Apr 20 2018 at 10:13):

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

#### Kevin Buzzard (Apr 20 2018 at 10:13):

And for some reason, only the last one does

#### Kevin Buzzard (Apr 20 2018 at 10:14):

and the associated complaint is full of metavariables

#### Kevin Buzzard (Apr 20 2018 at 10:14):

because it depends on some earlier holes

begin end

#### Kevin Buzzard (Apr 20 2018 at 10:14):

and then remove it later?

#### Kevin Buzzard (Apr 20 2018 at 10:14):

because it's a def

#### Kenny Lau (Apr 20 2018 at 10:14):

i just fill in stuff in front of begin end

#### Kenny Lau (Apr 20 2018 at 10:14):

I mean, replace your _ with begin end

#### Kenny Lau (Apr 20 2018 at 10:15):

I can show you that in person next week ^^

#### Kevin Buzzard (Apr 20 2018 at 10:15):

begin exact _ end

:-)

#### Kevin Buzzard (Apr 20 2018 at 10:15):

Many thanks Kenny!

#### Kevin Buzzard (Apr 20 2018 at 10:16):

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

#### Kenny Lau (Apr 20 2018 at 10:16):

you don’t need exact _

Last updated: May 08 2021 at 19:11 UTC