Proof expansion inside proof

Stream: new members

[Marcin Tomaszewski]

hi,
assuming we have

lemma zero_add (n : mynat) : 0 + n = n :=
begin
induction n with d hd,
refl,
rw add_succ,
...
end

then in the new proof we use the zero_add for example:

lemma ...
begin
rw zero_add,
...
end

how could we expand / add the zero_add proof inside the new proof to get something like below?

lemma ...
begin
zero_add:
begin
...
end
rw zero_add,
...
end

[Ruben Van de Velde]

Please use #backticks

[Yaël Dillies]

You can do

lemma ...
begin
have zero_add : ∀ (n : mynat), 0 + n = n,
{
...
},
rw zero_add,
...
end

[Marcin Tomaszewski]

thanks

[Hagb (Junyu Guo)]

(deleted: Sorry, I accidentally sent the message)