How to expand a definition

Stream: new members

[Lars Ericson]

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]

you can just do unfold coprime at h6

[Ruben Van de Velde]

Or use docs#nat.coprime.gcd_eq_one