Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.fst ≫
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inl +
      { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.snd ≫
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inr =
    𝟙
      { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
          snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
          inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
          inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
          inr_snd := ⋯ }.pt

Tactic:
ext1

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      ({ pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.fst ≫
          { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inl +
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.snd ≫
          { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
              snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
              inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
              inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inr) =
    Hom.hom
      (𝟙
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.pt)