∀ {α : Type u_2} {β : Type u_3} {γ : Type u_1} (x : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }),
  Disjoint
    (Set.range
      ⇑(Function.Embedding.inl.trans
              (match x with
              | ⟨(f, g), disj⟩ =>
                {
                  toFun := fun x =>
                    match x with
                    | Sum.inl a => f a
                    | Sum.inr b => g b,
                  inj' := ⋯ }),
            Function.Embedding.inr.trans
              (match x with
              | ⟨(f, g), disj⟩ =>
                {
                  toFun := fun x =>
                    match x with
                    | Sum.inl a => f a
                    | Sum.inr b => g b,
                  inj' := ⋯ })).1)
    (Set.range
      ⇑(Function.Embedding.inl.trans
              (match x with
              | ⟨(f, g), disj⟩ =>
                {
                  toFun := fun x =>
                    match x with
                    | Sum.inl a => f a
                    | Sum.inr b => g b,
                  inj' := ⋯ }),
            Function.Embedding.inr.trans
              (match x with
              | ⟨(f, g), disj⟩ =>
                {
                  toFun := fun x =>
                    match x with
                    | Sum.inl a => f a
                    | Sum.inr b => g b,
                  inj' := ⋯ })).2)