Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: equip x0 x2.

Assume H1: equip x1 x3.

Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with x0, x2, equip (setsum x0 x1) (setsum x2 x3) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x4 of type ι → ι be given.

Assume H2: bij x0 x2 x4.

Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with x0, x2, x4, equip (setsum x0 x1) (setsum x2 x3) leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: inj x0 x2 x4.

Assume H4: ∀ x5 . In x5 x2 ⟶ ∃ x6 . and (In x6 x0) (x4 x6 = x5).

Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with x1, x3, equip (setsum x0 x1) (setsum x2 x3) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x5 of type ι → ι be given.

Assume H5: bij x1 x3 x5.

Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with x1, x3, x5, equip (setsum x0 x1) (setsum x2 x3) leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H6: inj x1 x3 x5.

Assume H7: ∀ x6 . In x6 x3 ⟶ ∃ x7 . and (In x7 x1) (x5 x7 = x6).

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setsum x0 x1, setsum x2 x3, combine_funcs x0 x1 (λ x6 . Inj0 (x4 x6)) (λ x6 . Inj1 (x5 x6)).

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setsum x0 x1, setsum x2 x3, combine_funcs x0 x1 (λ x6 . Inj0 (x4 x6)) (λ x6 . Inj1 (x5 x6)) leaving 2 subgoals.

Apply unknownprop_6c2d83e01e35cd8c7db6bd981b84dd9dade9ed501c5a94229b14f6869614ac63 with x0, x1, setsum x2 x3, λ x6 . Inj0 (x4 x6), λ x6 . Inj1 (x5 x6) leaving 3 subgoals.

Apply unknownprop_a48f98e8977f0c6ed45175c0ee32c0078f43cea0a5c01b41606702afcab1761e with x0, x2, setsum x2 x3, x4, Inj0 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying unknownprop_191ba52f7596eac3c13199d06abc28bd67d9baab59edf519e02ad968d3f37956 with x2, x3.

Apply unknownprop_a48f98e8977f0c6ed45175c0ee32c0078f43cea0a5c01b41606702afcab1761e with x1, x3, setsum x2 x3, x5, Inj1 leaving 2 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying unknownprop_25f4c8732a356859144d2a5c5d9e8c513248dd09f08255deb7914574cf9de821 with x2, x3.

Let x6 of type ι be given.

Assume H8: In x6 x0.

Let x7 of type ι be given.

Assume H9: In x7 x1.

The subproof is completed by applying unknownprop_2909aa42e9d0a354d060bc7d707070a586f9ab4666ef2c2e92d5cb1072a37e98 with x4 x6, x5 x7.

Let x6 of type ι be given.

Assume H8: In x6 (setsum x2 x3).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x2, x3, x6, λ x7 . ∃ x8 . and (In x8 (setsum x0 x1)) (combine_funcs x0 x1 (λ x9 . Inj0 (x4 x9)) (λ x9 . Inj1 (x5 x9)) x8 = x7) leaving 3 subgoals.

The subproof is completed by applying H8.

Let x7 of type ι be given.

Assume H9: In x7 x2.

Apply H4 with x7, ∃ x8 . and (In x8 (setsum x0 x1)) (combine_funcs x0 x1 (λ x9 . Inj0 (x4 x9)) (λ x9 . Inj1 (x5 x9)) x8 = Inj0 x7) leaving 2 subgoals.

The subproof is completed by applying H9.

Let x8 of type ι be given.

Assume H10: (λ x9 . and (In x9 x0) (x4 x9 = x7)) x8.

Apply andE with In x8 x0, x4 x8 = x7, ∃ x9 . and (In x9 (setsum x0 x1)) (combine_funcs x0 x1 (λ x10 . Inj0 (x4 x10)) (λ x10 . Inj1 (x5 x10)) ... = ...) leaving 2 subgoals.

...

■

Proofgold Proof