Zulip Chat Archive

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):

Or use docs#nat.coprime.gcd_eq_one


Last updated: Dec 20 2023 at 11:08 UTC