## Stream: new members

### Topic: How to expand a definition

#### Lars Ericson (Jan 10 2021 at 16:10):

mathlib has this definition:

@[reducible] def coprime (m n : ℕ) : Prop := gcd m n = 1


I have a goal state which is

h6 : a.num.nat_abs.coprime a.denom,


I want to expand this definition into the gcd in the coprime definition. I find myself writing a use-once lemma:

lemma expand_coprime (m n : ℕ) : coprime m n → (gcd m n = 1) :=
begin
exact (rfl.congr rfl).mp,
end


I can then apply this lemma to expand h6 into the gcd form of the underlying definition:

    have h8 := expand_coprime a.num.nat_abs a.denom,
have h9 := h8 h6,


giving

h8: a.num.nat_abs.coprime a.denom → a.num.nat_abs.gcd a.denom = 1
h9: a.num.nat_abs.gcd a.denom = 1


Is there a way to expand a given definition, without having to declare a lemma?

#### Kenny Lau (Jan 10 2021 at 16:12):

you can just do unfold coprime at h6

#### Ruben Van de Velde (Jan 10 2021 at 19:11):

Last updated: May 15 2021 at 23:13 UTC