ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ TaggedPrepartition.tag (biUnionTagged π πi) J' =
    TaggedPrepartition.tag (πi (biUnionIndex π (fun J => (πi J).toPrepartition) J')) J'
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ TaggedPrepartition.tag (biUnionTagged π πi) J' = TaggedPrepartition.tag (πi J) J'
rw [← π.biUnionIndex_of_mem (πi := fun J => (πi J).toPrepartition) hJ hJ']
no goals
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ TaggedPrepartition.tag (biUnionTagged π πi) J' =
    TaggedPrepartition.tag (πi (biUnionIndex π (fun J => (πi J).toPrepartition) J')) J'
rfl