feat(algebra/group/hom): add inv_comp and comp_inv (#6046)

Two missing lemmas. Used in the Liquid Tensor Experiment.

Inversion for monoid hom is (correctly) only defined when the target is a comm_group; this explains the choice of typeclasses. I follow `inv_apply` and use `{}` rather than `[]`, but this is certainly not my area of expertise.

src/algebra/group/hom.lean

@@ -764,15 +764,23 @@ add_decl_doc add_monoid_hom.has_neg
   (f : M →* G) (x : M) :
   f⁻¹ x = (f x)⁻¹ := rfl
 
+@[simp, to_additive] lemma inv_comp {M N A} {mM : monoid M} {gN : monoid N}
+  {gA : comm_group A} (φ : N →* A) (ψ : M →* N) : φ⁻¹.comp ψ = (φ.comp ψ)⁻¹ :=
+by { ext, simp only [function.comp_app, inv_apply, coe_comp] }
+
+@[simp, to_additive] lemma comp_inv {M A B} {mM : monoid M} {mA : comm_group A}
+  {mB : comm_group B} (φ : A →* B) (ψ : M →* A) : φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹ :=
+by { ext, simp only [function.comp_app, inv_apply, map_inv, coe_comp] }
+
 /-- If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism
-sending `x` to `(f x) / (g x). -/
+sending `x` to `(f x) / (g x)`. -/
 @[to_additive]
 instance {M G} [monoid M] [comm_group G] : has_div (M →* G) :=
 ⟨λ f g, mk' (λ x, f x / g x) $ λ a b,
   by simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]⟩
 
 /-- If `f` and `g` are monoid homomorphisms to an additive commutative group, then `f - g`
-is the homomorphism sending `x` to `(f x) - (g x). -/
+is the homomorphism sending `x` to `(f x) - (g x)`. -/
 add_decl_doc add_monoid_hom.has_sub
 
 @[simp, to_additive] lemma div_apply {M G} {mM : monoid M} {gG : comm_group G}