How to reason with bundled definitions

Stream: mathlib4

[Snir Broshi]

How can I reason with bundled definitions?
For example, I want a hypothesis that says a specific function is a group/graph isomorphism-

import Mathlib.Algebra.Group.Equiv.Basic
import Mathlib.Combinatorics.SimpleGraph.Maps

 theorem comp_group_iso_implies_injective
   {A B C : Type}
   [Group A] [Group C]
   (f : A -> B) (g : B -> C)
   :
   -- what hypothesis says "(g ∘ f) is an isomorphism from A to C"?
   A ≃* C ->
   f.Injective
   := sorry

 theorem comp_graph_iso_implies_injective
   {A B C : Type}
   (gA : SimpleGraph A) (gC : SimpleGraph C)
   (f : A -> B) (g : B -> C)
   :
   -- what hypothesis says "(g ∘ f) is an isomorphism from gA to gC"?
   gA ≃g gC ->
   f.Injective
   := sorry

I'm looking for a way to say "the expression (...) is an isomorphism between ...", but a bundled approach for it is also fine- a way to convert the existingisomorphism property to a new bundled property that contains the two functions and the fact that their composition is an isomorphism would also work. But crucially the point is to avoid restating the definition of isomorphism.
Wdyt?
(I'm new to Lean btw, this is probably a common pitfall)

[Matt Diamond]

you could write (f : A -> B) (g : B -> C) (iso : A ≃* C) (iso_eq_comp : iso = g ∘ f)

though it seems like what you're really trying to prove in these specific examples is just docs#Function.Injective.of_comp ... it just so happens that the injectivity of the composition is due to being an equivalence

[Matt Diamond]

I guess my point is that these lemmas are trying to do too much... you only need a simpler fact in each case

[Snir Broshi]

Matt Diamond said:

you could write (f : A -> B) (g : B -> C) (iso : A ≃* C) (iso_eq_comp : iso = g ∘ f)

though it seems like what you're really trying to prove in these specific examples is just docs#Function.Injective.of_comp ... it just so happens that the injectivity of the composition is due to being an equivalence

Isn't there a better solution without using equality like that?
Also, using the Injective.of_comp still requires showing that the composition is injective, which brings us back to requiring that the composition is an isomorphism

[Snir Broshi]

Matt Diamond said:

I guess my point is that these lemmas are trying to do too much... you only need a simpler fact in each case

How do you suggest formalizing the theorem: "if g∘f is an isomorphism between groups A and B, then f is injective"

[Matt Diamond]

I'm saying that I don't know if it's a useful theorem to have

the critical parts are these lemmas:
1) an isomorphism is injective
2) if (g ∘ f) is injective, then f is injective

then, in whatever larger proof you're working on, you tie these together using the equality iso = (g ∘ f) to get where you need to go

[Snir Broshi]

There's no larger proof, and I'm trying to avoid using equality like that

[Matt Diamond]

you could use docs#Function.Bijective which is unbundled, but it sounds like you want to talk about specific kinds of isomorphisms

[Matt Diamond]

you could write your own definition, like

import Mathlib

def isMulEquiv {A B} [Mul A] [Mul B] (f : A → B) : Prop :=
∃ (g : A ≃* B), g = f

[Matt Diamond]

maybe someone else will have a better idea... it's tricky to work with these bundled structures in a way that specifies the content of the structure

[Snir Broshi]

The issue is that I want to use defeq instead of semantical equality
And the gist of my question is since bundled definitions are so common in mathlib, whether Lean or mathlib have some mechanism to unbundle definitions when talking about them, like some fancy syntax or macro. Or alternatively, if it's common to define both bundled and unbundled definitions of stuff (like group isomorphism) and prove they're interchangable